Received-SPF: pass (google.com: domain of linux-kernel+bounces-128364-linux.lists.archive=gmail.com@vger.kernel.org designates 139.178.88.99 as permitted sender) client-ip=139.178.88.99;
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>
 <CAM=Ch04BBaucesmw0MY5U2bsrtqPAjurLdLkMdxMRMB0OuOtcw@mail.gmail.com> <4229e0ff-777b-6afb-f0c0-a329e426d87e@iogearbox.net>
In-Reply-To: <4229e0ff-777b-6afb-f0c0-a329e426d87e@iogearbox.net>
From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Date: Tue, 2 Apr 2024 12:43:42 -0400
Message-ID: <CAM=Ch04GNCQ0dJQUPXqYotaoSAULXrR5LiF3EjeQOEyq67kyeQ@mail.gmail.com>
Subject: Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value tracking
To: Daniel Borkmann <daniel@iogearbox.net>
Cc: Andrii Nakryiko <andrii.nakryiko@gmail.com>, 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>, 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 Tue, Apr 2, 2024 at 9:06=E2=80=AFAM Daniel Borkmann <daniel@iogearbox.ne=
t> wrote:
>
> On 3/30/24 5:35 PM, Harishankar Vishwanathan wrote:
> > 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@gma=
il.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_=
val);
> >>>>>        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" =
here?
> >>>> It seems that having one of the min values as 0 shouldn't be an issu=
e,
> >>>> but maybe I miss something.
> >>>
> >>> You are right, this is a mistake, I sent the wrong version of the pat=
ch. Thanks
> >>> for catching it. I will send a new patch.
> >>>
> >>> Note that in the correct version i'll be sending, instead of the foll=
owing
> >>> 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 unsigne=
d
> >>> 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 p=
atch is
> > more precise than just unconditionally setting the signed bounds to unb=
ounded
> > [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.
>
> Given your version is more precise, then that would be preferred. Might
> be good to have the above as part of the commit description for future
> reference.
>
> Thanks,
> Daniel

Thanks Shung-Hsi, Eduard, Andrii, Daniel. I'll send over a new version
of the patch addressing
all the points discussed above.

Best,
Hari