Re: [syzbot] [bpf?] WARNING in reg_bounds_sanity_check

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2025-07-03 at 19:02 +0200, Paul Chaignon wrote:
> On Tue, Jul 01, 2025 at 06:55:28PM -0700, syzbot wrote:
> > Hello,
> >
> > syzbot found the following issue on:
> >
> > HEAD commit:    cce3fee729ee selftests/bpf: Enable dynptr/test_probe_read_..
> > git tree:       bpf-next
> > console+strace: https://syzkaller.appspot.com/x/log.txt?x=147793d4580000
> > kernel config:  https://syzkaller.appspot.com/x/.config?x=79da270cec5ffd65
> > dashboard link: https://syzkaller.appspot.com/bug?extid=c711ce17dd78e5d4fdcf
> > compiler:       Debian clang version 20.1.6 (++20250514063057+1e4d39e07757-1~exp1~20250514183223.118), Debian LLD 20.1.6
> > syz repro:      https://syzkaller.appspot.com/x/repro.syz?x=1594e48c580000
> > C reproducer:   https://syzkaller.appspot.com/x/repro.c?x=1159388c580000
> >
> > Downloadable assets:
> > disk image: https://storage.googleapis.com/syzbot-assets/f286a7ef4940/disk-cce3fee7.raw.xz
> > vmlinux: https://storage.googleapis.com/syzbot-assets/e2f2ebe1fdc3/vmlinux-cce3fee7.xz
> > kernel image: https://storage.googleapis.com/syzbot-assets/6e3070663778/bzImage-cce3fee7.xz
> >
> > IMPORTANT: if you fix the issue, please add the following tag to the commit:
> > Reported-by: syzbot+c711ce17dd78e5d4fdcf@syzkaller.appspotmail.com
> >
> > ------------[ cut here ]------------
> > verifier bug: REG INVARIANTS VIOLATION (false_reg1): range bounds violation u64=[0x0, 0x0] s64=[0x0, 0x0] u32=[0x1, 0x0] s32=[0x0, 0x0] var_off=(0x0, 0x0)(1)
> > WARNING: CPU: 1 PID: 5833 at kernel/bpf/verifier.c:2688 reg_bounds_sanity_check+0x6e6/0xc20 kernel/bpf/verifier.c:2682
>
> I'm unsure how to handle this one.
>
> One example repro is as follows.
>
>   0: call bpf_get_netns_cookie
>   1: if r0 == 0 goto <exit>
>   2: if r0 & Oxffffffff goto <exit>
>
> The issue is on the path where we fall through both jumps.
>
> That path is unreachable at runtime: after insn 1, we know r0 != 0, but
> with the sign extension on the jset, we would only fallthrough insn 2
> if r0 == 0. Unfortunately, is_branch_taken() isn't currently able to
> figure this out, so the verifier walks all branches. As a result, we end
> up with inconsistent register ranges on this unreachable path:
>
>   0: if r0 == 0 goto <exit>
>     r0: u64=[0x1, 0xffffffffffffffff] var_off=(0, 0xffffffffffffffff)
>   1: if r0 & 0xffffffff goto <exit>
>     r0 before reg_bounds_sync: u64=[0x1, 0xffffffffffffffff] var_off=(0, 0)
>     r0 after reg_bounds_sync:  u64=[0x1, 0] var_off=(0, 0)
>
> I suspect there isn't anything specific to these two conditions, and
> anytime we start walking an unreachable path, we may end up with
> inconsistent register ranges. The number of times syzkaller is currently
> hitting this (180 in 1.5 days) suggests there are many different ways to
> reproduce.
>
> We could teach is_branch_taken() about this case, but we probably won't
> be able to cover all cases. We could stop warning on this, but then we
> may also miss legitimate cases (i.e., invariants violations on reachable
> paths). We could also teach reg_bounds_sync() to stop refining the
> bounds before it gets inconsistent, but I'm unsure how useful that'd be.

Hi Paul,

In general, I think that reg_bounds_sync() can be used as a substitute
for is_branch_taken() -> whenever an impossible range is produced,
the branch should be deemed impossible at runtime and abandoned.
If I recall correctly Andrii considered this too risky some time ago,
so this warning is in place to catch bugs.

Which leaves only the option to refine is_branch_taken().

I think is_branch_taken() modification should not be too complicated.
For JSET it only checks tnum, but does not take ranges into account.
Reasoning about ranges is something along the lines:
- for unsigned range a = b & CONST -> a is in [b_min & CONST, b_max & CONST];
- for signed ranged same thing, but consider two unsigned sub-ranges;
- for non CONST cases, I think same reasoning can apply, but more
  min/max combinations need to be explored.
- then check if zero is a member or 'a' range.

Wdyt?

> The number of times syzkaller is currently hitting this (180 in 1.5
> days) suggests there are many different ways to reproduce.

It is a bit inconvenient to read syzbot BPF reports at the moment,
because it us hard to figure out how the program looks like.
Do you happen to know how complicated would it be to modify syzbot
output to:
- produce a comment with BPF program
- generating reproducer with a flag, allowing to print level 2
  verifier log
?

Thanks,
Eduard