Date: Wed, 3 Apr 2024 14:25:44 +0100
From: Edward Cree <ecree@....com>
To: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>,
 ast@...nel.org
Cc: harishankar.vishwanathan@...gers.edu, paul@...valent.com,
 Matan Shachnai <m.shachnai@...gers.edu>,
 Srinivas Narayana <srinivas.narayana@...gers.edu>,
 Santosh Nagarakatte <santosh.nagarakatte@...gers.edu>,
 Daniel Borkmann <daniel@...earbox.net>,
 John Fastabend <john.fastabend@...il.com>,
 Andrii Nakryiko <andrii@...nel.org>, Martin KaFai Lau
 <martin.lau@...ux.dev>, Eduard Zingerman <eddyz87@...il.com>,
 Song Liu <song@...nel.org>, Yonghong Song <yonghong.song@...ux.dev>,
 KP Singh <kpsingh@...nel.org>, Stanislav Fomichev <sdf@...gle.com>,
 Hao Luo <haoluo@...gle.com>, Jiri Olsa <jolsa@...nel.org>,
 "David S. Miller" <davem@...emloft.net>, bpf@...r.kernel.org,
 linux-kernel@...r.kernel.org, Edward Cree <ecree.xilinx@...il.com>
Subject: Re: [PATCH v2 bpf-next] bpf: Fix latent unsoundness in and/or/xor
 value tracking

On 4/2/24 22:20, Harishankar Vishwanathan wrote:
> Previous works [1, 2] have discovered and reported this issue. Our tool
> Agni [2, 3] consideres it a false positive. This is because, during the
> verification of the abstract operator scalar_min_max_and(), Agni restricts
> 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 set signed bounds
> such that smin_value > smax_value. This patch fixes it, making the abstract
> operator sound for all (well-formed) inputs.

Just to check I'm understanding correctly: you're saying that the existing
 code has an undocumented precondition, that's currently maintained by the
 callers, and your patch removes the precondition in case a future patch
 (or cosmic rays?) makes a call without satisfying it?
Or is it in principle possible (just "unlikely") for a program to induce
 the current verifier to call scalar_min_max_foo() on a register that
 hasn't been through reg_bounds_sync()?
If the former, I think Fixes: is inappropriate here as there is no need to
 backport this change to stable kernels, although I agree the change is
 worth making in -next.

> It is worth noting that we can update the signed bounds using the unsigned
> bounds whenever the unsigned bounds do not cross the sign boundary (not
> just when the input signed bounds are positive, as was the case
> previously). This patch does exactly that
Commit message could also make clearer that the new code considers whether
 the *output* ubounds cross sign, rather than looking at the input bounds
 as the previous code did.  At first I was confused as to why XOR didn't
 need special handling (since -ve xor -ve is +ve).

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index fcb62300f407..a7404a7d690f 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -13326,23 +13326,21 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
>                 return;
>         }
> 
> -       /* We get our minimum from the var_off, since that's inherently
> +       /* We get our minimum from the var32_off, since that's inherently
>          * bitwise.  Our maximum is the minimum of the operands' maxima.
>          */

This change, adjusting a comment to match the existing code, should probably
 be in a separate patch.
> @@ -13395,23 +13391,21 @@ static void scalar32_min_max_or(struct bpf_reg_state *dst_reg,
>                 return;
>         }
> 
> -       /* We get our maximum from the var_off, and our minimum is the
> -        * maximum of the operands' minima
> +       /* We get our maximum from the var32_off, and our minimum is the
> +        * maximum of the operands' minima.
>          */

Same here.

Apart from that,
Acked-by: Edward Cree <ecree.xilinx@...il.com>

Powered by blists - more mailing lists