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

[Kris Van Hees <kris.van.hees@oracle.com>]

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.
> >