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

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

[Harishankar Vishwanathan]

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

[RFC PATCH 1/1] bpf, verifier: Introduce tnum_step to step through tnum's members

[Harishankar Vishwanathan]

This commit introduces tnum_step(), a function that, when given t, and a
number z returns the smallest member of t larger than z. The number z
must be greater or equal to the smallest member of t and less than the
largest member of t.

The first step is to compute j, a number that keeps all of t's known
bits, and matches all unknown bits to z's bits. Since j is a member of
the t, it is already a candidate for result. However, we want our result
to be (minimally) greater than z.

There are only two possible cases:

(1) Case j <= z. In this case, we want to increase the value of j and
make it > z.
(2) Case j > z. In this case, we want to decrease the value of j while
keeping it > z.

(Case 1) j <= z

t = xx11x0x0
z = 10111101 (189)
j = 10111000 (184)
         ^
         k

(Case 1.1) Let's first consider the case where j < z. We will address j
== z later.

Since z > j, there had to be a bit position that was 1 in z and a 0 in
j, beyond which all positions of higher significance are equal in j and
z. Further, this position could not have been unknown in a, because the
unknown positions of a match z. This position had to be a 1 in z and
known 0 in t.

Let k be position of the most significant 1-to-0 flip. In our example, k
= 3 (starting the count at 1 at the least significant bit).  Setting (to
1) the unknown bits of t in positions of significance smaller than
k will not produce a result > z. Hence, we must set/unset the unknown
bits at positions of significance higher than k. Specifically, we look
for the next larger combination of 1s and 0s to place in those
positions, relative to the combination that exists in z. We can achieve
this by concatenating bits at unknown positions of t into an integer,
adding 1, and writing the bits of that result back into the
corresponding bit positions previously extracted from z.

From our example, considering only positions of significance greater
than k:

t =  xx..x
z =  10..1
    +    1
     -----
     11..0

This is the exact combination 1s and 0s we need at the unknown bits of t
in positions of significance greater than k. Further, our result must
only increase the value minimally above z. Hence, unknown bits in
positions of significance smaller than k should remain 0. We finally
have,

result = 11110000 (240)

(Case 1.2) Now consider the case when j = z, for example

t = 1x1x0xxx
z = 10110100 (180)
j = 10110100 (180)

Matching the unknown bits of the t to the bits of z yielded exactly z.
To produce a number greater than z, we must set/unset the unknown bits
in t, and *all* the unknown bits of t candidates for being set/unset. We
can do this similar to Case 1.1, by adding 1 to the bits extracted from
the masked bit positions of z. Essentially, this case is equivalent to
Case 1.1, with k = 0.

t =  1x1x0xxx
z =  .0.1.100
    +       1
    ---------
     .0.1.101

This is the exact combination of bits needed in the unknown positions of
t. After recalling the known positions of t, we get

result = 10110101 (181)

(Case 2) j > z

t = x00010x1
z = 10000010 (130)
j = 10001011 (139)
	^
	k

Since j > z, there had to be a bit position which was 0 in z, and a 1 in
j, beyond which all positions of higher significance are equal in j and
z. This position had to be a 0 in z and known 1 in t. Let k be the
position of the most significant 0-to-1 flip. In our example, k = 4.

Because of the 0-to-1 flip at position k, a member of t can become
greater than z if the bits in positions greater than k are themselves >=
to z. To make that member *minimally* greater than z, the bits in
positions greater than k must be exactly = z. Hence, we simply match all
of t's unknown bits in positions more significant than k to z's bits. In
positions less significant than k, we set all t's unknonwn bits to 0
to retain minimality.

In our example, in positions of greater significance than k (=4),
t=x000. These positions are matched with z (1000) to produce 1000. In
positions of lower significance than k, t=10x1. All unknown bits are set
to 0 to produce 1001. The final result is:

result = 10001001 (137)

This concludes the computation for a result > z that is a member of t.

The procedure for tnum_step() in this commit implements the idea
described above. As a proof of correctness, we verified the algorithm
against a logical specification of tnum_step. The specification asserts
the following about the inputs t, z and output res that:

