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

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2026-04-16 at 19:13 -0400, Harishankar Vishwanathan wrote:
> On Wed, Apr 15, 2026 at 9:10 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Wed, 2026-04-15 at 12:07 -0400, Harishankar Vishwanathan wrote:
> [...]
> > 
> > For example, given the current implementations for
> > is_scalar_branch_taken(), regs_refine_cond_op(),
> > deduce_bounds_64_from_64() is it ever possible for u64 range not to
> > intersect with s64 range?
> 
> > After spending some time with pen and paper for BPF_JLE operation I
> > suspect that it is not possible. I also encoded this as a small cbmc
> > test: https://github.com/eddyz87/intersection-check.
> > I suspect that same reasoning applies for other operations.
> 
> Hi Eduard,
> 
> First to confirm if I am reading the CBMC code
> correctly, the precondition for the verification is that the inputs to the
> BPF_JLE code are
> 1) register states are valid initial states (at least one concrete
> value satisfying both its u64 and s64 bounds)
> 2) the input register states have been passed through
> deduce_bounds_64_from_64()

Yes, that's what I tried to check.

> Without the 2), the verification fails.
> I am assuming the rationale is that any inputs to the BPF_JLE code in
> actual verifier will have passed through reg_bounds_sync()
> in a previous instruction.
> 
> If the understanding is correct, then, I had the following questions:
> 
> 1) Other reg_bounds_sync() functions.
> What if the other reg_bounds_sync() functions update the
> abstract register values in a way that makes the jump operators
> produce no intersection between u64 and s64 (when reg_bound_offset
> and update_reg_bounds are run at the end)? Is this not possible?
> 
> 2) Other jump operators.
> The CBMC code currently doesn't check for, i.e. JEQ, JNE, JSLE,
> JSLT, JSGE, JSGT, JSET. Could they produce an u64-s64 empty
> intersection?

To answer both your questions: this needs additional investigation.
In general, I think it would be nice for the parts of reg_bounds_sync()
to have the following properties:
- valid register remains valid
- invalid register remains invalid

This would need some modifications and proofing to work.

> 
> > I'd suggest to drop the u32/s32 and u64/s64 checks, unless a counter
> > example can be found. I'm not sure about 64/32-bit checks.
> > Wdyt?
> 
> Given Paul's tests [1] on the Cilium suite revealed almost no performance
> impact of these checks, should we keep them all to stay on the safe side?

What I don't like is that we go through all the trouble to intersect
the ranges and still have an incomplete result, because we still don't
know if all ranges intersect at some common point (that's true for 5
arbitrary sets, here we have connected domains, so maybe there are
some additional constraints that make pairwise comparison guarantee
common intersection, but that requires additional reasoning).

Could you please comment about the witness idea?
Suppose reg_bounds_sync() is modified to preserve the properties I
described above, would it be sufficient to check two candidates:
tmin and tnum_step(tmin) to identify a register in an invalid state?