Re: [PATCH bpf-next 1/2] bpf/verifier: Use intersection checks when simulating to detect dead branches

[Paul Chaignon <paul.chaignon@gmail.com>]

On Wed, Apr 15, 2026 at 12:07:27PM -0400, Harishankar Vishwanathan wrote:
> This commit introduces checks to detect if the ranges and/or tnums have
> intersections between them, and uses the checks in
> simulate_both_branches_taken and reg_bounds_sync.
> 
> The verifier is known to evolve the reg_states correctly (i.e. soundly)
> on a live branch. In a previous commit [1], we used the ill-formedness
> of a range (e.g. umin > umax), identified by range_bounds_violation, to
> detect dead branches and prune the branch along which the ill-formedness
> occurs.
> 
> Another opportunity to prune branches is when the ranges and/or tnums
> have don't intersect. When the verifier evolves the reg_state along a
> dead branch, it is possible that abstract value in one domain (e.g tnum)
> doesn't match with the abstract value in the other domain (e.g. u64), so
> that there is no single value x, that is contained in both the abstract
> values.
> 
> First, we introduce intersection checks for each of the 5 domains (for a
> total of 10 domain pairs), and wrap it in reg_bounds_intersect.
> 
> Next, in simulate_both_branches_taken, we use reg_bounds_intersect
> instead of the existing range_bounds_violation to detect dead branches.
> Because the new check in reg_bounds_intersect also checks for
> range_bounds_violation, we are strictly increasing the detection of dead
> branches when using the new check.
> 
> Finally, this commit also replaces the early exit in reg_bounds_sync. In
> an older commit [2] we detected invalid inputs to reg_bounds_sync using
> range_bounds_violation, i.e. checking for ill-formed ranges (e.g. umin >
> umax), and exited early. If the inputs to reg_bounds_sync do not have
> any intersection, they are also invalid. This way, we ensure that
> subsequent operations in reg_bounds_sync don't inadvertently "fix" the
> reg_state to become valid. This is important for example, when we
> simulate_both_branches_taken; the call to reg_bounds_sync won't fix the
> reg_state bounds, so we can still detect dead branches using
> reg_bounds_intersect.
> 
> As a proof of correctness, for each domain pair, we individually
> verified the C implementation against a logical specification. For each
> pair, we used Agni [3] to encode the C implementation in logic. The
> logical specification for a given pair asserts that an intersection
> exists if and only if there is at least one concrete integer value that
> is simultaneously a valid member of both abstract domains. All 10
> verifications returned an "unsat", confirming the C implementation is
> equivalent to the specification.
> 
> [1] commit b254c6d816e5 ("bpf: Simulate branches to prune based on range violations")
> [2] commit a2a14e874b4e ("bpf: Exit early if reg_bounds_sync gets invalid inputs")
> [3] https://github.com/bpfverif/agni
> 
> 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>

I tested this with the Cilium complexity test suite [1]. I wanted to
check the impact on the verification time so I ran it on my host (no VM)
and disabled parallelism.

First, there is almost no impact on the number of instructions processed
(< 13 insns). That makes sense since reports of invariant violations
have been rare in Cilium. Now, the impact on the verification time also
seems null. Even running on the host, there are a few outliers, but the
mean difference is consistently reported to be null.

Considering that and the consistent veristat results:

Tested-by: Paul Chaignon <paul.chaignon@gmail.com>
Acked-by: Paul Chaignon <paul.chaignon@gmail.com>

1: https://pchaigno.github.io/test-verifier-complexity.html

