From: Paul Chaignon <paul.chaignon@gmail.com>
To: Andrii Nakryiko <andrii.nakryiko@gmail.com>,
Harishankar Vishwanathan <harishankar.vishwanathan@rutgers.edu>,
Srinivas Narayana <srinivas.narayana@rutgers.edu>
Cc: Alexei Starovoitov <alexei.starovoitov@gmail.com>,
Paul Chaignon <paul@isovalent.com>,
Andrii Nakryiko <andrii@kernel.org>,
bpf@vger.kernel.org, ast@kernel.org, daniel@iogearbox.net,
martin.lau@kernel.org, kernel-team@meta.com
Subject: Re: [PATCH v5 bpf-next 00/23] BPF register bounds logic and testing improvements
Date: Wed, 1 Nov 2023 13:37:37 +0100 [thread overview]
Message-ID: <ZUJGkRGnw+qI15Pv@Mem> (raw)
In-Reply-To: <CAEf4BzZyLwO_ZppGObkY=4aXZEGE+k+tTtJug7MP63DffoxrYA@mail.gmail.com>
On Mon, Oct 30, 2023 at 10:19:01PM -0700, Andrii Nakryiko wrote:
> On Mon, Oct 30, 2023 at 10:55 AM Alexei Starovoitov
> <alexei.starovoitov@gmail.com> wrote:
> >
> > On Fri, Oct 27, 2023 at 11:13:23AM -0700, Andrii Nakryiko wrote:
> > >
> > > Note, this is not unique to <range> vs <range> logic. Just recently ([0])
> > > a related issue was reported for existing verifier logic. This patch set does
> > > fix that issues as well, as pointed out on the mailing list.
> > >
> > > [0] https://lore.kernel.org/bpf/CAEf4Bzbgf-WQSCz8D4Omh3zFdS4oWS6XELnE7VeoUWgKf3cpig@mail.gmail.com/
> >
> > Quick comment regarding shift out of bound issue.
> > I think this patch set makes Hao Sun's repro not working, but I don't think
> > the range vs range improvement fixes the underlying issue.
>
> Correct, yes, I think adjust_reg_min_max_vals() might still need some fixing.
>
> > Currently we do:
> > if (umax_val >= insn_bitness)
> > mark_reg_unknown
> > else
> > here were use src_reg->u32_max_value or src_reg->umax_value
> > I suspect the insn_bitness check is buggy and it's still possible to hit UBSAN splat with
> > out of bounds shift. Just need to try harder.
> > if w8 < 0xffffffff goto +2;
> > if r8 != r6 goto +1;
> > w0 >>= w8;
> > won't be enough anymore.
>
> Agreed, but I felt that fixing adjust_reg_min_max_vals() is out of
> scope for this already large patch set. If someone can take a deeper
> look into reg bounds for arithmetic operations, it would be great.
>
> On the other hand, one of those academic papers claimed to verify
> soundness of verifier's reg bounds, so I wonder why they missed this?
AFAICS, it should have been able to detect this bug. Equation (3) from
[1, page 10] encodes the soundness condition for conditional jumps and
the implementation definitely covers BPF_JEQ/JNE and the logic in
check_cond_jmp_op. So either there's a bug in the implementation or I'm
missing something about how it works. Let me cc two of the paper's
authors :)
Hari, Srinivas: Hao Sun recently discovered a bug in the range analysis
logic of the verifier, when comparing two unknown scalars with
non-overlapping ranges. See [2] for Eduard Zingerman's explanation. It
seems to have existed for a while. Any idea why Agni didn't uncover it?
1 - https://harishankarv.github.io/assets/files/agni-cav23.pdf
2 - https://lore.kernel.org/bpf/8731196c9a847ff35073a2034662d3306cea805f.camel@gmail.com/
> cc Paul, maybe he can clarify (and also, Paul, please try to run all
> that formal verification machinery against this patch set, thanks!)
I tried it yesterday but am running into what looks like a bug in the
LLVM IR to SMT conversion. Probably not something I can fix myself
quickly so I'll need help from Hari & co.
That said, even without your patchset, I'm running into another issue
where the formal verification takes several times longer (up to weeks
/o\) since v6.4.
next prev parent reply other threads:[~2023-11-01 12:37 UTC|newest]
Thread overview: 77+ messages / expand[flat|nested] mbox.gz Atom feed top
2023-10-27 18:13 [PATCH v5 bpf-next 00/23] BPF register bounds logic and testing improvements Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 01/23] selftests/bpf: fix RELEASE=1 build for tc_opts Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 02/23] selftests/bpf: satisfy compiler by having explicit return in btf test Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 03/23] bpf: derive smin/smax from umin/max bounds Andrii Nakryiko
2023-10-31 15:37 ` Eduard Zingerman
2023-10-31 17:30 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 04/23] bpf: derive smin32/smax32 from umin32/umax32 bounds Andrii Nakryiko
2023-10-31 15:37 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 05/23] bpf: derive subreg bounds from full bounds when upper 32 bits are constant Andrii Nakryiko
2023-10-31 15:37 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 06/23] bpf: add special smin32/smax32 derivation from 64-bit bounds Andrii Nakryiko
2023-10-31 15:37 ` Eduard Zingerman
2023-10-31 17:39 ` Andrii Nakryiko
2023-10-31 18:41 ` Alexei Starovoitov
2023-10-31 18:49 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 07/23] bpf: improve deduction of 64-bit bounds from 32-bit bounds Andrii Nakryiko
2023-10-31 15:37 ` Eduard Zingerman
2023-10-31 20:26 ` Alexei Starovoitov
2023-10-31 20:33 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 08/23] bpf: try harder to deduce register bounds from different numeric domains Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 09/23] bpf: drop knowledge-losing __reg_combine_{32,64}_into_{64,32} logic Andrii Nakryiko
2023-10-31 15:38 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 10/23] selftests/bpf: BPF register range bounds tester Andrii Nakryiko
2023-11-08 22:08 ` Eduard Zingerman
2023-11-08 23:23 ` Andrii Nakryiko
2023-11-09 0:30 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 11/23] bpf: rename is_branch_taken reg arguments to prepare for the second one Andrii Nakryiko
2023-10-30 19:39 ` Alexei Starovoitov
2023-10-31 5:19 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 12/23] bpf: generalize is_branch_taken() to work with two registers Andrii Nakryiko
2023-10-31 15:38 ` Eduard Zingerman
2023-10-31 17:41 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 13/23] bpf: move is_branch_taken() down Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 14/23] bpf: generalize is_branch_taken to handle all conditional jumps in one place Andrii Nakryiko
2023-10-31 15:38 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 15/23] bpf: unify 32-bit and 64-bit is_branch_taken logic Andrii Nakryiko
2023-10-30 19:52 ` Alexei Starovoitov
2023-10-31 5:28 ` Andrii Nakryiko
2023-10-31 17:35 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 16/23] bpf: prepare reg_set_min_max for second set of registers Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 17/23] bpf: generalize reg_set_min_max() to handle two sets of two registers Andrii Nakryiko
2023-10-31 2:02 ` Alexei Starovoitov
2023-10-31 6:03 ` Andrii Nakryiko
2023-10-31 16:23 ` Alexei Starovoitov
2023-10-31 17:50 ` Andrii Nakryiko
2023-10-31 17:56 ` Andrii Nakryiko
2023-10-31 18:04 ` Alexei Starovoitov
2023-10-31 18:06 ` Andrii Nakryiko
2023-10-31 18:14 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 18/23] bpf: generalize reg_set_min_max() to handle non-const register comparisons Andrii Nakryiko
2023-10-31 23:25 ` Eduard Zingerman
2023-11-01 16:35 ` Andrii Nakryiko
2023-11-01 17:12 ` Eduard Zingerman
2023-10-27 18:13 ` [PATCH v5 bpf-next 19/23] bpf: generalize is_scalar_branch_taken() logic Andrii Nakryiko
2023-10-31 2:12 ` Alexei Starovoitov
2023-10-31 6:12 ` Andrii Nakryiko
2023-10-31 16:34 ` Alexei Starovoitov
2023-10-31 18:01 ` Andrii Nakryiko
2023-10-31 20:53 ` Andrii Nakryiko
2023-10-31 20:55 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 20/23] bpf: enhance BPF_JEQ/BPF_JNE is_branch_taken logic Andrii Nakryiko
2023-10-31 2:20 ` Alexei Starovoitov
2023-10-31 6:16 ` Andrii Nakryiko
2023-10-31 16:36 ` Alexei Starovoitov
2023-10-31 18:04 ` Andrii Nakryiko
2023-10-31 18:06 ` Alexei Starovoitov
2023-10-27 18:13 ` [PATCH v5 bpf-next 21/23] selftests/bpf: adjust OP_EQ/OP_NE handling to use subranges for branch taken Andrii Nakryiko
2023-11-08 18:22 ` Eduard Zingerman
2023-11-08 19:59 ` Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 22/23] selftests/bpf: add range x range test to reg_bounds Andrii Nakryiko
2023-10-27 18:13 ` [PATCH v5 bpf-next 23/23] selftests/bpf: add iter test requiring range x range logic Andrii Nakryiko
2023-10-30 17:55 ` [PATCH v5 bpf-next 00/23] BPF register bounds logic and testing improvements Alexei Starovoitov
2023-10-31 5:19 ` Andrii Nakryiko
2023-11-01 12:37 ` Paul Chaignon [this message]
2023-11-01 17:13 ` Andrii Nakryiko
2023-11-07 6:37 ` Harishankar Vishwanathan
2023-11-07 16:38 ` Paul Chaignon
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=ZUJGkRGnw+qI15Pv@Mem \
--to=paul.chaignon@gmail.com \
--cc=alexei.starovoitov@gmail.com \
--cc=andrii.nakryiko@gmail.com \
--cc=andrii@kernel.org \
--cc=ast@kernel.org \
--cc=bpf@vger.kernel.org \
--cc=daniel@iogearbox.net \
--cc=harishankar.vishwanathan@rutgers.edu \
--cc=kernel-team@meta.com \
--cc=martin.lau@kernel.org \
--cc=paul@isovalent.com \
--cc=srinivas.narayana@rutgers.edu \
/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 an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.