Received-SPF: pass (google.com: domain of linux-kernel+bounces-125784-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45e3:2400::1 as permitted sender) client-ip=2604:1380:45e3:2400::1;
Precedence: bulk
MIME-Version: 1.0
References: <20240329030119.29995-1-harishankar.vishwanathan@gmail.com>
 <f2e1c5dc6f6ea2c7f046e8673dd364dd14056781.camel@gmail.com>
 <CAM=Ch04JAJDS84xYHFUfjrShwqSSc8gQ5a_sLCoRNAsf6tyjYQ@mail.gmail.com> <CAEf4BzZp69diFeyjUAa8-jbZatDouwSaexwuakJdXHTdHwsBLQ@mail.gmail.com>
In-Reply-To: <CAEf4BzZp69diFeyjUAa8-jbZatDouwSaexwuakJdXHTdHwsBLQ@mail.gmail.com>
From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Date: Sat, 30 Mar 2024 12:35:41 -0400
Message-ID: <CAM=Ch04BBaucesmw0MY5U2bsrtqPAjurLdLkMdxMRMB0OuOtcw@mail.gmail.com>
Subject: Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value tracking
To: Andrii Nakryiko <andrii.nakryiko@gmail.com>
Cc: Eduard Zingerman <eddyz87@gmail.com>, ast@kernel.org, harishankar.vishwanathan@rutgers.edu, 
	sn624@cs.rutgers.edu, sn349@cs.rutgers.edu, m.shachnai@rutgers.edu, 
	paul@isovalent.com, Srinivas Narayana <srinivas.narayana@rutgers.edu>, 
	Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>, Daniel Borkmann <daniel@iogearbox.net>, 
	John Fastabend <john.fastabend@gmail.com>, Andrii Nakryiko <andrii@kernel.org>, 
	Martin KaFai Lau <martin.lau@linux.dev>, Song Liu <song@kernel.org>, 
	Yonghong Song <yonghong.song@linux.dev>, KP Singh <kpsingh@kernel.org>, 
	Stanislav Fomichev <sdf@google.com>, Hao Luo <haoluo@google.com>, Jiri Olsa <jolsa@kernel.org>, 
	bpf@vger.kernel.org, linux-kernel@vger.kernel.org
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

On Sat, Mar 30, 2024 at 1:28=E2=80=AFAM Andrii Nakryiko
<andrii.nakryiko@gmail.com> wrote:
>
> On Fri, Mar 29, 2024 at 8:25=E2=80=AFPM Harishankar Vishwanathan
> <harishankar.vishwanathan@gmail.com> wrote:
> >
> > On Fri, Mar 29, 2024 at 6:27=E2=80=AFAM Eduard Zingerman <eddyz87@gmail=
com> wrote:
> > >
> > > On Thu, 2024-03-28 at 23:01 -0400, Harishankar Vishwanathan wrote:
> > >
> > > [...]
> > >
> > > > @@ -13387,18 +13389,19 @@ static void scalar32_min_max_or(struct bp=
f_reg_state *dst_reg,
> > > >        */
> > > >       dst_reg->u32_min_value =3D max(dst_reg->u32_min_value, umin_v=
al);
> > > >       dst_reg->u32_max_value =3D 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 ">=3D 0" h=
ere?
> > > 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 follow=
ing
> > if condition,
> >
> > if (dst_reg->s32_min_value >=3D 0 && smin_val >=3D 0 &&
> > (s32)dst_reg->u32_min_value <=3D (s32)dst_reg->u32_max_value)
> >
> > it will use this if condition:
> >
> > if ((s32)dst_reg->u32_min_value <=3D (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 t=
o
> > 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 unbound=
ed
[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 <=3D (s32)dst_reg->u32_ma=
x_value) {
> > > > +             /* ORing two positives gives a positive, so safe to c=
ast
> > > > +              * u32 result into s32 when u32 doesn't cross sign bo=
undary.
> > > > +              */
> > > > +             dst_reg->s32_min_value =3D dst_reg->u32_min_value;
> > > > +             dst_reg->s32_max_value =3D 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 =3D S32_MIN;
> > > >               dst_reg->s32_max_value =3D S32_MAX;
> > > > -     } else {
> > > > -             /* ORing two positives gives a positive, so safe to
> > > > -              * cast result into s64.
> > > > -              */
> > > > -             dst_reg->s32_min_value =3D dst_reg->u32_min_value;
> > > > -             dst_reg->s32_max_value =3D dst_reg->u32_max_value;
> > > >       }
> > > >  }
> > >
> > > [...]
> > >
> > > > @@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct b=
pf_reg_state *dst_reg,
> > > >       /* We get both minimum and maximum from the var32_off. */
> > > >       dst_reg->u32_min_value =3D var32_off.value;
> > > >       dst_reg->u32_max_value =3D var32_off.value | var32_off.mask;
> > > > -
> > > > -     if (dst_reg->s32_min_value >=3D 0 && smin_val >=3D 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 <=3D (s32)dst_reg->u32_ma=
x_value) {
> > > > +             /* XORing two positives gives a positive, so safe to =
cast
> > > > +              * u32 result into s32 when u32 doesn't cross sign bo=
undary.
> > > >                */
> > > >               dst_reg->s32_min_value =3D dst_reg->u32_min_value;
> > > >               dst_reg->s32_max_value =3D dst_reg->u32_max_value;
> > >
> > > [...]