linux-kernel - Re: [PATCH bpf-next] 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]

Date: Fri, 29 Mar 2024 14:34:00 +0800
From: Shung-Hsi Yu <shung-hsi.yu@...e.com>
To: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>
Cc: ast@...nel.org, harishankar.vishwanathan@...gers.edu, 
	sn624@...rutgers.edu, sn349@...rutgers.edu, m.shachnai@...gers.edu, paul@...valent.com, 
	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>, 
	bpf@...r.kernel.org, linux-kernel@...r.kernel.org
Subject: Re: [PATCH bpf-next] Fix latent unsoundness in and/or/xor value
 tracking

On Thu, Mar 28, 2024 at 11:01:19PM -0400, Harishankar Vishwanathan wrote:
> The scalar(32)_min_max_and/or/xor functions can exhibit unsound behavior
> when setting signed bounds. The following example illustrates the issue for
> 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 = dst_reg->umin_value;
> 		dst_reg->smax_value = 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 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 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, there
> is no change in precision. When the unsigned bounds (umin/umax_value) cross
> 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-analysis22.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@...gers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@...gers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@...gers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@...gers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@...gers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@...gers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@...il.com>

I'd suggest adding a fixes tag as well. This seems to go all the way
back to the signed/unsigned split.

Fixed: b03c9f9fdc37 ("bpf/verifier: track signed and unsigned min/max values")

Otherwise

Acked-by: Shung-Hsi Yu <shung-hsi.yu@...e.com>