Received-SPF: pass (google.com: domain of linux-kernel+bounces-136925-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:40f1:3f00::1 as permitted sender) client-ip=2604:1380:40f1:3f00::1;
Date: Tue, 9 Apr 2024 21:16:23 +0800
From: Shung-Hsi Yu <shung-hsi.yu@suse.com>
To: Edward Cree <ecree@amd.com>
Cc: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>, 
	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>
Subject: Re: [PATCH v2 bpf-next] bpf: Fix latent unsoundness in and/or/xor
 value tracking
Message-ID: <hjovxjcwishjy6mwqxz42ek5qhs626udfmmnnasmbj3mlb7mlr@fjbedhdsetjc>
References: <20240402212039.51815-1-harishankar.vishwanathan@gmail.com>
 <77f5c5ed-881e-c9a8-cfdb-200c322fb55d@amd.com>
 <CAM=Ch04xd5u75UFeQwVrzP7=A5KPAw3x7_drqQHK3C-43T4T2w@mail.gmail.com>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Disposition: inline
Content-Transfer-Encoding: 8bit
In-Reply-To: <CAM=Ch04xd5u75UFeQwVrzP7=A5KPAw3x7_drqQHK3C-43T4T2w@mail.gmail.com>

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@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 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@vger.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.

> [...]