| 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
| ||
|
Message-ID: <a39e1ed2db4121b690796c347f1259da09e23e13.camel@gmail.com>
Date: Wed, 11 Jun 2025 11:11:28 -0700
From: Eduard Zingerman <eddyz87@...il.com>
To: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>,
ast@...nel.org
Cc: Matan Shachnai <m.shachnai@...gers.edu>, Srinivas Narayana
<srinivas.narayana@...gers.edu>, Santosh Nagarakatte
<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>, 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] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB
On Tue, 2025-06-10 at 18:13 -0400, Harishankar Vishwanathan wrote:
> This patch improves the precison of the scalar(32)_min_max_add and
> scalar(32)_min_max_sub functions, which update the u(32)min/u(32)_max
> ranges for the BPF_ADD and BPF_SUB instructions. We discovered this more
> precise operator using a technique we are developing for automatically
> synthesizing functions for updating tnums and ranges.
>
> According to the BPF ISA [1], "Underflow and overflow are allowed during
> arithmetic operations, meaning the 64-bit or 32-bit value will wrap".
> Our patch leverages the wrap-around semantics of unsigned overflow and
> underflow to improve precision.
>
> Below is an example of our patch for scalar_min_max_add; the idea is
> analogous for all four functions.
>
> There are three cases to consider when adding two u64 ranges [dst_umin,
> dst_umax] and [src_umin, src_umax]. Consider a value x in the range
> [dst_umin, dst_umax] and another value y in the range [src_umin,
> src_umax].
>
> (a) No overflow: No addition x + y overflows. This occurs when even the
> largest possible sum, i.e., dst_umax + src_umax <= U64_MAX.
>
> (b) Partial overflow: Some additions x + y overflow. This occurs when
> the largest possible sum overflows (dst_umax + src_umax > U64_MAX), but
> the smallest possible sum does not overflow (dst_umin + src_umin <=
> U64_MAX).
>
> (c) Full overflow: All additions x + y overflow. This occurs when both
> the smallest possible sum and the largest possible sum overflow, i.e.,
> both (dst_umin + src_umin) and (dst_umax + src_umax) are > U64_MAX.
>
> The current implementation conservatively sets the output bounds to
> unbounded, i.e, [umin=0, umax=U64_MAX], whenever there is *any*
> possibility of overflow, i.e, in cases (b) and (c). Otherwise it
> computes tight bounds as [dst_umin + src_umin, dst_umax + src_umax]:
>
> if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
> check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
> *dst_umin = 0;
> *dst_umax = U64_MAX;
> }
>
> Our synthesis-based technique discovered a more precise operator.
> Particularly, in case (c), all possible additions x + y overflow and
> wrap around according to eBPF semantics, and the computation of the
> output range as [dst_umin + src_umin, dst_umax + src_umax] continues to
> work. Only in case (b), do we need to set the output bounds to
> unbounded, i.e., [0, U64_MAX].
>
> Case (b) can be checked by seeing if the minimum possible sum does *not*
> overflow and the maximum possible sum *does* overflow, and when that
> happens, we set the output to unbounded:
>
> min_overflow = check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin);
> max_overflow = check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax);
>
> if (!min_overflow && max_overflow) {
> *dst_umin = 0;
> *dst_umax = U64_MAX;
> }
>
> Below is an example eBPF program and the corresponding log from the
> verifier. Before instruction 6, register r3 has bounds
> [0x8000000000000000, U64_MAX].
>
> The current implementation sets r3's bounds to [0, U64_MAX] after
> instruction r3 += r3, due to conservative overflow handling.
>
> 0: R1=ctx() R10=fp0
> 0: (18) r3 = 0x8000000000000000 ; R3_w=0x8000000000000000
> 2: (18) r4 = 0x0 ; R4_w=0
> 4: (87) r4 = -r4 ; R4_w=scalar()
> 5: (4f) r3 |= r4 ; R3_w=scalar(smax=-1,umin=0x8000000000000000,var_off=(0x8000000000000000; 0x7fffffffffffffff)) R4_w=scalar()
> 6: (0f) r3 += r3 ; R3_w=scalar()
> 7: (b7) r0 = 1 ; R0_w=1
> 8: (95) exit
>
> With our patch, r3's bounds after instruction 6 are set to a more precise
> [0, 0xfffffffffffffffe].
>
> ...
> 6: (0f) r3 += r3 ; R3_w=scalar(umax=0xfffffffffffffffe)
> 7: (b7) r0 = 1 ; R0_w=1
> 8: (95) exit
>
> The logic for scalar32_min_max_add is analogous. For the
> scalar(32)_min_max_sub functions, the reasoning is similar but applied
> to detecting underflow instead of overflow.
>
> We verified the correctness of the new implementations using Agni [3,4].
>
> We since also discovered that a similar technique has been used to
> calculate output ranges for unsigned interval addition and subtraction
> in Hacker's Delight [2].
>
> [1] https://docs.kernel.org/bpf/standardization/instruction-set.html
> [2] Hacker's Delight Ch.4-2, Propagating Bounds through Add’s and Subtract’s
> [3] https://github.com/bpfverif/agni
> [4] https://people.cs.rutgers.edu/~sn349/papers/sas24-preprint.pdf
>
> Co-developed-by: Matan Shachnai <m.shachnai@...gers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@...gers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@...gers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@...gers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@...gers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@...gers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
> ---
Is this patch dictated by mere possibility of improvement or you
observed some C programs that can benefit from the change?
Could you please add selftests covering each overflow / underflow
combination?
Please use same framework as tools/testing/selftests/bpf/progs/verifier_and.c.
[...]
Powered by blists - more mailing lists