Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value tracking

[Andrii Nakryiko]

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@xxxxxxxxx> 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.

>
> 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;
> >
> > [...]