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

[Shung-Hsi Yu <shung-hsi.yu@suse.com>]

On Sat, Oct 21, 2023 at 09:42:46PM -0700, Andrii Nakryiko wrote:
> On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy
> <sn624@cs.rutgers.edu> wrote:
> >
> > Hi all,
> >
> > Thanks, @Shung-Hsi, for bringing up this conversation about
> > integrating formal verification approaches into the BPF CI and testing.
> >
> > > On 19-Oct-2023, at 1:34 PM, Andrii Nakryiko <andrii.nakryiko@gmail.com> wrote:
> > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > >> On Thu, Oct 19, 2023 at 03:30:33PM +0800, Shung-Hsi Yu 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)
> > >>>
> > >>>> 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).
> > >>
> > >> Found it. For reference, code used in "Sound, Precise, and Fast Abstract
> > >> Interpretation with Tristate Numbers"[1] can be found at
> > >> https://github.com/bpfverif/tnums-cgo22/blob/main/verification/tnum.py
> > >>
> > >> Below is a truncated form of the above that only check tnum_add(), requires
> > >> a package called python3-z3 on most distros:
> > >
> > > Great! I'd be curious to see how range tracking logic can be encoded
> > > using this approach, please give it a go!
> >
> > We have some recent work that applies formal verification approaches
> > to the entirety of range tracking in the eBPF verifier. We posted a
> > note to the eBPF mailing list about it sometime ago:
> >
> > [1] https://lore.kernel.org/bpf/SJ2PR14MB6501E906064EE19F5D1666BFF93BA@SJ2PR14MB6501.namprd14.prod.outlook.com/T/#u
> 
> Oh, I totally missed this, as I just went on a long vacation a few
> days before that and declared email bankruptcy afterwards. I'll try to
> give it a read, though I see lots of math symbols there and make no
> promises ;)

Feels the same when I start reading their previous work, but I can vouch
their work their work are definitely worth the read. (Though I had to admit
I secretly chant "math is easier than code, math is easier than code" to
convincing my mind to not go into flight mode when seeing math symbols ;D)

> > Our paper, also posted on [1], appeared at Computer Aided Verification (CAV)’23.
> >
> > [2] https://people.cs.rutgers.edu/~sn624/papers/agni-cav23.pdf
> >
> > Together with @Paul Chaignon and @Harishankar Vishwanathan (CC'ed), we
> > are working to get our tooling into a form that is integrable into BPF
> > CI. We will look forward to your feedback when we post patches.
> 
> If this could be integrated in a way that we can regularly run this
> and validate latest version of verifier, that would be great. I have a
> second part of verifier changes coming up that extends range tracking
> logic further to support range vs range (as opposed to range vs const
> that we do currently) comparisons and is_branch_taken, so having
> independent and formal verification of these changes would be great!

+1 (from a quick skim) this work is already great as-is, and it'd be even
better once it get's in the CI. From the paper there's this

  We conducted our experiments on ... a machine with two 10-core Intel
  Skylake CPUs running at 2.20 GHz with 192 GB of memory...

I suppose the memory requirement comes from the vast amount of state space
that the Z3 SMT solver have to go through, and perhaps that poses a
challenge for CI integration?

Just wondering is there are some low-hanging fruit the can make things
easier for the SMT solver.

> > Thanks,
> >
> > --
> > Srinivas
> > The fastest algorithm can frequently be replaced by one that is almost as fast and much easier to understand.
> >