On Sat, Dec 14, 2024 at 11:04 AM Matan Shachnai <m.shachnai@xxxxxxxxx> wrote:
>
> This patch improves (or maintains) the precision of register value tracking
> in BPF_MUL across all possible inputs. It also simplifies
> scalar32_min_max_mul() and scalar_min_max_mul().
>
> As it stands, BPF_MUL is composed of three functions:
>
> case BPF_MUL:
> tnum_mul();
> scalar32_min_max_mul();
> scalar_min_max_mul();
>
> The current implementation of scalar_min_max_mul() restricts the u64 input
> ranges of dst_reg and src_reg to be within [0, U32_MAX]:
>
> /* Both values are positive, so we can work with unsigned and
> * copy the result to signed (unless it exceeds S64_MAX).
> */
> if (umax_val > U32_MAX || dst_reg->umax_value > U32_MAX) {
> /* Potential overflow, we know nothing */
> __mark_reg64_unbounded(dst_reg);
> return;
> }
>
> This restriction is done to avoid unsigned overflow, which could otherwise
> wrap the result around 0, and leave an unsound output where umin > umax. We
> also observe that limiting these u64 input ranges to [0, U32_MAX] leads to
> a loss of precision. Consider the case where the u64 bounds of dst_reg are
> [0, 2^34] and the u64 bounds of src_reg are [0, 2^2]. While the
> multiplication of these two bounds doesn't overflow and is sound [0, 2^36],
> the current scalar_min_max_mul() would set the entire register state to
> unbounded.
>
> Importantly, we update BPF_MUL to allow signed bound multiplication
> (i.e. multiplying negative bounds) as well as allow u64 inputs to take on
> values from [0, U64_MAX]. We perform signed multiplication on two bounds
> [a,b] and [c,d] by multiplying every combination of the bounds
> (i.e. a*c, a*d, b*c, and b*d) and checking for overflow of each product. If
> there is an overflow, we mark the signed bounds unbounded [S64_MIN, S64_MAX].
> In the case of no overflow, we take the minimum of these products to
> be the resulting smin, and the maximum to be the resulting smax.
>
> The key idea here is that if there’s no possibility of overflow, either
> when multiplying signed bounds or unsigned bounds, we can safely multiply the
> respective bounds; otherwise, we set the bounds that exhibit overflow
> (during multiplication) to unbounded.
>
> if (check_mul_overflow(*dst_umax, src_reg->umax_value, dst_umax) ||
> (check_mul_overflow(*dst_umin, src_reg->umin_value, dst_umin))) {
> /* Overflow possible, we know nothing */
> dst_reg->umin_value = 0;
> dst_reg->umax_value = U64_MAX;
> }
> ...
>
> Below, we provide an example BPF program (below) that exhibits the
> imprecision in the current BPF_MUL, where the outputs are all unbounded. In
> contrast, the updated BPF_MUL produces a bounded register state:
>
> BPF_LD_IMM64(BPF_REG_1, 11),
> BPF_LD_IMM64(BPF_REG_2, 4503599627370624),
> BPF_ALU64_IMM(BPF_NEG, BPF_REG_2, 0),
> BPF_ALU64_IMM(BPF_NEG, BPF_REG_2, 0),
> BPF_ALU64_REG(BPF_AND, BPF_REG_1, BPF_REG_2),
> BPF_LD_IMM64(BPF_REG_3, 809591906117232263),
> BPF_ALU64_REG(BPF_MUL, BPF_REG_3, BPF_REG_1),
> BPF_MOV64_IMM(BPF_REG_0, 1),
> BPF_EXIT_INSN(),
>
> Verifier log using the old BPF_MUL:
>
> func#0 @0
> 0: R1=ctx() R10=fp0
> 0: (18) r1 = 0xb ; R1_w=11
> 2: (18) r2 = 0x10000000000080 ; R2_w=0x10000000000080
> 4: (87) r2 = -r2 ; R2_w=scalar()
> 5: (87) r2 = -r2 ; R2_w=scalar()
> 6: (5f) r1 &= r2 ; R1_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=11,var_off=(0x0; 0xb)) R2_w=scalar()
> 7: (18) r3 = 0xb3c3f8c99262687 ; R3_w=0xb3c3f8c99262687
> 9: (2f) r3 *= r1 ; R1_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=11,var_off=(0x0; 0xb)) R3_w=scalar()
> ...
>
> Verifier using the new updated BPF_MUL (more precise bounds at label 9)
>
> func#0 @0
> 0: R1=ctx() R10=fp0
> 0: (18) r1 = 0xb ; R1_w=11
> 2: (18) r2 = 0x10000000000080 ; R2_w=0x10000000000080
> 4: (87) r2 = -r2 ; R2_w=scalar()
> 5: (87) r2 = -r2 ; R2_w=scalar()
> 6: (5f) r1 &= r2 ; R1_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=11,var_off=(0x0; 0xb)) R2_w=scalar()
> 7: (18) r3 = 0xb3c3f8c99262687 ; R3_w=0xb3c3f8c99262687
> 9: (2f) r3 *= r1 ; R1_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=11,var_off=(0x0; 0xb)) R3_w=scalar(smin=0,smax=umax=0x7b96bb0a94a3a7cd,var_off=(0x0; 0x7fffffffffffffff))
> ...
>
> Finally, we proved the soundness of the new scalar_min_max_mul() and
> scalar32_min_max_mul() functions. Typically, multiplication operations are
> expensive to check with bitvector-based solvers. We were able to prove the
> soundness of these functions using Non-Linear Integer Arithmetic (NIA)
> theory. Additionally, using Agni [2,3], we obtained the encodings for
> scalar32_min_max_mul() and scalar_min_max_mul() in bitvector theory, and
> were able to prove their soundness using 8-bit bitvectors (instead of
> 64-bit bitvectors that the functions actually use).
>
> In conclusion, with this patch,
>
> 1. We were able to show that we can improve the overall precision of
> BPF_MUL. We proved (using an SMT solver) that this new version of
> BPF_MUL is at least as precise as the current version for all inputs
> and more precise for some inputs.
>
> 2. We are able to prove the soundness of the new scalar_min_max_mul() and
> scalar32_min_max_mul(). By leveraging the existing proof of tnum_mul
> [1], we can say that the composition of these three functions within
> BPF_MUL is sound.
>
> [1] https://ieeexplore.ieee.org/abstract/document/9741267
> [2] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_12
> [3] https://people.cs.rutgers.edu/~sn349/papers/sas24-preprint.pdf
>
> Co-developed-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@xxxxxxxxxxx>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@xxxxxxxxxxx>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@xxxxxxxxxxx>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@xxxxxxxxxxx>
> Signed-off-by: Matan Shachnai <m.shachnai@xxxxxxxxx>
> ---
> kernel/bpf/verifier.c | 72 +++++++++++++++++++------------------------
> 1 file changed, 32 insertions(+), 40 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index c855e7905c35..5b0f83cc7f4d 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -14118,64 +14118,56 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
> static void scalar32_min_max_mul(struct bpf_reg_state *dst_reg,
> struct bpf_reg_state *src_reg)
> {
> - s32 smin_val = src_reg->s32_min_value;
> - u32 umin_val = src_reg->u32_min_value;
> - u32 umax_val = src_reg->u32_max_value;
> + 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;
> + s32 tmp_prod[4];
>
> - if (smin_val < 0 || dst_reg->s32_min_value < 0) {
> - /* Ain't nobody got time to multiply that sign */
> - __mark_reg32_unbounded(dst_reg);
> - return;
> - }
> - /* Both values are positive, so we can work with unsigned and
> - * copy the result to signed (unless it exceeds S32_MAX).
> - */
> - if (umax_val > U16_MAX || dst_reg->u32_max_value > U16_MAX) {
> - /* Potential overflow, we know nothing */
> - __mark_reg32_unbounded(dst_reg);
> - return;
> + if (check_mul_overflow(*dst_umax, src_reg->u32_max_value, dst_umax) ||
> + check_mul_overflow(*dst_umin, src_reg->u32_min_value, dst_umin)) {
> + /* Overflow possible, we know nothing */
> + dst_reg->u32_min_value = 0;
> + dst_reg->u32_max_value = U32_MAX;
It would be cleaner to use:
*dst_umin = 0;
*dst_umax = U32_MAX;
to make it obvious that though check_mul_overflow()-s wrote something
into dst_umax and dst_umin,
we clean them up with these two assignments.
Just like scalar32_min_max_add() does already.
> }
> - dst_reg->u32_min_value *= umin_val;
> - dst_reg->u32_max_value *= umax_val;
> - if (dst_reg->u32_max_value > S32_MAX) {
> + if (check_mul_overflow(*dst_smin, src_reg->s32_min_value, &tmp_prod[0]) ||
> + check_mul_overflow(*dst_smin, src_reg->s32_max_value, &tmp_prod[1]) ||
> + check_mul_overflow(*dst_smax, src_reg->s32_min_value, &tmp_prod[2]) ||
> + check_mul_overflow(*dst_smax, src_reg->s32_max_value, &tmp_prod[3])) {
> /* Overflow possible, we know nothing */
> dst_reg->s32_min_value = S32_MIN;
> dst_reg->s32_max_value = S32_MAX;
> } else {
> - dst_reg->s32_min_value = dst_reg->u32_min_value;
> - dst_reg->s32_max_value = dst_reg->u32_max_value;
> + dst_reg->s32_min_value = min_array(tmp_prod, 4);
> + dst_reg->s32_max_value = max_array(tmp_prod, 4);
dst_smin/smax here too.
