Possible (long standing) issue in the BPF verifier?

Possible (long standing) issue in the BPF verifier?

[Kris Van Hees]

So, I found the following in a BPF log on kernel 6.8.0:

BPF: 799: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,smin=smin3
2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,smin=smin3
2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff))
BPF: 800: (07) r4 += 7                     ; frame2: R4_w=scalar(smin=umin=smin32=umin32=7,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1ff))
BPF: 801: (57) r4 &= -8                    ; frame2: R4_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1f8))

And when checking kernel 6.5.0:

BPF: 791: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,umax=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,umax=255,var_off=(0x0; 0xff))
BPF: 792: (07) r4 += 7                     ; frame2: R4_w=scalar(umin=7,umax=262,var_off=(0x0; 0x1ff))
BPF: 793: (57) r4 &= -8                    ; frame2: R4_w=scalar(umax=262,var_off=(0x0; 0x1f8)) 

And kernel 5.15.0:

BPF: 799: (bf) r4 = r6
BPF: 800: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
BPF: 800: (07) r4 += 7
BPF: 801: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umin_value=7,umax_value=262,var_off=(0x0; 0x1ff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
BPF: 801: (57) r4 &= -8
BPF: 802: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umax_value=262,var_off=(0x0; 0x1f8)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value

This code is supposed to round the value in %r4 up to the nearest multiple of
8.  So, if %r4 is 255, one would expect this to yield 256.  Yet, it does not.

Re: Possible (long standing) issue in the BPF verifier?

[Eugene Loh]

I'm confused what problem you're describing here.  Are you saying there 
is an opportunity for the verifier to do better?  Or are you saying that 
the actual computation is incorrect?

So far as I can tell, the actual computation is fine (at least with 
5.15.0).  Specifically, if r4 is assigned 253, 254, 255, 256, and 257, 
then after the +=7 and &=-8 I get 256, 256, 256, 256, and 264, 
respectively.  That looks right.

Now, [7:262] & -8 = [0:256].  So when the verifier bounds the result as 
[0:262], it isn't wrong -- it simply is not as aggressive as it could 
be.  It should be able to bound the result more tightly.  Is that the 
issue you're talking about?

On 4/27/24 21:35, Kris Van Hees wrote:
> So, I found the following in a BPF log on kernel 6.8.0:
>
> BPF: 799: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,smin=smin3
> 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,smin=smin3
> 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff))
> BPF: 800: (07) r4 += 7                     ; frame2: R4_w=scalar(smin=umin=smin32=umin32=7,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1ff))
> BPF: 801: (57) r4 &= -8                    ; frame2: R4_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1f8))
>
> And when checking kernel 6.5.0:
>
> BPF: 791: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,umax=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,umax=255,var_off=(0x0; 0xff))
> BPF: 792: (07) r4 += 7                     ; frame2: R4_w=scalar(umin=7,umax=262,var_off=(0x0; 0x1ff))
> BPF: 793: (57) r4 &= -8                    ; frame2: R4_w=scalar(umax=262,var_off=(0x0; 0x1f8))
>
> And kernel 5.15.0:
>
> BPF: 799: (bf) r4 = r6
> BPF: 800: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> BPF: 800: (07) r4 += 7
> BPF: 801: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umin_value=7,umax_value=262,var_off=(0x0; 0x1ff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> BPF: 801: (57) r4 &= -8
> BPF: 802: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umax_value=262,var_off=(0x0; 0x1f8)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
>
> This code is supposed to round the value in %r4 up to the nearest multiple of
> 8.  So, if %r4 is 255, one would expect this to yield 256.  Yet, it does not.
>

Re: Possible (long standing) issue in the BPF verifier?

[Kris Van Hees]

On Mon, Apr 29, 2024 at 12:42:36PM -0400, Eugene Loh wrote:
> I'm confused what problem you're describing here.  Are you saying there is
> an opportunity for the verifier to do better?  Or are you saying that the
> actual computation is incorrect?
> 
> So far as I can tell, the actual computation is fine (at least with
> 5.15.0).  Specifically, if r4 is assigned 253, 254, 255, 256, and 257, then
> after the +=7 and &=-8 I get 256, 256, 256, 256, and 264, respectively. 
> That looks right.

That is not what I see on my OL8 UEK7 (5.15.0-based kernel).  It calculates
[0:262] as bound as shown below.

> Now, [7:262] & -8 = [0:256].  So when the verifier bounds the result as
> [0:262], it isn't wrong -- it simply is not as aggressive as it could be. 
> It should be able to bound the result more tightly.  Is that the issue
> you're talking about?

Well, in this case it ought to be fine (and it is on kernels other than 6.8.0
of those that I tested), but that is simply because you use %r4 as upper limit
for a loop condition.  But if we were to e.g. use that value as iterator value
(which is what I am planning to do so this works on 6.8.0 also), then it is
important that %r4 *is* a multiple of 8.  So, the more inaccurate calculation
that the verifier does here *can* cause actual issues because the value that
is calculated is not correct.  That would mean that values calculated with the
use of bitwise operations like AND cannot be used as actual numeric values in
all cases.

That is a real issue.

> On 4/27/24 21:35, Kris Van Hees wrote:
> > So, I found the following in a BPF log on kernel 6.8.0:
> > 
> > BPF: 799: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,smin=smin3
> > 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,smin=smin3
> > 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff))
> > BPF: 800: (07) r4 += 7                     ; frame2: R4_w=scalar(smin=umin=smin32=umin32=7,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1ff))
> > BPF: 801: (57) r4 &= -8                    ; frame2: R4_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1f8))
> > 
> > And when checking kernel 6.5.0:
> > 
> > BPF: 791: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,umax=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,umax=255,var_off=(0x0; 0xff))
> > BPF: 792: (07) r4 += 7                     ; frame2: R4_w=scalar(umin=7,umax=262,var_off=(0x0; 0x1ff))
> > BPF: 793: (57) r4 &= -8                    ; frame2: R4_w=scalar(umax=262,var_off=(0x0; 0x1f8))
> > 
> > And kernel 5.15.0:
> > 
> > BPF: 799: (bf) r4 = r6
> > BPF: 800: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> > BPF: 800: (07) r4 += 7
> > BPF: 801: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umin_value=7,umax_value=262,var_off=(0x0; 0x1ff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> > BPF: 801: (57) r4 &= -8
> > BPF: 802: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umax_value=262,var_off=(0x0; 0x1f8)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> > 
> > This code is supposed to round the value in %r4 up to the nearest multiple of
> > 8.  So, if %r4 is 255, one would expect this to yield 256.  Yet, it does not.
> > 

Re: Possible (long standing) issue in the BPF verifier?

[Eugene Loh]

On 4/29/24 13:22, Kris Van Hees wrote:

> On Mon, Apr 29, 2024 at 12:42:36PM -0400, Eugene Loh wrote:
>> I'm confused what problem you're describing here.  Are you saying there is
>> an opportunity for the verifier to do better?  Or are you saying that the
>> actual computation is incorrect?
>>
>> So far as I can tell, the actual computation is fine (at least with
>> 5.15.0).  Specifically, if r4 is assigned 253, 254, 255, 256, and 257, then
>> after the +=7 and &=-8 I get 256, 256, 256, 256, and 264, respectively.
>> That looks right.
> That is not what I see on my OL8 UEK7 (5.15.0-based kernel).  It calculates
> [0:262] as bound as shown below.

I agree that the verifier is bounding the value as [0:262].

The distinction I was trying to make was between the actual value in the 
register and the bounds on that value used by the verifier. E.g., let's 
say we do %r4=%r6.  The actual value in the register might be 255, but 
all the verifier happens to know is that the value is [0:255].  After 
the "round up to multiple of 8" operation, the actual value in the 
register appears to be 256, which is correct. Meanwhile, the bounds used 
by the verifier are [0:262].  The actual value (256) is indeed contained 
in these bounds.  In that sense the bounds are correct.  But I agree:  
based on the information on hand, the bounds could actually be tighter:  
[0:256].

>> Now, [7:262] & -8 = [0:256].  So when the verifier bounds the result as
>> [0:262], it isn't wrong -- it simply is not as aggressive as it could be.
>> It should be able to bound the result more tightly.  Is that the issue
>> you're talking about?
> Well, in this case it ought to be fine (and it is on kernels other than 6.8.0
> of those that I tested), but that is simply because you use %r4 as upper limit
> for a loop condition.  But if we were to e.g. use that value as iterator value
> (which is what I am planning to do so this works on 6.8.0 also), then it is
> important that %r4 *is* a multiple of 8.  So, the more inaccurate calculation
> that the verifier does here *can* cause actual issues because the value that
> is calculated is not correct.  That would mean that values calculated with the
> use of bitwise operations like AND cannot be used as actual numeric values in
> all cases.
>
> That is a real issue.

Sorry, I'm really confused.  I would think that there is some actual 
arithmetic that gets performed at execution time using values in 
registers, while the BPF verifier is acting at program load time doing 
some static analysis to bound values.  Those are two different things.  
Maybe this will help resolve my confusion.  Are you saying that:

*)  at program load time, the BPF verifier allows unsafe programs?
*)  at program load time, the BPF verifier forbids safe programs?
*)  at run time, arithmetic on register values produces incorrect values?

