__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 --- kernel/bpf/verifier.c | 44 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index e2fcea860755..152b97a71f85 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -2523,6 +2523,50 @@ static void __reg64_deduce_bounds(struct bpf_reg_state *reg) if ((u64)reg->smin_value <= (u64)reg->smax_value) { reg->umin_value = max_t(u64, reg->smin_value, reg->umin_value); reg->umax_value = min_t(u64, reg->smax_value, reg->umax_value); + } else { + /* If the s64 range crosses the sign boundary, then it's split + * between the beginning and end of the U64 domain. In that + * case, we can derive new bounds if the u64 range overlaps + * with only one end of the s64 range. + * + * In the following example, the u64 range overlaps only with + * positive portion of the s64 range. + * + * 0 U64_MAX + * | [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx] | + * |----------------------------|----------------------------| + * |xxxxx s64 range xxxxxxxxx] [xxxxxxx| + * 0 S64_MAX S64_MIN -1 + * + * 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 + * + * If they overlap in two places, we can't derive anything + * because reg_state can't represent two ranges per numeric + * domain. + * + * 0 U64_MAX + * | [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx] | + * |----------------------------|----------------------------| + * |xxxxx s64 range xxxxxxxxx] [xxxxxxxxxx| + * 0 S64_MAX S64_MIN -1 + * + * The first condition below corresponds to the diagram above. + * The second condition considers the case where the u64 range + * overlaps with the negative porition of the s64 range. + */ + if (reg->umax_value < (u64)reg->smin_value) { + reg->smin_value = (s64)reg->umin_value; + reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value); + } else if ((u64)reg->smax_value < reg->umin_value) { + reg->smax_value = (s64)reg->umax_value; + reg->umin_value = max_t(u64, reg->umin_value, reg->smin_value); + } } } -- 2.43.0 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 --- .../testing/selftests/bpf/prog_tests/reg_bounds.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c index 39d42271cc46..e261b0e872db 100644 --- a/tools/testing/selftests/bpf/prog_tests/reg_bounds.c +++ b/tools/testing/selftests/bpf/prog_tests/reg_bounds.c @@ -465,6 +465,20 @@ static struct range range_refine(enum num_t x_t, struct range x, enum num_t y_t, return range_improve(x_t, x, x_swap); } + if (!t_is_32(x_t) && !t_is_32(y_t) && x_t != y_t) { + if (x_t == S64 && x.a > x.b) { + if (x.b < y.a && x.a <= y.b) + return range(x_t, x.a, y.b); + if (x.a > y.b && x.b >= y.a) + return range(x_t, y.a, x.b); + } else if (x_t == U64 && y.a > y.b) { + if (y.b < x.a && y.a <= x.b) + return range(x_t, y.a, x.b); + if (y.a > x.b && y.b >= x.a) + return range(x_t, x.a, y.b); + } + } + /* otherwise, plain range cast and intersection works */ return range_improve(x_t, x, y_cast); } -- 2.43.0 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 6279846b9b25 ("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 --- .../selftests/bpf/progs/verifier_bounds.c | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c index 63b533ca4933..d104d43ff911 100644 --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c @@ -1550,4 +1550,27 @@ l0_%=: r0 = 0; \ : __clobber_all); } +SEC("socket") +__description("bounds deduction sync cross sign boundary") +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS) +__retval(0) +__naked void test_invariants(void) +{ + asm volatile(" \ + call %[bpf_get_prandom_u32]; \ + w3 = w0; \ + w6 = (s8)w0; \ + r0 = (s8)r0; \ + if w6 >= 0xf0000000 goto l0_%=; \ + r0 += r6; \ + r6 += 400; \ + r0 -= r6; \ + if r3 < r0 goto l0_%=; \ +l0_%=: r0 = 0; \ + exit; \ +" : + : __imm(bpf_get_prandom_u32) + : __clobber_all); +} + char _license[] SEC("license") = "GPL"; -- 2.43.0 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 --- tools/testing/selftests/bpf/progs/verifier_bounds.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c index d104d43ff911..ddf36d8ab07a 100644 --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c @@ -1066,7 +1066,7 @@ l0_%=: r0 = 0; \ SEC("xdp") __description("bound check with JMP_JSLT for crossing 64-bit signed boundary") __success __retval(0) -__flag(!BPF_F_TEST_REG_INVARIANTS) /* known invariants violation */ +__flag(BPF_F_TEST_REG_INVARIANTS) __naked void crossing_64_bit_signed_boundary_2(void) { asm volatile (" \ -- 2.43.0