linux-kernel - Re: [PATCH v2 1/2] bpf, verifier: Improve precision for BPF_ADD and BPF

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: <CAM=Ch06HkqNgh67TGv=_LGp8qdmdtOt3oYk1ZozF15Jg9c3PnA@mail.gmail.com>
Date: Thu, 19 Jun 2025 18:17:09 -0400
From: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
To: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>, 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: [PATCH v2 1/2] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB

On Wed, Jun 18, 2025 at 7:24 AM Hao Sun <sunhao.th@...il.com> wrote:
>
> On Tue, Jun 17, 2025 at 07:17:31PM -0400, Harishankar Vishwanathan wrote:
[...]
>
> Both cvc5 and z3 can prove the above, and one can try this and expect
> it producing SAT on:
> https://cvc5.github.io/app/#temp_a95e25c4-88c5-4257-96c8-0bd74125b179

Thanks for verifying this! As mentioned, we tested the new operators
using Agni, which extracts SMT encodings automatically from the C
source code and
verifies them with Z3, and found the operators to be sound. It is nice
to see that your
testing also concluded that the new operators are sound.

If you’re comfortable, feel free to reply to the patch with a
Tested-by: tag. I’d be happy
to include it in v3 of the patch.

> In addition, the unsoundness of partial case-b can also be proved by
> the following formula, and the counter examples generated may be used
> as test cases if needed:
> https://pastebin.com/raw/qrT7rC1P

We have found that using counterexamples directly for writing test cases is not
straightforward. For instance, consider constructing a test case for the partial
overflow case B. A counterexample might return specific range inputs
([umin, umax]) to
scalar_min_max_add(), which should cause the output to be unbounded
([0, U64_MAX]) due
to the partial overflow. However, these specific range inputs suggested by the
counterexample might not be reachable at all during real verifier
execution. In other
cases, the *tnum* may later refine the result in reg_bounds_sync(),
making the final
output not actually unbounded (when seen in the verifier log).

As such, we adapted Agni's enumerative synthesis procedure with
additional constraints
to generate the test cases.