> ---
>  kernel/bpf/verifier.c | 224 +++++++++++++++++++++++++++++++++++++++++-
>  1 file changed, 219 insertions(+), 5 deletions(-)
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 9e4980128151..3f0d24ed2acc 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2345,12 +2345,15 @@ static void __reg_bound_offset(struct bpf_reg_state *reg)
>  	reg->var_off = tnum_or(tnum_clear_subreg(var64_off), var32_off);
>  }
>  
> -static bool range_bounds_violation(struct bpf_reg_state *reg);
> +static bool reg_bounds_intersect(struct bpf_reg_state *reg);
>  
>  static void reg_bounds_sync(struct bpf_reg_state *reg)
>  {
> -	/* If the input reg_state is invalid, we can exit early */
> -	if (range_bounds_violation(reg))
> +	/* If the input reg_state has no intersection between abstract values, it is
> +	 * invalid. We can exit early, ensuring that subsequent operations don't
> +	 * inadvertently fix the reg_state.
> +	 */
> +	if (!reg_bounds_intersect(reg))
>  		return;
>  	/* We might have learned new bounds from the var_off. */
>  	__update_reg_bounds(reg);
> @@ -2397,6 +2400,217 @@ static bool const_tnum_range_mismatch_32(struct bpf_reg_state *reg)
>  	       reg->s32_min_value != sval32 || reg->s32_max_value != sval32;
>  }
>  
> +/*
> + * Check if a reg_state's bounds in all domains (u64, s64, u32, s32, tnum)
> + * intersect. This ensures that for every pair of abstract values, there is
> + * *at least one* value x, such that x is a member of both abstract values.
> + * If there is no intersection between *any* pair of abstract values (10 pairs
> + * from the five domains), return false. Otherwise, return true.
> + */
> +static bool reg_bounds_intersect(struct bpf_reg_state *reg)
> +{
> +	u64 umin = reg->umin_value, umax = reg->umax_value;
> +	s64 smin = reg->smin_value, smax = reg->smax_value;
> +	u32 u32_min = reg->u32_min_value, u32_max = reg->u32_max_value;
> +	s32 s32_min = reg->s32_min_value, s32_max = reg->s32_max_value;
> +	struct tnum t = reg->var_off;
> +	struct tnum t32 = tnum_subreg(t);
> +	u64 tmin = t.value, tmax = t.value | t.mask;
> +	u32 t32_min = t32.value, t32_max = t32.value | t32.mask;
> +
> +	/*
> +	 * If the min > max, then the range itself is ill-formed, so there can be no
> +	 * intersection in abstract values across domains.
> +	 */
> +	if (range_bounds_violation(reg))
> +		return false;
> +
> +	/*
> +	 * If the var_off is ill-formed, there can be no intersection in abstract
> +	 * values across domains.
> +	 */
> +	if ((t.value & t.mask) != 0)
> +		return false;
> +
> +	/*
> +	 * Intersect u64 with s64. We map the s64 range to u64 domain and check if
> +	 * there is an intersection. If s64 range does not cross the sign boundary,
> +	 * then we can treat it as a u64 range and check if its bounding values are
> +	 * outside the u64 range. If s64 range crosses the sign boundary, then it
> +	 * spans the u64 intervals [0, smax] and [smin, U64_MAX]. Intersection
> +	 * exists if the u64 range overlaps either of these components, which is
> +	 * equivalent to checking that the u64 range is not trapped between
> +	 * (u64)smax and (u64)smin.
> +	 */
> +	if ((u64)smin <= (u64)smax) { /* s64 does not cross the sign boundary */
> +		if ((u64)smax < umin || umax < (u64)smin)
> +			return false;
> +	} else { /* s64 crosses the sign boundary */
> +		if ((u64)smin > umax && (u64)smax < umin)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u32 with s32. This case is similar to u64-s64, but we map
> +	 * the s32 range to the u32 domain.
> +	 */
> +	if ((u32)s32_min <= (u32)s32_max) {
> +		if ((u32)s32_max < u32_min || u32_max < (u32)s32_min)
> +			return false;
> +	} else {
> +		if ((u32)s32_min > u32_max && (u32)s32_max < u32_min)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u64 with tnum. When we map the tnum to the u64 domain, the
> +	 * bounding values of tnum might be outside the bounding values of u64.
> +	 * In this case, there is no intersection. For example:
> +	 *
> +	 * u64:  --[xxxxxx]--------------
> +	 * tnum: -----------xx-x-x----x--
> +	 *               tmin         tmax
> +	 *
> +	 * However, it is also possible that the tnum "jumps over" the
> +	 * u64, making the u64 range lie entirely "in-between" the tnum, and
> +	 * in this case as well, there is no intersection. For example:
> +	 *
> +	 * u64:  ----[xxxxxx]------
> +	 * tnum: -x-----------x----
> +	 *      tmin         tmax
> +	 *
> +	 * We can check for intersection by checking if the next tnum value after
> +	 * umin is beyond umax. If it is, there is no intersection.
> +	 */
> +	if (tmax < umin || tmin > umax)
> +		return false;
> +	if (t.value != (umin & ~t.mask)) {
> +		if (tnum_step(t, umin) > umax)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u32 with tnum. This case is similar to u64-tnum, but we map
> +	 * the tnum to the u32 domain.
> +	 */
> +	if (t32_max < u32_min || t32_min > u32_max)
> +		return false;
> +	if (t32.value != (u32_min & ~t32.mask)) {
> +		if (tnum_step(t32, u32_min) > u32_max)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect s64 with tnum. Similar to u64-tnum, but we map s64 and tnum to
> +	 * the u64 domain. If s64 range does not cross the sign boundary, we can
> +	 * treat it as a normal u64 range and check intersection with the tnum as
> +	 * above. If s64 range crosses the sign boundary, it spans the u64 intervals
> +	 * [0, smax] and [smin, U64_MAX]. Intersection exists if the tnum overlaps
> +	 * either of these components. The tnum cannot "jump over" either of these
> +	 * two intervals, because they contain endpoints 0 and U64_MAX respectively.
> +	 * So it is sufficient to check if the bounding values of tnum are outside
> +	 * the bounding values of the mapped s64.
> +	 */
> +	if ((u64)smin <= (u64)smax) { /* s64 does not cross sign boundary */
> +		if (tmax < (u64)smin || tmin > (u64)smax)
> +			return false;
> +		if (t.value != ((u64)smin & ~t.mask)) {
> +			if (tnum_step(t, (u64)smin) > (u64)smax)
> +				return false;
> +		}
> +	} else { /* s64 crosses sign boundary */
> +		if (tmin > (u64)smax && tmax < (u64)smin)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect s32 with tnum. This case is similar to s64-tnum, but we map
> +	 * s32 and tnum to the u32 domain.
> +	 */
> +	if ((u32)s32_min <= (u32)s32_max) { /* s32 does not cross sign boundary */
> +		if (t32_min > (u32)s32_max || t32_max < (u32)s32_min)
> +			return false;
> +		if (t32.value != ((u32)s32_min & ~t32.mask)) {
> +			if (tnum_step(t32, (u32)s32_min) > (u32)s32_max)
> +				return false;
> +		}
> +	} else { /* s32 crosses sign boundary */
> +		if (t32_min > (u32)s32_max && t32_max < (u32)s32_min)
> +			return false;
> +	}
> +
> +	/*
> +	 * Intersect u64 with u32. If the u64 range spans >=U32_MAX values then an
> +	 * intersection is guaranteed, so we skip that case. Otherwise, we map the
> +	 * u64 bounds to the u32 domain. When mapped, the u64 range might cross the
> +	 * U32_MAX boundary. If it doesn't cross the boundary, it forms a single
> +	 * contiguous range: [(u32)umin, (u32)umax] that we check intersection with
> +	 * u32 bounds. If it does cross the U32_MAX boundary, we get two contiguous
> +	 * ranges: [0, (u32)umax] and [(u32)umin, U32_MAX]. We check if any part of
> +	 * the u32 bounds overlaps with either segment, which is equivalent to
> +	 * ensuring the u32 bounds are not trapped between (u32)umax and (u32)umin.
> +	 */
> +	if (umax - umin < U32_MAX) { /* u64 range does not span entire 32-bit domain */
> +		if ((u32)umin <= (u32)umax) { /* mapped u32 range is a single contiguous range */
> +			if ((u32)umax < u32_min || u32_max < (u32)umin)
> +				return false;
> +		} else { /* mapped u32 range crosses U32_MAX boundary */
> +			if ((u32)umin > u32_max && (u32)umax < u32_min)
> +				return false;
> +		}
> +	}
> +
> +	/*
> +	 * Intersect s64 with u32. This case is similar to u64-u32, but the s64
> +	 * range is mapped to the u32 domain.
> +	 */
> +	if ((u64)smax - (u64)smin < U32_MAX) { /* s64 range does not span entire 32-bit domain */
> +		if ((u32)smin <= (u32)smax) { /* mapped u32 range is a single contiguous range */
> +			if ((u32)smax < u32_min || u32_max < (u32)smin)
> +				return false;
> +		} else { /* mapped u32 range crosses U32_MAX boundary */
> +			if ((u32)smin > u32_max && (u32)smax < u32_min)
> +				return false;
> +		}
> +	}
> +
> +	/*
> +	 * Intersect u64 with s32. We map the u64 range to the s32 domain, where it
> +	 * might cross the S32_MIN/S32_MAX boundary. If it doesn't cross the
> +	 * boundary (it might still cross the -1/0 boundary), we check for overlap
> +	 * in the standard way. Otherwise, we get two contiguous ranges (one of
> +	 * which might cross the -1/0 boundary): [S32_MIN, (s32)umax] and
> +	 * [(s32)umin, S32_MAX]. Intersection exists if the s32 bounds overlap with
> +	 * either segment, which is equivalent to ensuring the s32 bounds are not
> +	 * trapped between (s32)umax and (s32)umin.
> +	 */
> +	if (umax - umin < U32_MAX) { /* u64 range does not span entire 32-bit domain */
> +		if ((s32)umin <= (s32)umax) { /* mapped s32 range is a single contiguous range */
> +			if ((s32)umax < s32_min || s32_max < (s32)umin)
> +				return false;
> +		} else { /* mapped s32 range crosses S32_MIN/S32_MAX boundary */
> +			if ((s32)umin > s32_max && (s32)umax < s32_min)
> +				return false;
> +		}
> +	}
> +
> +	/*
> +	 * Intersect s64 with s32. This case is similar to u64-s32, but the s64
> +	 * range is mapped to the s32 domain.
> +	 */
> +	if ((u64)smax - (u64)smin < U32_MAX) { /* s64 range does not span entire 32-bit domain */
> +		if ((s32)smin <= (s32)smax) { /* mapped s32 range is a single contiguous range */
> +			if ((s32)smax < s32_min || s32_max < (s32)smin)
> +				return false;
> +		} else { /* mapped s32 range crosses S32_MAX/S32_MIN boundary */
> +			if ((s32)smin > s32_max && (s32)smax < s32_min)
> +				return false;
> +		}
> +	}
> +
> +	return true;
> +}
> +
>  static int reg_bounds_sanity_check(struct bpf_verifier_env *env,
>  				   struct bpf_reg_state *reg, const char *ctx)
>  {
> @@ -15493,7 +15707,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
>  	 * reg_states in the FALSE branch (i.e. reg1, reg2), the FALSE branch must be dead. Only
>  	 * TRUE branch will be taken.
>  	 */
> -	if (range_bounds_violation(&env->false_reg1) || range_bounds_violation(&env->false_reg2))
> +	if (!reg_bounds_intersect(&env->false_reg1) || !reg_bounds_intersect(&env->false_reg2))
>  		return 1;
>  
>  	/* Jump (TRUE) branch */
> @@ -15505,7 +15719,7 @@ static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode,
>  	 * reg_states in the TRUE branch (i.e. true_reg1, true_reg2), the TRUE branch must be dead.
>  	 * Only FALSE branch will be taken.
>  	 */
> -	if (range_bounds_violation(&env->true_reg1) || range_bounds_violation(&env->true_reg2))
> +	if (!reg_bounds_intersect(&env->true_reg1) || !reg_bounds_intersect(&env->true_reg2))
>  		return 0;
>  
>  	/* Both branches are possible, we can't determine which one will be taken. */
> -- 
> 2.51.0
>