Received-SPF: pass (google.com: domain of linux-kernel+bounces-127994-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:45e3:2400::1 as permitted sender) client-ip=2604:1380:45e3:2400::1;
Subject: Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value
 tracking
To: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>,
 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>,
 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
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>
From: Daniel Borkmann <daniel@iogearbox.net>
Message-ID: <4229e0ff-777b-6afb-f0c0-a329e426d87e@iogearbox.net>
Date: Tue, 2 Apr 2024 15:06:18 +0200
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101
 Thunderbird/60.7.2
Precedence: bulk
MIME-Version: 1.0
In-Reply-To: <CAM=Ch04BBaucesmw0MY5U2bsrtqPAjurLdLkMdxMRMB0OuOtcw@mail.gmail.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit

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