bpf: Improve 64bits bounds refinement #9330
Open
+82
−1
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
![kernel-patches-daemon-bpf[bot]](https://avatars.githubusercontent.com/u/70728002?s=60&v=4){kind=small}
|
Upstream branch: 42be23e |
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
ffefc6d to
4ccf98a
Compare
|
Upstream branch: 42be23e |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/983995=>bpf-next
branch
from
f462831 to
17bf332
Compare
|
Upstream branch: 42be23e |
kernel-patches-daemon-bpf
bot
force-pushed
the
series/983995=>bpf-next
branch
from
17bf332 to
7b247c6
Compare
kernel-patches-daemon-bpf
bot
force-pushed
the
bpf-next_base
branch
from
4ccf98a to
95edab2
Compare
|
Upstream branch: 95993dc |
__reg64_deduce_bounds currently improves the s64 range using the u64
range and vice versa, but only if it doesn't cross the sign boundary.
This patch improves __reg64_deduce_bounds to cover the case where the
s64 range crosses the sign boundary but overlaps with the u64 range on
only one end. In that case, we can improve both ranges. Consider the
following example, with the s64 range crossing the sign boundary:
0 U64_MAX
| [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx] |
|----------------------------|----------------------------|
|xxxxx s64 range xxxxxxxxx] [xxxxxxx|
0 S64_MAX S64_MIN -1
The u64 range overlaps only with positive portion of the s64 range. We
can thus derive the following new s64 and u64 ranges.
0 U64_MAX
| [xxxxxx u64 range xxxxx] |
|----------------------------|----------------------------|
| [xxxxxx s64 range xxxxx] |
0 S64_MAX S64_MIN -1
The same logic can probably apply to the s32/u32 ranges, but this patch
doesn't implement that change.
In addition to the selftests, this change was also tested with Agni,
the formal verification tool for the range analysis [1].
Link: https://github.com/bpfverif/agni [1]
Signed-off-by: Paul Chaignon <[email protected]>
Acked-by: Eduard Zingerman <[email protected]>
This patch updates the range refinement logic in the reg_bound test to match the new logic from the previous commit. Without this change, tests would fail because we end with more precise ranges than the tests expect. Signed-off-by: Paul Chaignon <[email protected]> Acked-by: Eduard Zingerman <[email protected]>
This test is a simplified version of a BPF program generated by syzkaller that caused an invariant violation [1]. It looks like syzkaller could not extract the reproducer itself (and therefore didn't report it to the mailing list), but I was able to extract it from the console logs of a crash. 0: call bpf_get_prandom_u32#7 ; R0_w=scalar() 1: w3 = w0 ; R3_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff)) 2: w6 = (s8)w0 ; R6_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) 3: r0 = (s8)r0 ; R0_w=scalar(smin=smin32=-128,smax=smax32=127) 4: if w6 >= 0xf0000000 goto pc+4 ; R6_w=scalar(smin=0,smax=umax=umax32=0xefffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff)) 5: r0 += r6 ; R0_w=scalar(smin=-128,smax=0xf000007e,smin32=-256,smax32=254) 6: r6 += 400 ; R6_w=scalar(smin=umin=smin32=umin32=400,smax=umax=smax32=umax32=527,var_off=(0x0; 0x3ff)) 7: r0 -= r6 ; R0=scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1,umax=0xffffffffffffff6e,smin32=-783,smax32=-146,umax32=0xffffff6e,var_off=(0xfffffc00; 0xffffffff000003ff)) 8: if r3 < r0 goto pc+0 REG INVARIANTS VIOLATION (false_reg2): range bounds violation u64=[0xfffffcf1, 0xffffff6e] s64=[0xfffffcf1, 0xeffffeee] u32=[0xfffffcf1, 0xffffff6e] s32=[0xfffffcf1, 0xffffff6e] var_off=(0xfffffc00, 0x3ff) The principle is similar to the invariant violation described in 6279846 ("bpf: Forget ranges when refining tnum after JSET"): the verifier walks a dead branch, uses the condition to refine ranges, and ends up with inconsistent ranges. In this case, the dead branch is when we fallthrough on both jumps. At the second fallthrough, the verifier concludes that R0's umax is bounded by R3's umax so R0_u64=[0xfffffcf1; 0xffffffff]. That refinement allows __reg64_deduce_bounds to further refine R0's smin value to 0xfffffcf1. It ends up with R0_s64=[0xfffffcf1; 0xeffffeee], which doesn't make any sense. The first patch in this series ("bpf: Improve bounds when s64 crosses sign boundary") fixes this by refining ranges before we reach the condition, such that the verifier can detect the jump is always taken. Indeed, at instruction 7, the ranges look as follows: 0 umin=0xfffffcf1 umax=0xff..ff6e U64_MAX | [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] | |----------------------------|------------------------------| |xxxxxxxxxx] [xxxxxxxxxxxx| 0 smax=0xeffffeee smin=-655 -1 The updated __reg64_deduce_bounds can therefore improve the ranges to s64=[-655; -146] (and the u64 equivalent). With this new range, it's clear that the condition at instruction 8 is always true: R3's umax is 0xffffffff and R0's umin is 0xfffffffffffffd71 ((u64)-655). We avoid the dead branch and don't end up with an invariant violation. Link: https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf [1] Signed-off-by: Paul Chaignon <[email protected]>
The improvement of the u64/s64 range refinement fixed the invariant violation that was happening on this test for BPF_JSLT when crossing the sign boundary. After this patch, we have one test remaining with a known invariant violation. It's the same test as fixed here but for 32 bits ranges. Signed-off-by: Paul Chaignon <[email protected]>
kernel-patches-daemon-bpf
bot
force-pushed
the
series/983995=>bpf-next
branch
from
7b247c6 to
afacd98
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Pull request for series with
subject: bpf: Improve 64bits bounds refinement
version: 1
url: https://patchwork.kernel.org/project/netdevbpf/list/?series=983995