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

[Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>]

On Tue, Apr 2, 2024 at 9:06 AM Daniel Borkmann <daniel@iogearbox.net> wrote:
>
> On 3/30/24 5:35 PM, Harishankar Vishwanathan wrote:
> > On Sat, Mar 30, 2024 at 1:28 AM Andrii Nakryiko
> > <andrii.nakryiko@gmail.com> wrote:
> >>
> >> On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
> >> <harishankar.vishwanathan@gmail.com> wrote:
> >>>
> >>> On Fri, Mar 29, 2024 at 6:27 AM 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 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.
>
> 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