Possible (long standing) issue in the BPF verifier?

DISCUSSION Kris Van Hees 2 participants 4 messages Apr 28, 2024 – Apr 29, 2024

Share & tools

Kris Van Hees

author

2024-04-28 01:35 UTC #0 lore raw

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.

Eugene Loh

2024-04-29 16:42 UTC #1 lore raw

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?

Quoted 26 lines · 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.

Kris Van Hees

author

2024-04-29 17:22 UTC #2 lore raw

Quoted 8 lines · 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.

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

Quoted 4 lines

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.

Quoted 27 lines · Kris Van Hees

Quoted 26 lines
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.

Eugene Loh

2024-04-29 18:14 UTC #3 lore raw

Quoted 11 lines · Kris Van Hees

Quoted 8 lines · 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.
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].

Quoted 14 lines

Quoted 4 lines
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.

Quoted 1 line

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?

Quoted 27 lines

Quoted 27 lines · Kris Van Hees
Quoted 26 lines
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.