Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value tracking
From: Harishankar Vishwanathan
Date: Sat Mar 30 2024 - 12:36:02 EST
On Sat, Mar 30, 2024 at 1:28 AM Andrii Nakryiko
<andrii.nakryiko@xxxxxxxxx> wrote:
>
> On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
> <harishankar.vishwanathan@xxxxxxxxx> wrote:
> >
> > On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@gmailcom> wrote:
> > >
> > > On Thu, 2024-03-28 at 23:01 -0400, Harishankar Vishwanathan wrote:
> > >
> > > [...]
> > >
> > > > @@ -13387,18 +13389,19 @@ static void scalar32_min_max_or(struct bpf_reg_state *dst_reg,
> > > > */
> > > > dst_reg->u32_min_value = max(dst_reg->u32_min_value, umin_val);
> > > > dst_reg->u32_max_value = var32_off.value | var32_off.mask;
> > > > - if (dst_reg->s32_min_value < 0 || smin_val < 0) {
> > > > + if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
> > >
> > > Hello,
> > >
> > > Could you please elaborate a bit, why do you use "> 0" not ">= 0" here?
> > > It seems that having one of the min values as 0 shouldn't be an issue,
> > > but maybe I miss something.
> >
> > You are right, this is a mistake, I sent the wrong version of the patch Thanks
> > for catching it. I will send a new patch.
> >
> > Note that in the correct version i'll be sending, instead of the following
> > if condition,
> >
> > if (dst_reg->s32_min_value >= 0 && smin_val >= 0 &&
> > (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value)
> >
> > it will use this if condition:
> >
> > if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value)
> >
> > Inside the if, the output signed bounds are updated using the unsigned
> > bounds; the only case in which this is unsafe is when the unsigned
> > bounds cross the sign boundary. The shortened if condition is enough to
> > prevent this. The shortened has the added benefit of being more
> > precise. We will make a note of this in the new commit message.
>
> And that's exactly what reg_bounds_sync() checks as well, which is why
> my question/suggestion to not duplicate this logic, rather reset s32
> bounds to unknown (S32_MIN/S32_MAX), and let generic reg_bounds_sync()
> handle the re-derivation of whatever can be derived.
We tried your suggestion (setting the bounds to be completely unbounded).
This would indeed make the abstract operator scalar(32)_min_max_and
sound. However, we found (through Agni and SMT verification) that our patch is
more precise than just unconditionally setting the signed bounds to unbounded
[S32_MIN/S32_MAX], [S64_MIN,S64_MAX].
For example, consider these inputs to BPF_AND:
dst_reg
-----------------------------------------
var_off.value: 8608032320201083347
var_off.mask: 615339716653692460
smin_value: 8070450532247928832
smax_value: 8070450532247928832
umin_value: 13206380674380886586
umax_value: 13206380674380886586
s32_min_value: -2110561598
s32_max_value: -133438816
u32_min_value: 4135055354
u32_max_value: 4135055354
src_reg
-----------------------------------------
var_off.value: 8584102546103074815
var_off.mask: 9862641527606476800
smin_value: 2920655011908158522
smax_value: 7495731535348625717
umin_value: 7001104867969363969
umax_value: 8584102543730304042
s32_min_value: -2097116671
s32_max_value: 71704632
u32_min_value: 1047457619
u32_max_value: 4268683090
After going through
tnum_and() -> scalar32_min_max_and() -> scalar_min_max_and() ->
reg_bounds_sync()
Our patch produces the following bounds for s32:
s32_min_value: -1263875629
s32_max_value: -159911942
Whereas, setting the signed bounds to unbounded in
scalar(32)_min_max_and produces:
s32_min_value: -1263875629
s32_max_value: -1
Our patch produces a tighter bound as you can see. We also confirmed
using SMT that
our patch always produces signed bounds that are equal to or more
precise than setting
the signed bounds to unbounded in scalar(32)_min_max_and.
Admittedly, this is a contrived example. It is likely the case that
such precision
gains are never realized in an actual BPF program.
Overall, both the fixes are sound. We're happy to send a patch for
either of them.
> >
> > This applies to all scalar(32)_min_max_and/or/xor.
> >
> > > > + (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > > > + /* ORing 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 ORing negative numbers,
> > > > * ain't nobody got time for that.
> > > > */
> > > > dst_reg->s32_min_value = S32_MIN;
> > > > dst_reg->s32_max_value = S32_MAX;
> > > > - } else {
> > > > - /* ORing 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;
> > > > }
> > > > }
> > >
> > > [...]
> > >
> > > > @@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
> > > > /* We get both minimum and maximum from the var32_off. */
> > > > dst_reg->u32_min_value = var32_off.value;
> > > > dst_reg->u32_max_value = var32_off.value | var32_off.mask;
> > > > -
> > > > - if (dst_reg->s32_min_value >= 0 && smin_val >= 0) {
> > > > - /* XORing two positive sign numbers gives a positive,
> > > > - * so safe to cast u32 result into s32.
> > > > + if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
> > >
> > > Same question here.
> > >
> > > > + (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > > > + /* XORing 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;
> > >
> > > [...]