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

[Harishankar Vishwanathan]

On Thu, Nov 13, 2025 at 12:17 PM Paul Chaignon <paul.chaignon@xxxxxxxxx> 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@xxxxxxxxxxxxxx/
> > [2] https://lore.kernel.org/bpf/75b3af3d315d60c1c5bfc8e3929ac69bb57d5cea.1752099022.git.paul.chaignon@xxxxxxxxx/
> > [3] https://lore.kernel.org/bpf/CACkBjsZen6AA1jXqgmA=uoZZJt5bLu+7Hz3nx3BrvLAP=CqGuA@xxxxxxxxxxxxxx/T/#e6604e4092656b192cf617c98f9a00b16c67aad87
> > [4] https://lore.kernel.org/bpf/aPJZs5h7ihqOb-e6@xxxxxxxxxxxxxx/
> > [5] https://lore.kernel.org/bpf/CAEf4BzY_f=iNKC2CVz-myfe_OERN9XWHiuNG6vng43-MXUAvSw@xxxxxxxxxxxxxx/
> >
> > 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
> >