linux-kernel - Re: [RFC PATCH 0/1] bpf, verifier: Detect empty intersection between tnum and ranges

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [day] [month] [year] [list]

Message-ID: <CAM=Ch07axjOfx4Ar01gdx7CGi5A5+mzqmCu6DNVMEOjk4BJ_iw@mail.gmail.com>
Date: Thu, 13 Nov 2025 18:16:28 -0500
From: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
To: Paul Chaignon <paul.chaignon@...il.com>
Cc: ast@...nel.org, m.shachnai@...gers.edu, srinivas.narayana@...gers.edu, 
	santosh.nagarakatte@...gers.edu, Daniel Borkmann <daniel@...earbox.net>, 
	John Fastabend <john.fastabend@...il.com>, Andrii Nakryiko <andrii@...nel.org>, 
	Martin KaFai Lau <martin.lau@...ux.dev>, Eduard Zingerman <eddyz87@...il.com>, Song Liu <song@...nel.org>, 
	Yonghong Song <yonghong.song@...ux.dev>, KP Singh <kpsingh@...nel.org>, 
	Stanislav Fomichev <sdf@...ichev.me>, Hao Luo <haoluo@...gle.com>, Jiri Olsa <jolsa@...nel.org>, 
	bpf@...r.kernel.org, linux-kernel@...r.kernel.org
Subject: Re: [RFC PATCH 0/1] bpf, verifier: Detect empty intersection between
 tnum and ranges

On Thu, Nov 13, 2025 at 12:17 PM Paul Chaignon <paul.chaignon@...il.com> wrote:
>
> On Fri, Nov 07, 2025 at 02:23:27PM -0500, Harishankar Vishwanathan wrote:
> > This RFC introduces an algorithm called tnum_step that can be used to
> > detect when a tnum and the range have an empty intersection. This can
> > help the verifier avoid walking dead branches that lead to range
> > invariant violations. I am sending this as a patchset to keep the
> > motivation (this email) separate from the details of algorithm
> > (following email).
> >
> > Several fuzzing campaigns have reported programs that trigger "REG
> > INVARIANTS VIOLATION" errors in the verifier [1, 2, 3, 4]. These
> > invariant violations happen when the verifier refines register bounds in
> > a branch that is actually dead. When reg_bounds_sync() attempts to
> > update the tnum and the range in such a dead branch, it can produce
> > inconsistent ranges, for example, a register state with umin > umax or
> > var_off values incompatible with the range bounds.
>
> I think an open question here is whether such patterns of tnum/ranges
> happen in practice, outside of syzkaller. We probably don't want to
> introduce additional logic for something that doesn't help "real"
> programs. I'm happy to check the impact on Cilium for example, but that
> would require a patch to actually start using the new tnum helper.
>

Fair point. But I wanted to highlight the completeness of this approach,
in addition to the soundness. The check:

    if (tmin > umax || tmax < umin || tnum_step(t, umin) > umax)

detects *all* possible cases of "no intersection" betweeen tnums and u64
ranges. If future updates to the regs_refine_cond_op() logic take the
tnum and ranges to any incompatible case, this check will detect them.

[...]
> > * Usage in the verifier and next steps
> >
> > The tnum_step() procedure is self-contained and can be incorporated
> > as-is.
> >
> > Regarding incorporating the range-tnum intersection test, as it
> > stands, if is_branch_taken() cannot determine that a branch is dead,
> > reg_set_min_max()->regs_refine_cond_op() are called to update the
> > register bounds.
> >
> > We can incorporate the range-tnum intersection test after the calls to
> > regs_refine_cond_op() or the calls to reg_bounds_sync(). If there is no
> > intersection between the ranges and the tnum, we are on a dead branch.
>
> Couldn't we incorporate such a test in is_branch_taken() today?

The idea behind suggesting the test in reg_set_min_max() and not
is_branch_taken() was that the empty intersection typically happens
after the call to reg_bounds_sync(), which updates the bounds so that
tnums and ranges become incompatible.

At this point however, the verifier has already forked new
bpf_verifier_states (via push_stack()). Once we detect an impossible
branch using the new check, we will need to clean up the states
corresponding to the impossible branch.

I was hoping for some comments on whether this approach is
feasible.

> >
> > Alternatively, the range-tnum intersection check could be incorporated
> > as part of Eduard's upcoming patchset, which is expected to rework the
> > logic in reg_set_min_max() and is_branch_taken().
> >
> > Looking forward to hearing any feedback and suggestions.
> >
> > [1] https://lore.kernel.org/bpf/aKWytdZ8mRegBE0H@mail.gmail.com/
> > [2] https://lore.kernel.org/bpf/75b3af3d315d60c1c5bfc8e3929ac69bb57d5cea.1752099022.git.paul.chaignon@gmail.com/
> > [3] https://lore.kernel.org/bpf/CACkBjsZen6AA1jXqgmA=uoZZJt5bLu+7Hz3nx3BrvLAP=CqGuA@mail.gmail.com/T/#e6604e4092656b192cf617c98f9a00b16c67aad87
> > [4] https://lore.kernel.org/bpf/aPJZs5h7ihqOb-e6@mail.gmail.com/
> > [5] https://lore.kernel.org/bpf/CAEf4BzY_f=iNKC2CVz-myfe_OERN9XWHiuNG6vng43-MXUAvSw@mail.gmail.com/
> >
> > Harishankar Vishwanathan (1):
> >   bpf, verifier: Introduce tnum_step to step through tnum's members
> >
> >  include/linux/tnum.h |  3 ++-
> >  kernel/bpf/tnum.c    | 52 ++++++++++++++++++++++++++++++++++++++++++++
> >  2 files changed, 54 insertions(+), 1 deletion(-)
> >
> > --
> > 2.45.2
> >