netdev - Re: [PATCH bpf-next v2 5/9] bpf, verifier: improve signed ranges inference for BPF

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: <a5afdfca337a59bfe8f730a59ea40cd48d9a3d6b.camel@gmail.com>
Date: Mon, 22 Jul 2024 00:13:20 -0700
From: Eduard Zingerman <eddyz87@...il.com>
To: Xu Kuohai <xukuohai@...weicloud.com>, bpf@...r.kernel.org, 
	netdev@...r.kernel.org, linux-security-module@...r.kernel.org
Cc: Alexei Starovoitov <ast@...nel.org>, Andrii Nakryiko
 <andrii@...nel.org>,  Daniel Borkmann <daniel@...earbox.net>, Shung-Hsi Yu
 <shung-hsi.yu@...e.com>, Yonghong Song <yonghong.song@...ux.dev>, KP Singh
 <kpsingh@...nel.org>, Roberto Sassu <roberto.sassu@...wei.com>, Matt
 Bobrowski <mattbobrowski@...gle.com>,  Yafang Shao <laoar.shao@...il.com>,
 Ilya Leoshkevich <iii@...ux.ibm.com>, "Jose E . Marchesi"
 <jose.marchesi@...cle.com>, James Morris <jamorris@...ux.microsoft.com>, 
 Kees Cook <kees@...nel.org>, Brendan Jackman <jackmanb@...gle.com>, Florent
 Revest <revest@...gle.com>
Subject: Re: [PATCH bpf-next v2 5/9] bpf, verifier: improve signed ranges
 inference for BPF_AND

On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote:
> From: Shung-Hsi Yu <shung-hsi.yu@...e.com>

[...]

> 
>                         |                         src_reg
>        smin' = ?        +----------------------------+---------------------------
>   smin'(r) <= smin(r)   |        negative            |       non-negative
> ---------+--------------+----------------------------+---------------------------
>          |   negative   |negative_bit_floor(         |negative_bit_floor(
>          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> dst_reg  +--------------+----------------------------+---------------------------
>          | non-negative |negative_bit_floor(         |negative_bit_floor(
>          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> 
> Meaning that simply using
> 
>     negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value))
> 
> to calculate the resulting smin_value would work across all sign combinations.
> 
> Together these allows the BPF verifier to infer the signed range of the
> result of BPF_AND operation using the signed range from its operands,
> and use that information
> 
>     r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
>     r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
> 
> [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
> 
> Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
> Cc: Eduard Zingerman <eddyz87@...il.com>
> Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@...e.com>
> Acked-by: Xu Kuohai <xukuohai@...wei.com>
> ---

I find derivation of these new rules logical.
Also tried a simple brute force testing of this algorithm for 6-bit
signed integers, and have not found any constraint violations:
https://github.com/eddyz87/bpf-and-brute-force-check

As a nitpick, I think that it would be good to have some shortened
version of the derivation in the comments alongside the code.
(Maybe with a link to the mailing list).

Acked-by: Eduard Zingerman <eddyz87@...il.com>

[...]