Re: [PATCH bpf-next v2 5/9] bpf, verifier: improve signed ranges inference for BPF_AND
From: Eduard Zingerman <eddyz87@gmail.com>
Date: 2024-07-22 07:13:26
Also in:
bpf, linux-security-module
On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote:
From: Shung-Hsi Yu <redacted>
[...]
| 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/ (local)
Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/ (local)
Cc: Eduard Zingerman <eddyz87@gmail.com>
Signed-off-by: Shung-Hsi Yu <redacted>
Acked-by: Xu Kuohai <redacted>
---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@gmail.com> [...]