Message-ID: <20251107192328.2190680-1-harishankar.vishwanathan@gmail.com>
Date: Fri,  7 Nov 2025 14:23:27 -0500
From: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
To: ast@...nel.org
Cc: m.shachnai@...gers.edu,
	srinivas.narayana@...gers.edu,
	santosh.nagarakatte@...gers.edu,
	paul.chaignon@...il.com,
	Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>,
	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: [RFC PATCH 0/1] bpf, verifier: Detect empty intersection between tnum and ranges

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.

There is a solution is in the works by Eduard [5] to modify verifier's
logic to use the fact that the register's tnum and range bounds are
incompatible to detect that a branch cannot be taken. Detecting an empty
intersection between the range and the tnum could be a useful primitive
to detect incompatiblity.

* Detecting Empty Intersections

Consider a range r [umin, umax] and a tnum t (tval, tmask). A simple way
to check if the range and the tnum intersect is to compare their
bounds:

	tmin = tval
	tmax = tval | tmask

	if (tmin > umax || tmax < umin)
		return -1;  // no intersection

However, this approach fails when the tnum represents a non-contiguous
set of values, and the range lies entirely "in-between". For example:

	t = x0x1	{1, 3, 9, 11}
	r = [4, 8]	{4, 5, 6, 7, 8}

Here, tmin <= umax && tmax >= umin, yet the two sets have no
intersection.

To implement set intersection for tnum and ranges, it would be useful to
have the ability to walk through the values in the tnum. If the next
valid tnum value after umin already jumps past umax, then there is no
value of t in [umin, umax]. In other words, we need a "step" function
for tnums that can determine the next numerically larger concrete value
that is contained in the tnum's set.

* The tnum_step() primitive

To correctly detect these cases, we introduce a new helper:

    u64 tnum_step(struct tnum t, u64 z);

This function returns the smallest number greater than z that is
representable by the tnum t. Using tnum_step(), intersection detection
can be implemented as:

	if (tmin > umax || tmax < umin)
		return -1;  // no intersection

	/* next valid tnum value after umin already jumps past umax,
	* implying there's no value of t in [umin, umax].
	*/
	if (tnum_step(t, umin) > umax)
		return -1;  // no intersection

	return 1;  // intersection exists

* A sound and complete procedure that runs in constant time

At first glance, one might expect that computing tnum_step() would
require iterating over the individual bits of t and z. However, the
procedure for tnum_step(), introduced in the next patch, derives the
next tnum value greater than z purely through bitwise operations, and
thus runs in constant time.

Importantly, using the tnum_step() primitive we can construct a
range-tnum intersection test (as shown) that is both *sound and
complete*: it never reports "no intersection" when there is one, and
does not miss any cases of "no intersection".

* 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.

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

Powered by blists - more mailing lists