Received-SPF: pass (google.com: domain of linux-kernel+bounces-125475-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>
In-Reply-To: <20240329030119.29995-1-harishankar.vishwanathan@gmail.com>
From: Andrii Nakryiko <andrii.nakryiko@gmail.com>
Date: Fri, 29 Mar 2024 15:19:30 -0700
Message-ID: <CAEf4BzZOxqPTPYAm7VFjqaUsSNVJBdZx-z6dgQdZWFoGNAnJgg@mail.gmail.com>
Subject: Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value tracking
To: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Cc: 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>, Eduard Zingerman <eddyz87@gmail.com>, 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 Thu, Mar 28, 2024 at 8:02=E2=80=AFPM Harishankar Vishwanathan
<harishankar.vishwanathan@gmail.com> wrote:
>
> The scalar(32)_min_max_and/or/xor functions can exhibit unsound behavior
> when setting signed bounds. The following example illustrates the issue f=
or
> scalar_min_max_and(), but it applies to the other functions.
>
> In scalar_min_max_and() the following clause is executed when ANDing
> positive numbers:
>
>                 /* ANDing two positives gives a positive, so safe to
>                  * cast result into s64.
>                  */
>                 dst_reg->smin_value =3D dst_reg->umin_value;
>                 dst_reg->smax_value =3D dst_reg->umax_value;
>
> However, if umin_value and umax_value of dst_reg cross the sign boundary
> (i.e., if (s64)dst_reg->umin_value > (s64)dst_reg->umax_value), then we
> will end up with smin_value > smax_value, which is unsound.
>
> Previous works [1, 2] have discovered and reported this issue. Our tool
> Agni [3] consideres it a false positive. This is because, during the
> verification of the abstract operator scalar_min_max_and(), Agni restrict=
s
> its inputs to those passing through reg_bounds_sync(). This mimics
> real-world verifier behavior, as reg_bounds_sync() is invariably executed
> at the tail of every abstract operator. Therefore, such behavior is
> unlikely in an actual verifier execution.
>
> However, it is still unsound for an abstract operator to exhibit behavior
> where smin_value > smax_value. This patch fixes it, making the abstract
> operator sound for all (well-formed) inputs.
>
> It's worth noting that this patch only modifies the output signed bounds
> (smin/smax_value) in cases where it was previously unsound. As such, ther=
e
> is no change in precision. When the unsigned bounds (umin/umax_value) cro=
ss
> the sign boundary, they shouldn't be used to update  the signed bounds
> (smin/max_value). In only such cases, we set the output signed bounds to
> unbounded [S64_MIN, S64_MAX]. We confirmed through SMT verification that
> the problem occurs if and only if the unsigned bounds cross the sign
> boundary.
>
> [1] https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis=
22.pdf
> [2] https://github.com/bpfverif/agni
> [3] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_12
>
> Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.c=
om>
> ---
>  kernel/bpf/verifier.c | 76 +++++++++++++++++++++++--------------------
>  1 file changed, 40 insertions(+), 36 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index ca6cacf7b42f..9bc4c2b1ca2e 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -13318,18 +13318,19 @@ static void scalar32_min_max_and(struct bpf_reg=
_state *dst_reg,
>          */
>         dst_reg->u32_min_value =3D var32_off.value;
>         dst_reg->u32_max_value =3D min(dst_reg->u32_max_value, umax_val);
> -       if (dst_reg->s32_min_value < 0 || smin_val < 0) {
> +       if (dst_reg->s32_min_value >=3D 0 && smin_val >=3D 0 &&
> +               (s32)dst_reg->u32_min_value < (s32)dst_reg->u32_max_value=
) {
> +               /* ANDing two positives gives a positive, so safe to cast
> +                * u32 result into s32 when u32 doesn't cross sign bounda=
ry.
> +                */
> +               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 ANDing 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 {
> -               /* ANDing 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;
>         }

have you tried just unconditionally setting s32_{min,max}_value to
S32_{MIN,MAX} and letting reg_bounds_sync perform u32/s32 bounds
derivation?

>  }
>

[...]