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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <hjovxjcwishjy6mwqxz42ek5qhs626udfmmnnasmbj3mlb7mlr@fjbedhdsetjc>
Date: Tue, 9 Apr 2024 21:16:23 +0800
From: Shung-Hsi Yu <shung-hsi.yu@...e.com>
To: Edward Cree <ecree@....com>
Cc: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>, 
	ast@...nel.org, 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 Wed, Apr 03, 2024 at 10:40:23PM -0400, Harishankar Vishwanathan wrote:
> On Wed, Apr 3, 2024 at 9:25 AM Edward Cree <ecree@....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 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.
> 
> 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’t 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’t 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).

I suggested the fixes tag to Harishankar in the v1 patchset, admittedly
without a thorough understanding at the same level of above.

However, given smin_value > smax_value is something we check in
reg_bounds_sanity_check(), I would still vote to have the patch
backported to stable (with "Cc: stable@...r.kernel.org"?) even if the
fixes tag is dropped. The overall change should be rather well contained
and isolated for relatively ease of backport; and probably save some
head scratching over the difference of behavior between mainline and
stable.

> [...]