* [PATCH] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB
@ 2025-06-10 22:13 Harishankar Vishwanathan
2025-06-11 18:11 ` Eduard Zingerman
0 siblings, 1 reply; 3+ messages in thread
From: Harishankar Vishwanathan @ 2025-06-10 22:13 UTC (permalink / raw)
To: ast
Cc: Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana,
Santosh Nagarakatte, Daniel Borkmann, John Fastabend,
Andrii Nakryiko, Martin KaFai Lau, Eduard Zingerman, Song Liu,
Yonghong Song, KP Singh, Stanislav Fomichev, Hao Luo, Jiri Olsa,
bpf, linux-kernel
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@rutgers.edu>
Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
---
kernel/bpf/verifier.c | 76 +++++++++++++++++++++++++++++++------------
1 file changed, 56 insertions(+), 20 deletions(-)
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index b1f797616f20..b4909b9cfc9f 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14553,14 +14553,25 @@ static void scalar32_min_max_add(struct bpf_reg_state *dst_reg,
s32 *dst_smax = &dst_reg->s32_max_value;
u32 *dst_umin = &dst_reg->u32_min_value;
u32 *dst_umax = &dst_reg->u32_max_value;
+ u32 umin_val = src_reg->u32_min_value;
+ u32 umax_val = src_reg->u32_max_value;
+ bool min_overflow, max_overflow;
if (check_add_overflow(*dst_smin, src_reg->s32_min_value, dst_smin) ||
check_add_overflow(*dst_smax, src_reg->s32_max_value, dst_smax)) {
*dst_smin = S32_MIN;
*dst_smax = S32_MAX;
}
- if (check_add_overflow(*dst_umin, src_reg->u32_min_value, dst_umin) ||
- check_add_overflow(*dst_umax, src_reg->u32_max_value, dst_umax)) {
+
+ /* If either all additions overflow or no additions overflow, then
+ * it is okay to set: dst_umin = dst_umin + src_umin, dst_umax =
+ * dst_umax + src_umax. Otherwise (some additions overflow), set
+ * the output bounds to unbounded.
+ */
+ min_overflow = check_add_overflow(*dst_umin, umin_val, dst_umin);
+ max_overflow = check_add_overflow(*dst_umax, umax_val, dst_umax);
+
+ if (!min_overflow && max_overflow) {
*dst_umin = 0;
*dst_umax = U32_MAX;
}
@@ -14573,14 +14584,25 @@ static void scalar_min_max_add(struct bpf_reg_state *dst_reg,
s64 *dst_smax = &dst_reg->smax_value;
u64 *dst_umin = &dst_reg->umin_value;
u64 *dst_umax = &dst_reg->umax_value;
+ u64 umin_val = src_reg->umin_value;
+ u64 umax_val = src_reg->umax_value;
+ bool min_overflow, max_overflow;
if (check_add_overflow(*dst_smin, src_reg->smin_value, dst_smin) ||
check_add_overflow(*dst_smax, src_reg->smax_value, dst_smax)) {
*dst_smin = S64_MIN;
*dst_smax = S64_MAX;
}
- if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
- check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
+
+ /* If either all additions overflow or no additions overflow, then
+ * it is okay to set: dst_umin = dst_umin + src_umin, dst_umax =
+ * dst_umax + src_umax. Otherwise (some additions overflow), set
+ * the output bounds to unbounded.
+ */
+ min_overflow = check_add_overflow(*dst_umin, umin_val, dst_umin);
+ max_overflow = check_add_overflow(*dst_umax, umax_val, dst_umax);
+
+ if (!min_overflow && max_overflow) {
*dst_umin = 0;
*dst_umax = U64_MAX;
}
@@ -14591,8 +14613,11 @@ static void scalar32_min_max_sub(struct bpf_reg_state *dst_reg,
{
s32 *dst_smin = &dst_reg->s32_min_value;
s32 *dst_smax = &dst_reg->s32_max_value;
+ u32 *dst_umin = &dst_reg->u32_min_value;
+ u32 *dst_umax = &dst_reg->u32_max_value;
u32 umin_val = src_reg->u32_min_value;
u32 umax_val = src_reg->u32_max_value;
+ bool min_underflow, max_underflow;
if (check_sub_overflow(*dst_smin, src_reg->s32_max_value, dst_smin) ||
check_sub_overflow(*dst_smax, src_reg->s32_min_value, dst_smax)) {
@@ -14600,14 +14625,18 @@ static void scalar32_min_max_sub(struct bpf_reg_state *dst_reg,
*dst_smin = S32_MIN;
*dst_smax = S32_MAX;
}
- if (dst_reg->u32_min_value < umax_val) {
- /* Overflow possible, we know nothing */
- dst_reg->u32_min_value = 0;
- dst_reg->u32_max_value = U32_MAX;
- } else {
- /* Cannot overflow (as long as bounds are consistent) */
- dst_reg->u32_min_value -= umax_val;
- dst_reg->u32_max_value -= umin_val;
+
+ /* If either all subtractions underflow or no subtractions
+ * underflow, it is okay to set: dst_umin = dst_umin - src_umax,
+ * dst_umax = dst_umax - src_umin. Otherwise (some subtractions
+ * underflow), set the output bounds to unbounded.
+ */
+ min_underflow = check_sub_overflow(*dst_umin, umax_val, dst_umin);
+ max_underflow = check_sub_overflow(*dst_umax, umin_val, dst_umax);
+
+ if (min_underflow && !max_underflow) {
+ *dst_umin = 0;
+ *dst_umax = U32_MAX;
}
}
@@ -14616,8 +14645,11 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
{
s64 *dst_smin = &dst_reg->smin_value;
s64 *dst_smax = &dst_reg->smax_value;
+ u64 *dst_umin = &dst_reg->umin_value;
+ u64 *dst_umax = &dst_reg->umax_value;
u64 umin_val = src_reg->umin_value;
u64 umax_val = src_reg->umax_value;
+ bool min_underflow, max_underflow;
if (check_sub_overflow(*dst_smin, src_reg->smax_value, dst_smin) ||
check_sub_overflow(*dst_smax, src_reg->smin_value, dst_smax)) {
@@ -14625,14 +14657,18 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
*dst_smin = S64_MIN;
*dst_smax = S64_MAX;
}
- if (dst_reg->umin_value < umax_val) {
- /* Overflow possible, we know nothing */
- dst_reg->umin_value = 0;
- dst_reg->umax_value = U64_MAX;
- } else {
- /* Cannot overflow (as long as bounds are consistent) */
- dst_reg->umin_value -= umax_val;
- dst_reg->umax_value -= umin_val;
+
+ /* If either all subtractions underflow or no subtractions
+ * underflow, it is okay to set: dst_umin = dst_umin - src_umax,
+ * dst_umax = dst_umax - src_umin. Otherwise (some subtractions
+ * underflow), set the output bounds to unbounded.
+ */
+ min_underflow = check_sub_overflow(*dst_umin, umax_val, dst_umin);
+ max_underflow = check_sub_overflow(*dst_umax, umin_val, dst_umax);
+
+ if (min_underflow && !max_underflow) {
+ *dst_umin = 0;
+ *dst_umax = U64_MAX;
}
}
--
2.45.2
^ permalink raw reply related [flat|nested] 3+ messages in thread
* Re: [PATCH] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB
2025-06-10 22:13 [PATCH] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB Harishankar Vishwanathan
@ 2025-06-11 18:11 ` Eduard Zingerman
2025-06-12 6:36 ` Harishankar Vishwanathan
0 siblings, 1 reply; 3+ messages in thread
From: Eduard Zingerman @ 2025-06-11 18:11 UTC (permalink / raw)
To: Harishankar Vishwanathan, ast
Cc: Matan Shachnai, Srinivas Narayana, Santosh Nagarakatte,
Daniel Borkmann, John Fastabend, Andrii Nakryiko,
Martin KaFai Lau, Song Liu, Yonghong Song, KP Singh,
Stanislav Fomichev, Hao Luo, Jiri Olsa, bpf, linux-kernel
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@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.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.
[...]
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [PATCH] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB
2025-06-11 18:11 ` Eduard Zingerman
@ 2025-06-12 6:36 ` Harishankar Vishwanathan
0 siblings, 0 replies; 3+ messages in thread
From: Harishankar Vishwanathan @ 2025-06-12 6:36 UTC (permalink / raw)
To: Eduard Zingerman
Cc: ast, Matan Shachnai, Srinivas Narayana, Santosh Nagarakatte,
Daniel Borkmann, John Fastabend, Andrii Nakryiko,
Martin KaFai Lau, Song Liu, Yonghong Song, KP Singh,
Stanislav Fomichev, Hao Luo, Jiri Olsa, bpf, linux-kernel
On Wed, Jun 11, 2025 at 2:11 PM Eduard Zingerman <eddyz87@gmail.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@rutgers.edu>
> > Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> > Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> > Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> > Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> > Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> > Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.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!
> [...]
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2025-06-12 6:37 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2025-06-10 22:13 [PATCH] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB Harishankar Vishwanathan
2025-06-11 18:11 ` Eduard Zingerman
2025-06-12 6:36 ` Harishankar Vishwanathan
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).