On Fri, 2025-07-25 at 21:08 +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
> commit 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>
> ---
Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx>
[...]
> +/* This test covers the bounds deduction on 64bits when the s64 and u64 ranges
> + * overlap on the positive side. At instruction 3, the ranges look as follows:
> + *
> + * 0 umin=0 umax=0xfffffffffffffeff U64_MAX
Nit: when I insert prints on master the umax is 0xffffffffffffff00,
which makes sense, as for the false branch the bound for r0
would be deduced from r0 <= r1 with r1 == 0xffffffffffffff00.
> + * [xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] |
> + * |----------------------------|------------------------------|
> + * |xxxxxxxx] [xxxxxxxx|
> + * 0 smax=127 smin=-128 -1
> + *
> + * We should therefore deduce the following new bounds:
> + *
> + * 0 u64=[0;127] U64_MAX
> + * [xxxxxxxx] |
> + * |----------------------------|------------------------------|
> + * [xxxxxxxx] |
> + * 0 s64=[0;127] -1
> + *
> + * Without the deduction cross sign boundary, the program is rejected due to
> + * the frame pointer write.
> + */
> +SEC("socket")
> +__description("bounds deduction cross sign boundary, positive overlap")
> +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> +__msg("3: (2d) if r0 > r1 {{.*}} R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=127,var_off=(0x0; 0x7f))")
> +__retval(0)
> +__naked void bounds_deduct_positive_overlap(void)
> +{
> + asm volatile(" \
> + call %[bpf_get_prandom_u32]; \
> + r0 = (s8)r0; \
> + r1 = 0xffffffffffffff00; \
> + if r0 > r1 goto l0_%=; \
> + if r0 < 128 goto l0_%=; \
> + r10 = 0; \
> +l0_%=: r0 = 0; \
> + exit; \
> +" :
> + : __imm(bpf_get_prandom_u32)
> + : __clobber_all);
> +}
[...]
