Message-ID: <CAM=Ch06Jr11bSO1DHO+NSLmxj1kuRW8GmzUfBqKPnhNGs6i=nw@mail.gmail.com>
Date: Thu, 12 Jun 2025 02:36:56 -0400
From: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
To: Eduard Zingerman <eddyz87@...il.com>
Cc: ast@...nel.org, 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 Wed, Jun 11, 2025 at 2:11 PM Eduard Zingerman <eddyz87@...il.com> wrote:
>
> 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.

We didn't specifically look for C programs that show improvements. We
discovered this operator using our abstract operator synthesis
framework, and that was the motivation for the patch.

In theory, programs that make use of overflow or underflow behavior,
particularly where all outcomes overflow, should benefit from this
patch.

As illustrated in the commit message, we do have examples of eBPF
programs that benefit from the precision improvement. We can
definitely add selftests covering each case. I'll send a follow up v2
patch set.

Thanks for the feedback!

> [...]

Powered by blists - more mailing lists