| Message ID | ykuhustu7vt2ilwhl32kj655xfdgdlm2xkl5rff6tw2ycksovp@ss2n4gpjysnw (mailing list archive) |
|---|---|
| State | Superseded |
| Delegated to: | BPF |
| Headers | show |
| Series | [RFC,bpf-next] bpf, verifier: improve signed ranges inference for BPF_AND | expand |
On Tue, Jul 16, 2024 at 10:52:26PM GMT, Shung-Hsi Yu wrote: > This commit teach the BPF verifier how to infer signed ranges directly > from signed ranges of the operands to prevent verifier rejection ... > --- > kernel/bpf/verifier.c | 62 +++++++++++++++++++++++++++++-------------- > 1 file changed, 42 insertions(+), 20 deletions(-) > > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c > index 8da132a1ef28..6d4cdf30cd76 100644 > --- a/kernel/bpf/verifier.c > +++ b/kernel/bpf/verifier.c > @@ -13466,6 +13466,39 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg, > } > } > > +/* Clears all trailing bits after the most significant unset bit. > + * > + * Used for estimating the minimum possible value after BPF_AND. This > + * effectively rounds a negative value down to a negative power-of-2 value > + * (except for -1, which just return -1) and returning 0 for non-negative > + * values. E.g. masked32_negative(0xff0ff0ff) == 0xff000000. s/masked32_negative/negative32_bit_floor/ > + */ > +static inline s32 negative32_bit_floor(s32 v) > +{ > + /* XXX: per C standard section 6.5.7 right shift of signed negative > + * value is implementation-defined. Should unsigned type be used here > + * instead? > + */ > + v &= v >> 1; > + v &= v >> 2; > + v &= v >> 4; > + v &= v >> 8; > + v &= v >> 16; > + return v; > +} > + > +/* Same as negative32_bit_floor() above, but for 64-bit signed value */ > +static inline s64 negative_bit_floor(s64 v) > +{ > + v &= v >> 1; > + v &= v >> 2; > + v &= v >> 4; > + v &= v >> 8; > + v &= v >> 16; > + v &= v >> 32; > + return v; > +} > + > static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, > struct bpf_reg_state *src_reg) > { > @@ -13485,16 +13518,10 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, > dst_reg->u32_min_value = var32_off.value; > dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val); > > - /* Safe to set s32 bounds by casting u32 result into s32 when u32 > - * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded. > - */ > - if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) { > - dst_reg->s32_min_value = dst_reg->u32_min_value; > - dst_reg->s32_max_value = dst_reg->u32_max_value; > - } else { > - dst_reg->s32_min_value = S32_MIN; > - dst_reg->s32_max_value = S32_MAX; > - } > + /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */ > + dst_reg->s32_min_value = negative32_bit_floor(min(dst_reg->s32_min_value, > + src_reg->s32_min_value)); > + dst_reg->s32_max_value = max(dst_reg->s32_max_value, src_reg->s32_max_value); > } > > static void scalar_min_max_and(struct bpf_reg_state *dst_reg, > @@ -13515,16 +13542,11 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg, > dst_reg->umin_value = dst_reg->var_off.value; > dst_reg->umax_value = min(dst_reg->umax_value, umax_val); > > - /* Safe to set s64 bounds by casting u64 result into s64 when u64 > - * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded. > - */ > - if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) { > - dst_reg->smin_value = dst_reg->umin_value; > - dst_reg->smax_value = dst_reg->umax_value; > - } else { > - dst_reg->smin_value = S64_MIN; > - dst_reg->smax_value = S64_MAX; > - } > + /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */ > + dst_reg->smin_value = negative_bit_floor(min(dst_reg->smin_value, > + src_reg->smin_value)); > + dst_reg->smax_value = max(dst_reg->smax_value, src_reg->smax_value); > + > /* We may learn something more from the var_off */ > __update_reg_bounds(dst_reg); > } Checked that this passes BPF CI[0] (except s390x-gcc/test_verifier, which seems stucked), and verified the logic with z3 (see attached Python script, adapted from [1]); so it seems to work. Will try running tools/testing/selftests/bpf/prog_tests/reg_bounds.c against it next. 0: https://github.com/kernel-patches/bpf/actions/runs/9958322024 1: https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
On Tue, 2024-07-16 at 22:52 +0800, Shung-Hsi Yu wrote: [...] > To allow verification of such instruction pattern, update > scalar*_min_max_and() to infer signed ranges directly from signed ranges > of the operands. With BPF_AND, the resulting value always gains more > unset '0' bit, thus it only move towards 0x0000000000000000. The > difficulty lies with how to deal with signs. While non-negative > (positive and zero) value simply grows smaller, a negative number can > grows smaller, but may also underflow and become a larger value. > > To better address this situation we split the signed ranges into > negative range and non-negative range cases, ignoring the mixed sign > cases for now; and only consider how to calculate smax_value. > > Since negative range & negative range preserve the sign bit, so we know > the result is still a negative value, thus it only move towards S64_MIN, > but never underflow, thus a save bet is to use a value in ranges that is > closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For > negative range & positive range the sign bit is always cleared, thus we > know the resulting is a non-negative, and only moves towards 0, so a > safe bet is to use smax_value of the non-negative range. Last but not > least, non-negative range & non-negative range is still a non-negative > value, and only moves towards 0; however same as the unsigned range > case, the maximum is actually capped by the lesser of the two, and thus > min(dst_reg->smax_value, src_reg->smax_value); > > Listing out the above reasoning as a table (dst_reg abbreviated as dst, > src_reg abbreviated as src, smax_value abbrivated as smax) we get: > > | src_reg > smax = ? +---------------------------+--------------------------- > | negative | non-negative > ---------+--------------+---------------------------+--------------------------- > | negative | max(dst->smax, src->smax) | src->smax > dst_reg +--------------+---------------------------+--------------------------- > | non-negative | dst->smax | min(dst->smax, src->smax) > > However this is quite complicated, luckily it can be simplified given > the following observations > > max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value > max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value > max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value) > > So we could substitute the cells in the table above all with max(...), > and arrive at: > > | src_reg > smax' = ? +---------------------------+--------------------------- > | negative | non-negative > ---------+--------------+---------------------------+--------------------------- > | negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) > dst_reg +--------------+---------------------------+--------------------------- > | non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) > > Meaning that simply using > > max(dst_reg->smax_value, src_reg->smax_value) > > to calculate the resulting smax_value would work across all sign combinations. > > > For smin_value, we know that both non-negative range & non-negative > range and negative range & non-negative range both result in a > non-negative value, so an easy guess is to use the minimum non-negative > value, thus 0. > > | src_reg > smin = ? +----------------------------+--------------------------- > | negative | non-negative > ---------+--------------+----------------------------+--------------------------- > | negative | ? | 0 > dst_reg +--------------+----------------------------+--------------------------- > | non-negative | 0 | 0 > > This leave the negative range & negative range case to be considered. We > know that negative range & negative range always yield a negative value, > so a preliminary guess would be S64_MIN. However, that guess is too > imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern > we're trying to deal with here. > > This can be further improve with the observation that for negative range > & negative range, the smallest possible value must be one that has > longest _common_ most-significant set '1' bits sequence, thus we can use > min(dst_reg->smin_value, src->smin_value) as the starting point, as the > smaller value will be the one with the shorter most-significant set '1' > bits sequence. But that alone is not enough, as we do not know whether > rest of the bits would be set, so the safest guess would be one that > clear alls bits after the most-significant set '1' bits sequence, > something akin to bit_floor(), but for rounding to a negative power-of-2 > instead. > > negative_bit_floor(0xffff000000000003) == 0xffff000000000000 > negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000 > negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000 > > With negative range & negative range solve, we now have: > > | src_reg > smin = ? +----------------------------+--------------------------- > | negative | non-negative > ---------+--------------+----------------------------+--------------------------- > | negative |negative_bit_floor( | 0 > | | min(dst->smin, src->smin))| > dst_reg +--------------+----------------------------+--------------------------- > | non-negative | 0 | 0 > > This can be further simplied since min(dst->smin, src->smin) < 0 when both > dst_reg and src_reg have a negative range. Which means using > > negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value) > > to calculate the resulting smin_value would work across all sign combinations. > > Together these allows us to infer the signed range of the result of BPF_AND > operation using the signed range from its operands. Hi Shung-Hsi, This seems quite elegant. As an additional check, I did a simple brute-force for all possible ranges of 6-bit integers and bounds are computed safely. [...]
On Wed, Jul 17, 2024 at 02:10:35PM GMT, Eduard Zingerman wrote: > On Tue, 2024-07-16 at 22:52 +0800, Shung-Hsi Yu wrote: > > [...] > > > To allow verification of such instruction pattern, update > > scalar*_min_max_and() to infer signed ranges directly from signed ranges > > of the operands. With BPF_AND, the resulting value always gains more > > unset '0' bit, thus it only move towards 0x0000000000000000. The > > difficulty lies with how to deal with signs. While non-negative > > (positive and zero) value simply grows smaller, a negative number can > > grows smaller, but may also underflow and become a larger value. > > > > To better address this situation we split the signed ranges into > > negative range and non-negative range cases, ignoring the mixed sign > > cases for now; and only consider how to calculate smax_value. > > > > Since negative range & negative range preserve the sign bit, so we know > > the result is still a negative value, thus it only move towards S64_MIN, > > but never underflow, thus a save bet is to use a value in ranges that is > > closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For > > negative range & positive range the sign bit is always cleared, thus we > > know the resulting is a non-negative, and only moves towards 0, so a > > safe bet is to use smax_value of the non-negative range. Last but not > > least, non-negative range & non-negative range is still a non-negative > > value, and only moves towards 0; however same as the unsigned range > > case, the maximum is actually capped by the lesser of the two, and thus > > min(dst_reg->smax_value, src_reg->smax_value); > > > > Listing out the above reasoning as a table (dst_reg abbreviated as dst, > > src_reg abbreviated as src, smax_value abbrivated as smax) we get: > > > > | src_reg > > smax = ? +---------------------------+--------------------------- > > | negative | non-negative > > ---------+--------------+---------------------------+--------------------------- > > | negative | max(dst->smax, src->smax) | src->smax > > dst_reg +--------------+---------------------------+--------------------------- > > | non-negative | dst->smax | min(dst->smax, src->smax) > > > > However this is quite complicated, luckily it can be simplified given > > the following observations > > > > max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value > > max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value > > max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value) > > > > So we could substitute the cells in the table above all with max(...), > > and arrive at: > > > > | src_reg > > smax' = ? +---------------------------+--------------------------- > > | negative | non-negative > > ---------+--------------+---------------------------+--------------------------- > > | negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) > > dst_reg +--------------+---------------------------+--------------------------- > > | non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) > > > > Meaning that simply using > > > > max(dst_reg->smax_value, src_reg->smax_value) > > > > to calculate the resulting smax_value would work across all sign combinations. > > > > > > For smin_value, we know that both non-negative range & non-negative > > range and negative range & non-negative range both result in a > > non-negative value, so an easy guess is to use the minimum non-negative > > value, thus 0. > > > > | src_reg > > smin = ? +----------------------------+--------------------------- > > | negative | non-negative > > ---------+--------------+----------------------------+--------------------------- > > | negative | ? | 0 > > dst_reg +--------------+----------------------------+--------------------------- > > | non-negative | 0 | 0 > > > > This leave the negative range & negative range case to be considered. We > > know that negative range & negative range always yield a negative value, > > so a preliminary guess would be S64_MIN. However, that guess is too > > imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern > > we're trying to deal with here. > > > > This can be further improve with the observation that for negative range > > & negative range, the smallest possible value must be one that has > > longest _common_ most-significant set '1' bits sequence, thus we can use > > min(dst_reg->smin_value, src->smin_value) as the starting point, as the > > smaller value will be the one with the shorter most-significant set '1' > > bits sequence. But that alone is not enough, as we do not know whether > > rest of the bits would be set, so the safest guess would be one that > > clear alls bits after the most-significant set '1' bits sequence, > > something akin to bit_floor(), but for rounding to a negative power-of-2 > > instead. > > > > negative_bit_floor(0xffff000000000003) == 0xffff000000000000 > > negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000 > > negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000 > > > > With negative range & negative range solve, we now have: > > > > | src_reg > > smin = ? +----------------------------+--------------------------- > > | negative | non-negative > > ---------+--------------+----------------------------+--------------------------- > > | negative |negative_bit_floor( | 0 > > | | min(dst->smin, src->smin))| > > dst_reg +--------------+----------------------------+--------------------------- > > | non-negative | 0 | 0 > > > > This can be further simplied since min(dst->smin, src->smin) < 0 when both > > dst_reg and src_reg have a negative range. Which means using > > > > negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value) > > > > to calculate the resulting smin_value would work across all sign combinations. > > > > Together these allows us to infer the signed range of the result of BPF_AND > > operation using the signed range from its operands. > > Hi Shung-Hsi, > > This seems quite elegant. > As an additional check, I did a simple brute-force for all possible > ranges of 6-bit integers and bounds are computed safely. Thanks for looking into this, as well as the complement. Did took me quite awhile to try come up with a simple solution that works just well enough without further complication, felt quite proud :) > [...]
On Tue, Jul 16, 2024 at 10:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote: > > This commit teach the BPF verifier how to infer signed ranges directly > from signed ranges of the operands to prevent verifier rejection, which > is needed for the following BPF program's no-alu32 version, as shown by > Xu Kuohai: > > SEC("lsm/bpf_map") > int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) > { > if (map != (struct bpf_map *)&data_input) > return 0; > > if (fmode & FMODE_WRITE) > return -EACCES; > > return 0; > } > > Where the relevant verifer log upon rejection are: > > ... > 5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx() > ; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32 > 6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000)) > 7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0) > ; @ test_libbpf_get_fd_by_id_opts.c:0 > 8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) > 9: (95) exit > > This sequence of instructions comes from Clang's transformation located > in DAGCombiner::SimplifySelectCC() method, which combined the "fmode & > FMODE_WRITE" check with the return statement without needing BPF_JMP at > all. See Eduard's comment for more detail of this transformation[0]. > > While the verifier can correctly infer that the value of r0 is in a > tight [-1, 0] range after instruction "r0 s>>= 63", is was not able to > come up with a tight range for "r0 &= -13" (which would be [-13, 0]), > and instead inferred a very loose range: > > r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0) > r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) > > The reason is that scalar*_min_max_add() mainly relies on tnum for > interring value in register after BPF_AND, however [-1, 0] cannot be > tracked precisely with tnum, and effectively turns into [0, -1] (i.e. > tnum_unknown). So upon BPF_AND the resulting tnum is equivalent to > > dst_reg->var_off = tnum_and(tnum_unknown, tnum_const(-13)) > > And from there the BPF verifier was only able to infer smin=S64_MIN, > smax=0x7ffffffffffffff3, which is outside of the expected [-4095, 0] > range for return values, and thus the program was rejected. > > To allow verification of such instruction pattern, update > scalar*_min_max_and() to infer signed ranges directly from signed ranges > of the operands. With BPF_AND, the resulting value always gains more > unset '0' bit, thus it only move towards 0x0000000000000000. The > difficulty lies with how to deal with signs. While non-negative > (positive and zero) value simply grows smaller, a negative number can > grows smaller, but may also underflow and become a larger value. > > To better address this situation we split the signed ranges into > negative range and non-negative range cases, ignoring the mixed sign > cases for now; and only consider how to calculate smax_value. > > Since negative range & negative range preserve the sign bit, so we know > the result is still a negative value, thus it only move towards S64_MIN, > but never underflow, thus a save bet is to use a value in ranges that is > closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For > negative range & positive range the sign bit is always cleared, thus we > know the resulting is a non-negative, and only moves towards 0, so a > safe bet is to use smax_value of the non-negative range. Last but not > least, non-negative range & non-negative range is still a non-negative > value, and only moves towards 0; however same as the unsigned range > case, the maximum is actually capped by the lesser of the two, and thus > min(dst_reg->smax_value, src_reg->smax_value); > > Listing out the above reasoning as a table (dst_reg abbreviated as dst, > src_reg abbreviated as src, smax_value abbrivated as smax) we get: > > | src_reg > smax = ? +---------------------------+--------------------------- > | negative | non-negative > ---------+--------------+---------------------------+--------------------------- > | negative | max(dst->smax, src->smax) | src->smax > dst_reg +--------------+---------------------------+--------------------------- > | non-negative | dst->smax | min(dst->smax, src->smax) > > However this is quite complicated, luckily it can be simplified given > the following observations > > max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value > max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value > max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value) > > So we could substitute the cells in the table above all with max(...), > and arrive at: > > | src_reg > smax' = ? +---------------------------+--------------------------- > | negative | non-negative > ---------+--------------+---------------------------+--------------------------- > | negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) > dst_reg +--------------+---------------------------+--------------------------- > | non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) > > Meaning that simply using > > max(dst_reg->smax_value, src_reg->smax_value) > > to calculate the resulting smax_value would work across all sign combinations. > > > For smin_value, we know that both non-negative range & non-negative > range and negative range & non-negative range both result in a > non-negative value, so an easy guess is to use the minimum non-negative > value, thus 0. > > | src_reg > smin = ? +----------------------------+--------------------------- > | negative | non-negative > ---------+--------------+----------------------------+--------------------------- > | negative | ? | 0 > dst_reg +--------------+----------------------------+--------------------------- > | non-negative | 0 | 0 > > This leave the negative range & negative range case to be considered. We > know that negative range & negative range always yield a negative value, > so a preliminary guess would be S64_MIN. However, that guess is too > imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern > we're trying to deal with here. > > This can be further improve with the observation that for negative range > & negative range, the smallest possible value must be one that has > longest _common_ most-significant set '1' bits sequence, thus we can use > min(dst_reg->smin_value, src->smin_value) as the starting point, as the > smaller value will be the one with the shorter most-significant set '1' > bits sequence. But that alone is not enough, as we do not know whether > rest of the bits would be set, so the safest guess would be one that > clear alls bits after the most-significant set '1' bits sequence, > something akin to bit_floor(), but for rounding to a negative power-of-2 > instead. > > negative_bit_floor(0xffff000000000003) == 0xffff000000000000 > negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000 > negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000 > > With negative range & negative range solve, we now have: > > | src_reg > smin = ? +----------------------------+--------------------------- > | negative | non-negative > ---------+--------------+----------------------------+--------------------------- > | negative |negative_bit_floor( | 0 > | | min(dst->smin, src->smin))| > dst_reg +--------------+----------------------------+--------------------------- > | non-negative | 0 | 0 > > This can be further simplied since min(dst->smin, src->smin) < 0 when both > dst_reg and src_reg have a negative range. Which means using > > negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value) > > to calculate the resulting smin_value would work across all sign combinations. > > Together these allows us to infer the signed range of the result of BPF_AND > operation using the signed range from its operands. > > [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/ > > Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/ > Cc: Eduard Zingerman <eddyz87@gmail.com> > Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com> > --- > kernel/bpf/verifier.c | 62 +++++++++++++++++++++++++++++-------------- > 1 file changed, 42 insertions(+), 20 deletions(-) > > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c > index 8da132a1ef28..6d4cdf30cd76 100644 > --- a/kernel/bpf/verifier.c > +++ b/kernel/bpf/verifier.c > @@ -13466,6 +13466,39 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg, > } > } > > +/* Clears all trailing bits after the most significant unset bit. > + * > + * Used for estimating the minimum possible value after BPF_AND. This > + * effectively rounds a negative value down to a negative power-of-2 value > + * (except for -1, which just return -1) and returning 0 for non-negative > + * values. E.g. masked32_negative(0xff0ff0ff) == 0xff000000. > + */ > +static inline s32 negative32_bit_floor(s32 v) > +{ > + /* XXX: per C standard section 6.5.7 right shift of signed negative > + * value is implementation-defined. Should unsigned type be used here > + * instead? > + */ > + v &= v >> 1; > + v &= v >> 2; > + v &= v >> 4; > + v &= v >> 8; > + v &= v >> 16; > + return v; > +} > + > +/* Same as negative32_bit_floor() above, but for 64-bit signed value */ > +static inline s64 negative_bit_floor(s64 v) > +{ > + v &= v >> 1; > + v &= v >> 2; > + v &= v >> 4; > + v &= v >> 8; > + v &= v >> 16; > + v &= v >> 32; > + return v; > +} > + > static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, > struct bpf_reg_state *src_reg) > { > @@ -13485,16 +13518,10 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, > dst_reg->u32_min_value = var32_off.value; > dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val); > > - /* Safe to set s32 bounds by casting u32 result into s32 when u32 > - * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded. > - */ > - if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) { > - dst_reg->s32_min_value = dst_reg->u32_min_value; > - dst_reg->s32_max_value = dst_reg->u32_max_value; > - } else { > - dst_reg->s32_min_value = S32_MIN; > - dst_reg->s32_max_value = S32_MAX; > - } > + /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */ > + dst_reg->s32_min_value = negative32_bit_floor(min(dst_reg->s32_min_value, > + src_reg->s32_min_value)); > + dst_reg->s32_max_value = max(dst_reg->s32_max_value, src_reg->s32_max_value); > } > > static void scalar_min_max_and(struct bpf_reg_state *dst_reg, > @@ -13515,16 +13542,11 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg, > dst_reg->umin_value = dst_reg->var_off.value; > dst_reg->umax_value = min(dst_reg->umax_value, umax_val); > > - /* Safe to set s64 bounds by casting u64 result into s64 when u64 > - * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded. > - */ > - if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) { > - dst_reg->smin_value = dst_reg->umin_value; > - dst_reg->smax_value = dst_reg->umax_value; > - } else { > - dst_reg->smin_value = S64_MIN; > - dst_reg->smax_value = S64_MAX; > - } > + /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */ > + dst_reg->smin_value = negative_bit_floor(min(dst_reg->smin_value, > + src_reg->smin_value)); > + dst_reg->smax_value = max(dst_reg->smax_value, src_reg->smax_value); > + > /* We may learn something more from the var_off */ > __update_reg_bounds(dst_reg); > } > -- > 2.45.2 > Apologies for the late response and thank you for CCing us Shung-Hsi. The patch itself seems well thought out and looks correct. Great work! We quickly checked your patch using Agni [1], and were not able to find any violations. That is, given well-formed register state inputs to adjust_scalar_min_max_vals, the new algorithm always produces sound outputs for the BPF_AND (both 32/64) instruction. It looks like you already performed tests with Z3, and Eduard performed a brute force testing using 6-bit integers. Agni's result stands as an additional stronger guarantee because Agni generates SMT formulas directly from the C source code of the verifier and checks the correctness in Z3 without any external library functions, it uses full 64-bit size bitvectors in the formulas generated and considers the correctness for 64-bit integer inputs, and finally it considers the correctness of the *final* output abstract values generated after running update_reg_bounds() and reg_bounds_sync(). Using Agni's encodings we were also quickly able to check the precision of the new algorithm. An algorithm is more precise if it produces tighter range bounds, while being correct. We are happy to note that the new algorithm produces outputs that are at least as precise or more precise than the old algorithm, for all well-formed register state inputs. Best, Hari [1] https://github.com/bpfverif/agni
Hi Harishankar, On Sun, Jul 28, 2024 at 06:38:40PM GMT, Harishankar Vishwanathan wrote: > On Tue, Jul 16, 2024 at 10:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote: > > This commit teach the BPF verifier how to infer signed ranges directly > > from signed ranges of the operands to prevent verifier rejection, which > > is needed for the following BPF program's no-alu32 version, as shown by > > Xu Kuohai: [...] > Apologies for the late response and thank you for CCing us Shung-Hsi. > > The patch itself seems well thought out and looks correct. Great work! Thanks! :) > We quickly checked your patch using Agni [1], and were not able to find any > violations. That is, given well-formed register state inputs to > adjust_scalar_min_max_vals, the new algorithm always produces sound outputs > for the BPF_AND (both 32/64) instruction. That is great to hear and really boost the level of confidence. Though I did made an update[1] to the patch such that implementation of negative_bit_floor() is change from v &= v >> 1; v &= v >> 2; v &= v >> 4; v &= v >> 8; v &= v >> 16; v &= v >> 32; return v; to one that closer resembles tnum_range() u8 bits = fls64(~v); /* find most-significant unset bit */ u64 delta; /* special case, needed because 1ULL << 64 is undefined */ if (bits > 63) return 0; delta = (1ULL << bits) - 1; return ~delta; My understanding is that the two implementations should return the same output for the same input, so overall the deduction remains the same. And my simpler test with Z3 does not find violation in the new implementation. But it would be much better if we can have Agni check the new implementation for violation as well. Speak of which, would you and others involved in checking this patch be comfortable with adding a formal acknowledgment[2] for the patch so this work can be credited in the git repo as well? (i.e. usually replying with an Acked-by, other alternatives are Reviewed-by and Tested-by) IMHO the work done here is in the realm of Reviewed-by, but that itself comes with other implications[3], which may or may not be wanted depending on individual's circumstances. I'll probably post the updated patch out next week, changing only the comments in [1]. > It looks like you already performed tests with Z3, and Eduard performed a > brute force testing using 6-bit integers. Agni's result stands as an > additional stronger guarantee because Agni generates SMT formulas directly > from the C source code of the verifier and checks the correctness in Z3 > without any external library functions, it uses full 64-bit size bitvectors > in the formulas generated and considers the correctness for 64-bit integer > inputs, and finally it considers the correctness of the *final* output > abstract values generated after running update_reg_bounds() and > reg_bounds_sync(). I had some vague ideas that Agni provides better guarantee, but did not know exactly what they are. Thanks for the clear explanation on the additional guarantee Agni provides; its especially assuring to know that update_reg_bounds() and reg_bounds_sync() have been taken into account. > Using Agni's encodings we were also quickly able to check the precision of > the new algorithm. An algorithm is more precise if it produces tighter > range bounds, while being correct. We are happy to note that the new > algorithm produces outputs that are at least as precise or more precise > than the old algorithm, for all well-formed register state inputs. That is great to hear as well. I really should try Agni myself, hope I could find time in the near future. Cheers, Shung-Hsi 1: https://lore.kernel.org/bpf/20240719081702.137173-1-shung-hsi.yu@suse.com/ 2: https://www.kernel.org/doc/html/v6.9/process/submitting-patches.html#when-to-use-acked-by-cc-and-co-developed-by 3: https://www.kernel.org/doc/html/v6.9/process/submitting-patches.html#reviewer-s-statement-of-oversight
On Tue, Jul 30, 2024 at 12:26 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote: [...] > That is great to hear and really boost the level of confidence. Though I > did made an update[1] to the patch such that implementation of > negative_bit_floor() is change from > > v &= v >> 1; > v &= v >> 2; > v &= v >> 4; > v &= v >> 8; > v &= v >> 16; > v &= v >> 32; > return v; > > to one that closer resembles tnum_range() > > u8 bits = fls64(~v); /* find most-significant unset bit */ > u64 delta; > > /* special case, needed because 1ULL << 64 is undefined */ > if (bits > 63) > return 0; > > delta = (1ULL << bits) - 1; > return ~delta; > This [1] is indeed the version of the patch that we checked: the one that uses fls and fls64 in negative_bit_floor and negative32_bit_floor . I replied here because you had CCed us in this thread. Note that for checking in Agni, the implementation of fls and fls64 were borrowed from asm-generic [2,3,4]. Having said that, the patch [1] looks good to me. Tested-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com> [1]: https://lore.kernel.org/bpf/20240719081702.137173-1-shung-hsi.yu@suse.com/ [2]: https://elixir.bootlin.com/linux/v6.10/source/include/asm-generic/bitops/fls.h#L43 [3]: https://elixir.bootlin.com/linux/v6.10/source/include/asm-generic/bitops/fls64.h#L19 [4]: https://elixir.bootlin.com/linux/v6.10/source/include/asm-generic/bitops/__fls.h#L45
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index 8da132a1ef28..6d4cdf30cd76 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -13466,6 +13466,39 @@ static void scalar_min_max_mul(struct bpf_reg_state *dst_reg, } } +/* Clears all trailing bits after the most significant unset bit. + * + * Used for estimating the minimum possible value after BPF_AND. This + * effectively rounds a negative value down to a negative power-of-2 value + * (except for -1, which just return -1) and returning 0 for non-negative + * values. E.g. masked32_negative(0xff0ff0ff) == 0xff000000. + */ +static inline s32 negative32_bit_floor(s32 v) +{ + /* XXX: per C standard section 6.5.7 right shift of signed negative + * value is implementation-defined. Should unsigned type be used here + * instead? + */ + v &= v >> 1; + v &= v >> 2; + v &= v >> 4; + v &= v >> 8; + v &= v >> 16; + return v; +} + +/* Same as negative32_bit_floor() above, but for 64-bit signed value */ +static inline s64 negative_bit_floor(s64 v) +{ + v &= v >> 1; + v &= v >> 2; + v &= v >> 4; + v &= v >> 8; + v &= v >> 16; + v &= v >> 32; + return v; +} + static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, struct bpf_reg_state *src_reg) { @@ -13485,16 +13518,10 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg, dst_reg->u32_min_value = var32_off.value; dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val); - /* Safe to set s32 bounds by casting u32 result into s32 when u32 - * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded. - */ - if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) { - dst_reg->s32_min_value = dst_reg->u32_min_value; - dst_reg->s32_max_value = dst_reg->u32_max_value; - } else { - dst_reg->s32_min_value = S32_MIN; - dst_reg->s32_max_value = S32_MAX; - } + /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */ + dst_reg->s32_min_value = negative32_bit_floor(min(dst_reg->s32_min_value, + src_reg->s32_min_value)); + dst_reg->s32_max_value = max(dst_reg->s32_max_value, src_reg->s32_max_value); } static void scalar_min_max_and(struct bpf_reg_state *dst_reg, @@ -13515,16 +13542,11 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg, dst_reg->umin_value = dst_reg->var_off.value; dst_reg->umax_value = min(dst_reg->umax_value, umax_val); - /* Safe to set s64 bounds by casting u64 result into s64 when u64 - * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded. - */ - if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) { - dst_reg->smin_value = dst_reg->umin_value; - dst_reg->smax_value = dst_reg->umax_value; - } else { - dst_reg->smin_value = S64_MIN; - dst_reg->smax_value = S64_MAX; - } + /* Rough estimate tuned for [-1, 0] & -CONSTANT cases. */ + dst_reg->smin_value = negative_bit_floor(min(dst_reg->smin_value, + src_reg->smin_value)); + dst_reg->smax_value = max(dst_reg->smax_value, src_reg->smax_value); + /* We may learn something more from the var_off */ __update_reg_bounds(dst_reg); }
This commit teach the BPF verifier how to infer signed ranges directly from signed ranges of the operands to prevent verifier rejection, which is needed for the following BPF program's no-alu32 version, as shown by Xu Kuohai: SEC("lsm/bpf_map") int BPF_PROG(check_access, struct bpf_map *map, fmode_t fmode) { if (map != (struct bpf_map *)&data_input) return 0; if (fmode & FMODE_WRITE) return -EACCES; return 0; } Where the relevant verifer log upon rejection are: ... 5: (79) r0 = *(u64 *)(r1 +8) ; R0_w=scalar() R1=ctx() ; if (fmode & FMODE_WRITE) @ test_libbpf_get_fd_by_id_opts.c:32 6: (67) r0 <<= 62 ; R0_w=scalar(smax=0x4000000000000000,umax=0xc000000000000000,smin32=0,smax32=umax32=0,var_off=(0x0; 0xc000000000000000)) 7: (c7) r0 s>>= 63 ; R0_w=scalar(smin=smin32=-1,smax=smax32=0) ; @ test_libbpf_get_fd_by_id_opts.c:0 8: (57) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) 9: (95) exit This sequence of instructions comes from Clang's transformation located in DAGCombiner::SimplifySelectCC() method, which combined the "fmode & FMODE_WRITE" check with the return statement without needing BPF_JMP at all. See Eduard's comment for more detail of this transformation[0]. While the verifier can correctly infer that the value of r0 is in a tight [-1, 0] range after instruction "r0 s>>= 63", is was not able to come up with a tight range for "r0 &= -13" (which would be [-13, 0]), and instead inferred a very loose range: r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0) r0 &= -13 ; R0_w=scalar(smax=0x7ffffffffffffff3,umax=0xfffffffffffffff3,smax32=0x7ffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) The reason is that scalar*_min_max_add() mainly relies on tnum for interring value in register after BPF_AND, however [-1, 0] cannot be tracked precisely with tnum, and effectively turns into [0, -1] (i.e. tnum_unknown). So upon BPF_AND the resulting tnum is equivalent to dst_reg->var_off = tnum_and(tnum_unknown, tnum_const(-13)) And from there the BPF verifier was only able to infer smin=S64_MIN, smax=0x7ffffffffffffff3, which is outside of the expected [-4095, 0] range for return values, and thus the program was rejected. To allow verification of such instruction pattern, update scalar*_min_max_and() to infer signed ranges directly from signed ranges of the operands. With BPF_AND, the resulting value always gains more unset '0' bit, thus it only move towards 0x0000000000000000. The difficulty lies with how to deal with signs. While non-negative (positive and zero) value simply grows smaller, a negative number can grows smaller, but may also underflow and become a larger value. To better address this situation we split the signed ranges into negative range and non-negative range cases, ignoring the mixed sign cases for now; and only consider how to calculate smax_value. Since negative range & negative range preserve the sign bit, so we know the result is still a negative value, thus it only move towards S64_MIN, but never underflow, thus a save bet is to use a value in ranges that is closet to 0, thus "max(dst_reg->smax_value, src->smax_value)". For negative range & positive range the sign bit is always cleared, thus we know the resulting is a non-negative, and only moves towards 0, so a safe bet is to use smax_value of the non-negative range. Last but not least, non-negative range & non-negative range is still a non-negative value, and only moves towards 0; however same as the unsigned range case, the maximum is actually capped by the lesser of the two, and thus min(dst_reg->smax_value, src_reg->smax_value); Listing out the above reasoning as a table (dst_reg abbreviated as dst, src_reg abbreviated as src, smax_value abbrivated as smax) we get: | src_reg smax = ? +---------------------------+--------------------------- | negative | non-negative ---------+--------------+---------------------------+--------------------------- | negative | max(dst->smax, src->smax) | src->smax dst_reg +--------------+---------------------------+--------------------------- | non-negative | dst->smax | min(dst->smax, src->smax) However this is quite complicated, luckily it can be simplified given the following observations max(dst_reg->smax_value, src_reg->smax_value) >= src_reg->smax_value max(dst_reg->smax_value, src_reg->smax_value) >= dst_reg->smax_value max(dst_reg->smax_value, src_reg->smax_value) >= min(dst_reg->smax_value, src_reg->smax_value) So we could substitute the cells in the table above all with max(...), and arrive at: | src_reg smax' = ? +---------------------------+--------------------------- | negative | non-negative ---------+--------------+---------------------------+--------------------------- | negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) dst_reg +--------------+---------------------------+--------------------------- | non-negative | max(dst->smax, src->smax) | max(dst->smax, src->smax) Meaning that simply using max(dst_reg->smax_value, src_reg->smax_value) to calculate the resulting smax_value would work across all sign combinations. For smin_value, we know that both non-negative range & non-negative range and negative range & non-negative range both result in a non-negative value, so an easy guess is to use the minimum non-negative value, thus 0. | src_reg smin = ? +----------------------------+--------------------------- | negative | non-negative ---------+--------------+----------------------------+--------------------------- | negative | ? | 0 dst_reg +--------------+----------------------------+--------------------------- | non-negative | 0 | 0 This leave the negative range & negative range case to be considered. We know that negative range & negative range always yield a negative value, so a preliminary guess would be S64_MIN. However, that guess is too imprecise to help with the r0 <<= 62, r0 s>>= 63, r0 &= -13 pattern we're trying to deal with here. This can be further improve with the observation that for negative range & negative range, the smallest possible value must be one that has longest _common_ most-significant set '1' bits sequence, thus we can use min(dst_reg->smin_value, src->smin_value) as the starting point, as the smaller value will be the one with the shorter most-significant set '1' bits sequence. But that alone is not enough, as we do not know whether rest of the bits would be set, so the safest guess would be one that clear alls bits after the most-significant set '1' bits sequence, something akin to bit_floor(), but for rounding to a negative power-of-2 instead. negative_bit_floor(0xffff000000000003) == 0xffff000000000000 negative_bit_floor(0xf0ff0000ffff0000) == 0xf000000000000000 negative_bit_floor(0xfffffb0000000000) == 0xfffff80000000000 With negative range & negative range solve, we now have: | src_reg smin = ? +----------------------------+--------------------------- | negative | non-negative ---------+--------------+----------------------------+--------------------------- | negative |negative_bit_floor( | 0 | | min(dst->smin, src->smin))| dst_reg +--------------+----------------------------+--------------------------- | non-negative | 0 | 0 This can be further simplied since min(dst->smin, src->smin) < 0 when both dst_reg and src_reg have a negative range. Which means using negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value) to calculate the resulting smin_value would work across all sign combinations. Together these allows us to infer the signed range of the result of BPF_AND operation using the signed range from its operands. [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/ Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/ Cc: Eduard Zingerman <eddyz87@gmail.com> Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@suse.com> --- kernel/bpf/verifier.c | 62 +++++++++++++++++++++++++++++-------------- 1 file changed, 42 insertions(+), 20 deletions(-)