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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <aRYSlGmmQM1kfF_b@mail.gmail.com>
Date: Thu, 13 Nov 2025 18:17:08 +0100
From: Paul Chaignon <paul.chaignon@...il.com>
To: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
Cc: ast@...nel.org, m.shachnai@...gers.edu, srinivas.narayana@...gers.edu,
	santosh.nagarakatte@...gers.edu,
	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: Re: [RFC PATCH 0/1] bpf, verifier: Detect empty intersection between
 tnum and ranges

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
>