On Thu, Mar 28, 2024 at 8:02 PM Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx> wrote: > > The scalar(32)_min_max_and/or/xor functions can exhibit unsound behavior > when setting signed bounds. The following example illustrates the issue for > scalar_min_max_and(), but it applies to the other functions. > > In scalar_min_max_and() the following clause is executed when ANDing > positive numbers: > > /* ANDing two positives gives a positive, so safe to > * cast result into s64. > */ > dst_reg->smin_value = dst_reg->umin_value; > dst_reg->smax_value = dst_reg->umax_value; > > However, if umin_value and umax_value of dst_reg cross the sign boundary > (i.e., if (s64)dst_reg->umin_value > (s64)dst_reg->umax_value), then we > will end up with smin_value > smax_value, which is unsound. > > Previous works [1, 2] have discovered and reported this issue. Our tool > Agni [3] consideres it a false positive. This is because, during the > verification of the abstract operator scalar_min_max_and(), Agni restricts > its inputs to those passing through reg_bounds_sync(). This mimics > real-world verifier behavior, as reg_bounds_sync() is invariably executed > at the tail of every abstract operator. Therefore, such behavior is > unlikely in an actual verifier execution. > > However, it is still unsound for an abstract operator to exhibit behavior > where smin_value > smax_value. This patch fixes it, making the abstract > operator sound for all (well-formed) inputs. > > It's worth noting that this patch only modifies the output signed bounds > (smin/smax_value) in cases where it was previously unsound. As such, there > is no change in precision. When the unsigned bounds (umin/umax_value) cross > the sign boundary, they shouldn't be used to update the signed bounds > (smin/max_value). In only such cases, we set the output signed bounds to > unbounded [S64_MIN, S64_MAX]. We confirmed through SMT verification that > the problem occurs if and only if the unsigned bounds cross the sign > boundary. > > [1] https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf > [2] https://github.com/bpfverif/agni > [3] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_12 > > Co-developed-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx> > Signed-off-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx> > 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: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx> > --- > kernel/bpf/verifier.c | 76 +++++++++++++++++++++++-------------------- > 1 file changed, 40 insertions(+), 36 deletions(-) > > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c > index ca6cacf7b42f..9bc4c2b1ca2e 100644 > --- a/kernel/bpf/verifier.c > +++ b/kernel/bpf/verifier.c > @@ -13318,18 +13318,19 @@ 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); > - if (dst_reg->s32_min_value < 0 || smin_val < 0) { > + if (dst_reg->s32_min_value >= 0 && smin_val >= 0 && > + (s32)dst_reg->u32_min_value < (s32)dst_reg->u32_max_value) { > + /* ANDing two positives gives a positive, so safe to cast > + * u32 result into s32 when u32 doesn't cross sign boundary. > + */ > + dst_reg->s32_min_value = dst_reg->u32_min_value; > + dst_reg->s32_max_value = dst_reg->u32_max_value; > + } else { > /* Lose signed bounds when ANDing negative numbers, > * ain't nobody got time for that. > */ > dst_reg->s32_min_value = S32_MIN; > dst_reg->s32_max_value = S32_MAX; > - } else { > - /* ANDing two positives gives a positive, so safe to > - * cast result into s64. > - */ > - dst_reg->s32_min_value = dst_reg->u32_min_value; > - dst_reg->s32_max_value = dst_reg->u32_max_value; > } have you tried just unconditionally setting s32_{min,max}_value to S32_{MIN,MAX} and letting reg_bounds_sync perform u32/s32 bounds derivation? > } > [...]