1. res is a member of t, and
2. res is strictly greater than z, and
3. there does not exist another value res2 such that
	3a. res2 is also a member of t, and
	3b. res2 is greater than z
	3c. res2 is smaller than res

We checked the implementation against this logical specification using
an SMT solver. The verification formula in SMTLIB format is available
at [1]. The verification returned an "unsat": indicating that no input
assignment exists for which the implementation and the specification
produce different outputs.

In addition, we also automatically generated the logical encoding of the
C implementation using Agni [2] and verified it against the same
specification. This verification also returned an "unsat", confirming
that the implementation is equivalent to the specification. The formula
for this check is also available at [3].

[1] https://pastebin.com/raw/2eRWbiit
[2] https://github.com/bpfverif/agni
[3] https://pastebin.com/raw/EztVbBJ2

Co-developed-by: Matan Shachnai <m.shachnai@gmail.com>
Signed-off-by: Matan Shachnai <m.shachnai@gmail.com>
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
---
 include/linux/tnum.h |  3 ++-
 kernel/bpf/tnum.c    | 52 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+), 1 deletion(-)

diff --git a/include/linux/tnum.h b/include/linux/tnum.h
index c52b862dad45..63987f442b4a 100644
--- a/include/linux/tnum.h
+++ b/include/linux/tnum.h
@@ -125,5 +125,6 @@ static inline bool tnum_subreg_is_const(struct tnum a)
 {
 	return !(tnum_subreg(a)).mask;
 }
-
+/* Returns the smallest member of t larger than z. */
+u64 tnum_step(struct tnum t, u64 z);
 #endif /* _LINUX_TNUM_H */
diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index f8e70e9c3998..5c12d7d9ba22 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -253,3 +253,55 @@ struct tnum tnum_const_subreg(struct tnum a, u32 value)
 {
 	return tnum_with_subreg(a, tnum_const(value));
 }
+
+/* Given tnum t, and a number z such that tmin <= z < tmax, where tmin
+ * is the smallest member of the t (= t.value) and tmax is the largest
+ * member of t (= t.value | t.mask) returns the smallest member of t
+ * larger than z.
+ *
+ * For example,
+ * t      = x11100x0
+ * z      = 11110001 (241)
+ * result = 11110010 (242)
+ *
+ * Note: if this function is called with z >= tmax, it just returns
+ * early with tmax; if this function is called with z < tmin, the
+ * algorithm already returns tmin.
+ */
+u64 tnum_step(struct tnum t, u64 z)
+{
+	u64 tmax, j, p, q, r, s, v, u, w, res;
+	u8 k;
+
+	tmax = t.value | t.mask;
+
+	/* if z >= largest member of t, return largest member of t */
+	if (z >= tmax)
+		return tmax;
+
+	/* keep t's known bits, and match all unknown bits to z */
+	j = t.value | z & t.mask;
+
+	if (j > z) {
+		p = ~z & t.value & ~t.mask;
+		k = fls64(p); /* k is the most-significant 0-to-1 flip */
+		q = U64_MAX << k;
+		r = q & z; /* positions > k matched to z */
+		s = ~q & t.value; /* positions <= k matched to t.value */
+		v = r | s;
+		res = v;
+	} else {
+		p = z & ~t.value & ~t.mask;
+		k = fls64(p); /* k is the most-significant 1-to-0 flip */
+		q = U64_MAX << k;
+		r = q & t.mask & z; /* unknown positions > k, matched to z */
+		s = q & ~t.mask; /* known positions > k, set to 1 */
+		v = r | s;
+		/* add 1 to unknown positions > k to make value greater than z */
+		u = v + (1ULL << k);
+		/* extract bits in unknown positions > k from u, rest from t.value */
+		w = u & t.mask | t.value;
+		res = w;
+	}
+	return res;
+}
-- 
2.45.2

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

[Paul Chaignon]

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.

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

[...]

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

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

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@gmail.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
> >