On Thu, 2025-07-24 at 15:43 +0200, Paul Chaignon wrote:
> This patch adds coverage for the new cross-sign 64bits range refinement
> logic. The three tests cover the cases when the u64 and s64 ranges
> overlap (1) in the negative portion of s64, (2) in the positive portion
> of s64, and (3) in both portions.
>
> The first 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.
>
> 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. The new refinement logic improves the
> bounds such that the second jump is properly detected as always-taken
> and the verifier doesn't end up walking a dead branch.
>
> The second and third tests are inspired by the first, but rely on
> condition jumps to prepare the bounds instead of ALU instructions. An
> R10 write is used to trigger a verifier error when the bounds can't be
> refined.
>
> Link: https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf [1]
> Signed-off-by: Paul Chaignon <paul.chaignon@xxxxxxxxx>
> ---
Hi Paul,
Thank you for adding the tests, I think the patch looks good.
> .../selftests/bpf/progs/verifier_bounds.c | 118 ++++++++++++++++++
> 1 file changed, 118 insertions(+)
>
> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> index 63b533ca4933..dd4e3e9f41d3 100644
> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
> @@ -1550,4 +1550,122 @@ l0_%=: r0 = 0; \
> : __clobber_all);
> }
>
> +/* This test covers the bounds deduction on 64bits when the s64 and u64 ranges
> + * overlap on the negative side. 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
> + *
> + * We should therefore deduce the following new bounds:
> + *
> + * 0 u64=[0xff..ffd71;0xff..ff6e] U64_MAX
> + * | [xxx] |
> + * |----------------------------|------------------------------|
> + * | [xxx] |
> + * 0 s64=[-655;-146] -1
> + *
> + * Without the deduction cross sign boundary, we end up with an invariant
> + * violation error.
> + */
> +SEC("socket")
> +__description("bounds deduction cross sign boundary, negative overlap")
> +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")
Interesting, note the difference: smin=-655, smin32=-783.
There is a code to infer s32 range from s46 range in this situation in
__reg32_deduce_bounds(), but it looks like a third __reg_deduce_bounds
call is needed to trigger it. E.g. the following patch removes the
difference for me:
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index f0a41f1596b6..87050d17baf9 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2686,6 +2686,7 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
/* We might have learned something about the sign bit. */
__reg_deduce_bounds(reg);
__reg_deduce_bounds(reg);
+ __reg_deduce_bounds(reg);
/* We might have learned some bits from the bounds. */
__reg_bound_offset(reg);
/* Intersecting with the old var_off might have improved our bounds
> +__retval(0)
> +__naked void bounds_deduct_negative_overlap(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);
> +}
[...]
