Re: [PATCH bpf-next v3 1/2] bpf, verifier: Improve precision of BPF_MUL

[Matan Shachnai]

On Mon, Dec 16, 2024 at 3:31 PM Alexei Starovoitov
<alexei.starovoitov@xxxxxxxxx> wrote:
>
> 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.

Thanks, Alexei.
I'll fix it up and follow up with a v4 soon.

>
> >         }
> > -       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.