>> On 4/27/24 21:35, Kris Van Hees wrote:
>>> So, I found the following in a BPF log on kernel 6.8.0:
>>>
>>> BPF: 799: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,smin=smin3
>>> 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,smin=smin3
>>> 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff))
>>> BPF: 800: (07) r4 += 7                     ; frame2: R4_w=scalar(smin=umin=smin32=umin32=7,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1ff))
>>> BPF: 801: (57) r4 &= -8                    ; frame2: R4_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1f8))
>>>
>>> And when checking kernel 6.5.0:
>>>
>>> BPF: 791: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,umax=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,umax=255,var_off=(0x0; 0xff))
>>> BPF: 792: (07) r4 += 7                     ; frame2: R4_w=scalar(umin=7,umax=262,var_off=(0x0; 0x1ff))
>>> BPF: 793: (57) r4 &= -8                    ; frame2: R4_w=scalar(umax=262,var_off=(0x0; 0x1f8))
>>>
>>> And kernel 5.15.0:
>>>
>>> BPF: 799: (bf) r4 = r6
>>> BPF: 800: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
>>> BPF: 800: (07) r4 += 7
>>> BPF: 801: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umin_value=7,umax_value=262,var_off=(0x0; 0x1ff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
>>> BPF: 801: (57) r4 &= -8
>>> BPF: 802: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umax_value=262,var_off=(0x0; 0x1f8)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
>>>
>>> This code is supposed to round the value in %r4 up to the nearest multiple of
>>> 8.  So, if %r4 is 255, one would expect this to yield 256.  Yet, it does not.
>>>