Commits on Nov 29, 2024

1. bpf, verifier: Improve precision of BPF_MUL …

   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.
   
   The key idea of our patch is that if there’s no possibility of overflow, we
   can multiply the unsigned bounds; otherwise, we set the 64-bit bounds to
   [0, U64_MAX], marking them as 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;
       }
     ...
   
   Now, to update the signed bounds based on the unsigned bounds, we need to
   ensure that the unsigned bounds don't cross the signed boundary (i.e., if
   ((s64)reg->umin_value <= (s64)reg->umax_value)). We observe that this is
   done anyway by __reg_deduce_bounds later, so we can just set signed bounds
   to unbounded [S64_MIN, S64_MAX]. Deferring the assignment of s64 bounds to
   reg_bounds_sync removes the current redundancy in scalar_min_max_mul(),
   which currently sets the s64 bounds based on the u64 bounds only in the
   case where umin <= umax <= 2^(63)-1.
   
   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 16-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.
   
   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 <[email protected]>
   Signed-off-by: Harishankar Vishwanathan <[email protected]>
   Co-developed-by: Srinivas Narayana <[email protected]>
   Signed-off-by: Srinivas Narayana <[email protected]>
   Co-developed-by: Santosh Nagarakatte <[email protected]>
   Signed-off-by: Santosh Nagarakatte <[email protected]>
   Signed-off-by: Matan Shachnai <[email protected]>

   

   mshachnai authored and Kernel Patches Daemon committed Nov 29, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for f826d84
   • Browse repository at this point

   Copy the full SHA

   f826d84 View commit details

   Browse the repository at this point in the history