From: Eduard Zingerman <eddyz87@gmail.com>
To: Matan Shachnai <m.shachnai@gmail.com>, ast@kernel.org
Cc: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>,
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>,
Song Liu <song@kernel.org>,
Yonghong Song <yonghong.song@linux.dev>,
KP Singh <kpsingh@kernel.org>,
Stanislav Fomichev <sdf@fomichev.me>,
Hao Luo <haoluo@google.com>, Jiri Olsa <jolsa@kernel.org>,
bpf@vger.kernel.org, linux-kernel@vger.kernel.org
Subject: Re: [PATCH v2] bpf, verifier: Improve precision of BPF_MUL
Date: Wed, 27 Nov 2024 14:53:06 -0800 [thread overview]
Message-ID: <bada6a6b9ab67da9a51a73d3cae36f650c2d48e0.camel@gmail.com> (raw)
In-Reply-To: <20241127074156.17567-1-m.shachnai@gmail.com>
On Wed, 2024-11-27 at 02:41 -0500, Matan Shachnai wrote:
[...]
> In conclusion, with this patch,
>
> 1. We were able to show that we can improve the overall precision of
> BPF_MUL. We proved (using an SMT solver) that this new version of
> BPF_MUL is at least as precise as the current version for all inputs.
>
> 2. We are able to prove the soundness of the new scalar_min_max_mul() and
> scalar32_min_max_mul(). By leveraging the existing proof of tnum_mul
> [1], we can say that the composition of these three functions within
> BPF_MUL is sound.
Hi Matan,
I think this is a nice simplification of the existing code.
Could you please also add a few canary tests in the
tools/testing/selftests/bpf/progs/verifier_bounds.c ?
(e.g. simple case plus possible edge cases).
Something like:
SEC("tc")
__success __log_level(2)
__msg("r6 *= r7 {{.*}}; R6_w=some-range-here")
__naked void mult_mixed_sign(void)
{
asm volatile (
"call %[bpf_get_prandom_u32];"
"r6 = r0;"
"call %[bpf_get_prandom_u32];"
"r7 = r0;"
"r6 &= 0xf;"
"r6 -= 1000000000;"
"r7 &= 0xf;"
"r7 -= 2000000000;"
"r6 *= r7;"
"exit"
:
: __imm(bpf_get_prandom_u32),
__imm(bpf_skb_store_bytes)
: __clobber_all);
}
We usually do this as a separate patch in a patch-set.
Also, it looks like this has limited applicability in practice,
because small negative values denote huge unsigned values,
hence overflow check kicks in for such values.
E.g. no range inferred for [-10,5] * [-20,-5]:
0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar()
1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1)
2: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar()
3: (bf) r7 = r0 ; R0_w=scalar(id=2) R7_w=scalar(id=2)
4: (57) r6 &= 15 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=15,var_off=(0x0; 0xf))
5: (17) r6 -= 10 ; R6_w=scalar(smin=smin32=-10,smax=smax32=5)
6: (57) r7 &= 15 ; R7_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=15,var_off=(0x0; 0xf))
7: (17) r7 -= 20 ; R7_w=scalar(smin=smin32=-20,smax=smax32=-5,umin=0xffffffffffffffec,umax=0xfffffffffffffffb,umin32=0xffffffec,umax32=0xfffffffb,var_off=(0xffffffffffffffe0; 0x1f))
8: (2f) r6 *= r7 ; R6_w=scalar() R7_w=scalar(smin=smin32=-20,smax=smax32=-5,umin=0xffffffffffffffec,umax=0xfffffffffffffffb,umin32=0xffffffec,umax32=0xfffffffb,var_off=(0xffffffffffffffe0; 0x1f))
9: (95) exit
Compared to:
0: R1=ctx() R10=fp0
; asm volatile ( @ verifier_bounds.c:1208
0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar()
1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1)
2: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar()
3: (bf) r7 = r0 ; R0_w=scalar(id=2) R7_w=scalar(id=2)
4: (57) r6 &= 15 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=15,var_off=(0x0; 0xf))
5: (17) r6 -= 1000000000 ; R6_w=scalar(smin=0xffffffffc4653600,smax=0xffffffffc465360f,umin=0xffffffffc4653600,umax=0xffffffffc465360f,smin32=umin32=0xc4653600,smax32=umax32=0xc465360f,var_off=(0xffffffffc4653600; 0xf))
6: (57) r7 &= 15 ; R7_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=15,var_off=(0x0; 0xf))
7: (17) r7 -= 2000000000 ; R7_w=scalar(smin=0xffffffff88ca6c00,smax=0xffffffff88ca6c0f,umin=0xffffffff88ca6c00,umax=0xffffffff88ca6c0f,smin32=umin32=0x88ca6c00,smax32=umax32=0x88ca6c0f,var_off=(0xffffffff88ca6c00; 0xf))
8: (2f) r6 *= r7 ; R6_w=scalar(smax=0x7ffffffffffffeff,umax=0xfffffffffffffeff,smax32=0x7ffffeff,umax32=0xfffffeff,var_off=(0x0; 0xfffffffffffffeff)) R7_w=scalar(smin=0xffffffff88ca6c00,smax=0xffffffff88ca6c0f,umin=0xffffffff88ca6c00,umax=0xffffffff88ca6c0f,smin32=umin32=0x88ca6c00,smax32=umax32=0x88ca6c0f,var_off=(0xffffffff88ca6c00; 0xf))
9: (95) exit
Is it possible to do check_mul_overflow() for signed bounds and
rely on reg_bounds_sync() for unsigned?
[...]
next prev parent reply other threads:[~2024-11-27 22:53 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-11-27 7:41 [PATCH v2] bpf, verifier: Improve precision of BPF_MUL Matan Shachnai
2024-11-27 22:53 ` Eduard Zingerman [this message]
2024-12-02 23:31 ` M Shachnai
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=bada6a6b9ab67da9a51a73d3cae36f650c2d48e0.camel@gmail.com \
--to=eddyz87@gmail.com \
--cc=andrii@kernel.org \
--cc=ast@kernel.org \
--cc=bpf@vger.kernel.org \
--cc=daniel@iogearbox.net \
--cc=haoluo@google.com \
--cc=harishankar.vishwanathan@gmail.com \
--cc=john.fastabend@gmail.com \
--cc=jolsa@kernel.org \
--cc=kpsingh@kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=m.shachnai@gmail.com \
--cc=martin.lau@linux.dev \
--cc=santosh.nagarakatte@rutgers.edu \
--cc=sdf@fomichev.me \
--cc=song@kernel.org \
--cc=srinivas.narayana@rutgers.edu \
--cc=yonghong.song@linux.dev \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox