* Possible (long standing) issue in the BPF verifier?
@ 2024-04-28 1:35 Kris Van Hees
2024-04-29 16:42 ` Eugene Loh
0 siblings, 1 reply; 4+ messages in thread
From: Kris Van Hees @ 2024-04-28 1:35 UTC (permalink / raw)
To: dtrace, DTrace development list
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.
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Possible (long standing) issue in the BPF verifier?
2024-04-28 1:35 Possible (long standing) issue in the BPF verifier? Kris Van Hees
@ 2024-04-29 16:42 ` Eugene Loh
2024-04-29 17:22 ` Kris Van Hees
0 siblings, 1 reply; 4+ messages in thread
From: Eugene Loh @ 2024-04-29 16:42 UTC (permalink / raw)
To: Kris Van Hees, dtrace, DTrace development list
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.
>
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Possible (long standing) issue in the BPF verifier?
2024-04-29 16:42 ` Eugene Loh
@ 2024-04-29 17:22 ` Kris Van Hees
2024-04-29 18:14 ` Eugene Loh
0 siblings, 1 reply; 4+ messages in thread
From: Kris Van Hees @ 2024-04-29 17:22 UTC (permalink / raw)
To: Eugene Loh; +Cc: Kris Van Hees, dtrace, DTrace development list
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.
> >
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Possible (long standing) issue in the BPF verifier?
2024-04-29 17:22 ` Kris Van Hees
@ 2024-04-29 18:14 ` Eugene Loh
0 siblings, 0 replies; 4+ messages in thread
From: Eugene Loh @ 2024-04-29 18:14 UTC (permalink / raw)
To: dtrace; +Cc: DTrace development list
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.
>>>
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2024-04-29 18:14 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2024-04-28 1:35 Possible (long standing) issue in the BPF verifier? Kris Van Hees
2024-04-29 16:42 ` Eugene Loh
2024-04-29 17:22 ` Kris Van Hees
2024-04-29 18:14 ` Eugene Loh
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.