Re: [PATCH bpf 0/2] bpf: fork state when comparing sign crossing ranges with zero

["Emil Tsalapatis" <emil@etsalapatis.com>]

On Fri May 29, 2026 at 8:23 PM EDT, Eduard Zingerman wrote:
> On Fri, 2026-05-29 at 15:44 -0700, Eduard Zingerman wrote:
>> On Fri, 2026-05-29 at 01:13 -0700, Eduard Zingerman wrote:
>> > YiFei Zhu reported [1] the verifier regression after switch to cnum
>> > based scalars representation. When the following sequence of
>> > instructions is processed:
>> > 
>> >     1: ... rX setup with [negative, positive] bounds ...
>> >     2: if rX == 0 goto ...
>> >     3: if rX > C  goto ...
>> >     4: ... code relying on rX being in range [1, C] ...
>> > 
>> > The cnum-based implementation only infers that rX range is [0, C]
>> > at instruction (4). The pre-cnum signed/unsigned ranges based
>> > representation could always deduct from 'rX != 0' that
>> > umin bound is 1.
>> > 
>> > This patch introduces a workaround forking the verifier state when a
>> > register with sign-crossing range is compared to zero.
>> > 
>> > [1] https://lore.kernel.org/bpf/96c4a1aa4333d10b882a9b5093d2d982f9f106e3.camel@gmail.com/T/
>> > 
>> > ---
>> > Eduard Zingerman (2):
>> >       bpf: fork state when comparing sign crossing ranges with zero
>> >       selftests/bpf: test fork on zero comparison with wrapping ranges
>> > 
>> >  kernel/bpf/verifier.c                              | 71 ++++++++++++++++++++++
>> >  .../testing/selftests/bpf/progs/verifier_bounds.c  | 68 +++++++++++++++++++++
>> >  2 files changed, 139 insertions(+)
>> > ---
>> > base-commit: e42e53ae23b7d41df22ccd7788192bf578f24da2
>> > change-id: 20260529-cnum-split-at-zero-3c03db9234d3
>> 
>> I don't know why CI misses it:
>> 
>> https://github.com/kernel-patches/bpf/pull/12235
>> 
>> But I see two libarena tests failures with this series locally:
>> 
>> File                 Program                    Verdict  Duration (us)   Insns  States  Program size  Jited size
>> -------------------  -------------------------  -------  -------------  ------  ------  ------------  ----------
>> ...
>> libarena_asan.bpf.o  asan_test_buddy_oob        failure         879905  209739    4158          3931           0
>> ...
>> libarena_asan.bpf.o  test_buddy_alloc_multiple  failure         269851  110341    2774          3897           0
>> ...
>> -------------------  -------------------------  -------  -------------  ------  ------  ------------  ----------
>> 
>> Investigating.
>
> So, the gist is: suppose there is a loop:
>
>   for (i = 0; i < SUFFICIENTLY_LARGE; i++) {
>     x = ... range [-127, +128] ...;
>     if (x != 0) {
>       ...
>     }
>     ...
>   }
>
> With this patch-set the 'if (x != 0)' would pile up an additional
> state on the jump stack (second half of the range), compared to
> master. Because the loop is verified till the exit the additional
> states would accumulate on the jump stack. Which means that
> SUFFICIENTLY_LARGE can always be picked such that the program verifies
> on master but fails to verify with this patch.
>
> Two test cases in libarena_asan hit this wall because they have
> large-enough bounded loops (the loops are declared with 'can_loop',
> but 'zero' is declared with 'const', hence the trick doesn't work).
>
> Remaining options are:
> - explore a simple constraints engine
> - revert cnums
> - accept the possibility of such regression
>

For libarena specifically the default for now should be 3) since is is
misusing the volatile zero pattern. Fixing it causes verification errors
but those should be either a) due to pointer arithmetic on non-arena
data, in which case we should add bounds checking, or b) due to pointer
arithmetic on arena data somehow, in which case we should adjust the
verifier. In any case, it should be fixable.

> I'll work on the constraints engine over the weekend.