Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester - Shung-Hsi Yu

From: Shung-Hsi Yu <shung-hsi.yu@suse.com>
To: Andrii Nakryiko <andrii.nakryiko@gmail.com>
Cc: Andrii Nakryiko <andrii@kernel.org>,
	Langston Barrett <langston.barrett@gmail.com>,
	Srinivas Narayana <srinivas.narayana@rutgers.edu>,
	Santosh Nagarakatte <santosh.nagarakatte@cs.rutgers.edu>,
	bpf@vger.kernel.org, ast@kernel.org, daniel@iogearbox.net,
	martin.lau@kernel.org, kernel-team@meta.com
Subject: Re: [PATCH v2 bpf-next 7/7] selftests/bpf: BPF register range bounds tester
Date: Fri, 20 Oct 2023 20:27:32 +0800	[thread overview]
Message-ID: <ZTJyNJ44ekEdazfS@u94a> (raw)
In-Reply-To: <CAEf4Bzad+jgPWQ37VM5JOw4GPHbjZpJrxmRsFs8N0MqeMHyLSA@mail.gmail.com>

On Thu, Oct 19, 2023 at 11:31:55AM -0700, Andrii Nakryiko wrote:
> On Thu, Oct 19, 2023 at 12:30 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > On Wed, Oct 18, 2023 at 09:24:05PM -0700, Andrii Nakryiko wrote:
> > > Add tests that validate correctness and completeness of BPF verifier's
> > > register range bounds.
> >
> > Nitpick: in abstract-interpretation-speak, completeness seems to mean
> > something different. I believe what we're trying to check here is
> > soundness[1], again, in abstraction-interpretation-speak), so using
> > completeness here may be misleading to some. (I'll leave explanation to
> > other that understand this concept better than I do, rather than making an
> > ill attempt that would probably just make things worst)
> 
> I'll just say "Add test to validate BPF verifier's register range
> bounds tracking logic." to avoid terminology hazards :)

Sounds good to me :)

> > > The main bulk is a lot of auto-generated tests based on a small set of
> > > seed values for lower and upper 32 bits of full 64-bit values.
> > > Currently we validate only range vs const comparisons, but the idea is
> > > to start validating range over range comparisons in subsequent patch set.
> >
> > CC Langston Barrett who had previously send kunit-based tnum checks[2] a
> > while back. If this patch is merged, perhaps we can consider adding
> > validation for tnum as well in the future using similar framework.
> >
> > More comments below
> >
> > > When setting up initial register ranges we treat registers as one of
> > > u64/s64/u32/s32 numeric types, and then independently perform conditional
> > > comparisons based on a potentially different u64/s64/u32/s32 types. This
> > > tests lots of tricky cases of deriving bounds information across
> > > different numeric domains.
> > >
> > > Given there are lots of auto-generated cases, we guard them behind
> > > SLOW_TESTS=1 envvar requirement, and skip them altogether otherwise.
> > > With current full set of upper/lower seed value, all supported
> > > comparison operators and all the combinations of u64/s64/u32/s32 number
> > > domains, we get about 7.7 million tests, which run in about 35 minutes
> > > on my local qemu instance. So it's something that can be run manually
> > > for exhaustive check in a reasonable time, and perhaps as a nightly CI
> > > test, but certainly is too slow to run as part of a default test_progs run.
> >
> > FWIW an alternative approach that speeds things up is to use model checkers
> > like Z3 or CBMC. On my laptop, using Z3 to validate tnum_add() against *all*
> > possible inputs takes less than 1.3 seconds[3] (based on code from [1]
> > paper, but I somehow lost the link to their GitHub repository).
> >
> > One of the potential issue with [3] is that Z3Py is written in Python. So
> > there's the large over head of translating the C-implementation into Python
> > using Z3Py APIs each time we changed relevant code. This overhead could
> > potentially be removed with CBMC, which understand C, and we had a
> > precedence of using CBMC[4] within the kernel source code, though it was
> > later removed[5] due because SRCU changes are still happening too fast for
> > the format tests to keep up, so it looks like CBMC is not a silver-bullet.
> >
> > I really meant to look into the CMBC approach for verification of ranges and
> > tnum, but fails to allocate time for it, so far.
> 
> It would be great if someone did a proper model checker-based
> verification of range tracking logic of overall BPF verifier logic,
> agreed. Until we have that (and depending on how easy it is to
> integrate that approach into BPF CI), I think having something as part
> of test_progs is a good practical step forward.

Agree, by no mean was I trying to suggest we shouldn't have this test.
Mainly want to bring up checker-based verification, and was glad to hear
that it is considered worth investigating.

> > Shung-Hsi
> >
> > > ...
> >
> > 1: https://people.cs.rutgers.edu/~sn349/papers/cgo-2022.pdf
> > 2: https://lore.kernel.org/bpf/20220430215727.113472-1-langston.barrett@gmail.com/
> > 3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e
> > 4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@linux.vnet.ibm.com/