Received-SPF: pass (google.com: domain of linux-kernel+bounces-130841-linux.lists.archive=gmail.com@vger.kernel.org designates 147.75.80.249 as permitted sender) client-ip=147.75.80.249;
Precedence: bulk
MIME-Version: 1.0
References: <20240402212039.51815-1-harishankar.vishwanathan@gmail.com> <77f5c5ed-881e-c9a8-cfdb-200c322fb55d@amd.com>
In-Reply-To: <77f5c5ed-881e-c9a8-cfdb-200c322fb55d@amd.com>
From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Date: Wed, 3 Apr 2024 22:40:23 -0400
Message-ID: <CAM=Ch04xd5u75UFeQwVrzP7=A5KPAw3x7_drqQHK3C-43T4T2w@mail.gmail.com>
Subject: Re: [PATCH v2 bpf-next] bpf: Fix latent unsoundness in and/or/xor
 value tracking
To: Edward Cree <ecree@amd.com>
Cc: ast@kernel.org, harishankar.vishwanathan@rutgers.edu, paul@isovalent.com, 
	Matan Shachnai <m.shachnai@rutgers.edu>, 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>, 
	"David S. Miller" <davem@davemloft.net>, bpf@vger.kernel.org, linux-kernel@vger.kernel.org, 
	Edward Cree <ecree.xilinx@gmail.com>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

On Wed, Apr 3, 2024 at 9:25=E2=80=AFAM Edward Cree <ecree@amd.com> wrote:
>
> 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 restri=
cts
> > its inputs to those passing through reg_bounds_sync(). This mimics
> > real-world verifier behavior, as reg_bounds_sync() is invariably execut=
ed
> > 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 bou=
nds
> > such that smin_value > smax_value. This patch fixes it, making the abst=
ract
> > operator sound for all (well-formed) inputs.
>
> Just to check I'm understanding correctly: you're saying that the existin=
g
>  code has an undocumented precondition, that's currently maintained by th=
e
>  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 t=
o
>  backport this change to stable kernels, although I agree the change is
>  worth making in -next.

You are kind of right on both counts.

The existing code contains an undocumented precondition. When violated,
scalar_min_max_and() can produce unsound s64 bounds (where smin > smax).
Certain well-formed register state inputs can violate this precondition,
resulting in eventual unsoundness. However, register states that have
passed through reg_bounds_sync() -- or those that are completely known or
completely unknown -- satisfy the precondition, preventing unsoundness.

Since we haven=E2=80=99t examined all possible paths through the verifier, =
and we
cannot guarantee that every instruction preceding a BPF_AND in an eBPF
program will maintain the precondition, we cannot definitively say that
register state inputs to scalar_min_max_and() will always meet the
precondition. There is a potential for an invocation of
scalar_min_max_and() on a register state that hasn=E2=80=99t undergone
reg_bounds_sync(). The patch indeed removes the precondition.

Given the above, please advise if we should backport this patch to older
kernels (and whether I should use the fixes tag).

> > It is worth noting that we can update the signed bounds using the unsig=
ned
> > 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 whethe=
r
>  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).

Sounds good regarding making it clearer within the context of what the
existing code does. However, I wanted to clarify that XOR does indeed use
the same handling as all the other operations. Could you elaborate on what
you mean?

> > 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_r=
eg_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 inherent=
ly
> >          * bitwise.  Our maximum is the minimum of the operands' maxima=
.
> >          */
>
> This change, adjusting a comment to match the existing code, should proba=
bly
>  be in a separate patch.

Sounds good.

> > @@ -13395,23 +13391,21 @@ static void scalar32_min_max_or(struct bpf_re=
g_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 th=
e
> > +        * maximum of the operands' minima.
> >          */
>
> Same here.
>
> Apart from that,
> Acked-by: Edward Cree <ecree.xilinx@gmail.com>