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: <wjvdnep2od4kf3f7fiteh73s4gnktcfsii4lbb2ztvudexiyqw@hxqowhgokxf3>
Date: Mon, 22 Jul 2024 20:57:49 +0800
From: Shung-Hsi Yu <shung-hsi.yu@...e.com>
To: Eduard Zingerman <eddyz87@...il.com>, 
	Xu Kuohai <xukuohai@...weicloud.com>
Cc: bpf@...r.kernel.org, netdev@...r.kernel.org, 
	linux-security-module@...r.kernel.org, Alexei Starovoitov <ast@...nel.org>, 
	Andrii Nakryiko <andrii@...nel.org>, Daniel Borkmann <daniel@...earbox.net>, 
	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 Mon, Jul 22, 2024 at 12:13:20AM GMT, Eduard Zingerman wrote:
> 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

I accidentally left the above paragraph unfinished, it should end with

... and using that information, it can be sure that that the result of
[-1, 0] & -13 will be within that expected range of [-4095, 0].

> >     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

Thanks!

> As a nitpick, I think that it would be good to have some shortened
> version of the derivation in the comments alongside the code.

Agree it would. Will try to add a 2-4 sentence explanation.

> (Maybe with a link to the mailing list).

Adding a link to the mailing list seems out of the usual for comment in
verifier.c though, and it would be quite long. That said, it would be
nice to hint that there exists a more verbose version of the
explanation.

Maybe an explicit "see commit for the full detail" at the end of
the added comment?

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

Will send an update for this tomorrow.