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