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

[Paul Chaignon <paul.chaignon@gmail.com>]

On Mon, Oct 23, 2023 at 10:51:57PM -0700, Andrii Nakryiko wrote:
> On Mon, Oct 23, 2023 at 3:50 PM Andrii Nakryiko
> <andrii.nakryiko@gmail.com> wrote:
> >
> > On Mon, Oct 23, 2023 at 8:52 AM Paul Chaignon <paul@isovalent.com> wrote:
> > >
> > > On Mon, Oct 23, 2023 at 10:05:41PM +0800, Shung-Hsi Yu wrote:
> > > > 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:
> > >
> > > [...]
> > >
> > > > > > >>> 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
> > >
> > > Hari et al. did a great job at explaining the intuitions throughout the
> > > paper. So even if you skip the math, you should be able to follow.
> > >
> > > Having an understanding of abstract interpretation helps. The Mozilla
> > > wiki has a great one [1] and I wrote a shorter BPF example of it [2].
> > >
> > > 1 - https://wiki.mozilla.org/Abstract_Interpretation
> > > 2 - https://pchaigno.github.io/abstract-interpretation.html
> > >
> >
> > thanks :)
> 
> Hey Paul,
> 
> I had a bunch of time on the plane to catch up on reading, so I read
> your blog post about PREVAIL among other things. Hopefully you don't
> mind some comments posted here.
> 
> > Observation 1. The analysis must track binary relations among registers.
> 
> It's curious that the BPF verifier in kernel actually doesn't track
> relations in this sense, and yet it works for lots and lots of
> practical programs. :)

It kind of does, but only for the types where it's actually needed. For
example if we have:

  3: (bf) r3 = r1
  4: (07) r3 += 14
  5: (2d) if r3 > r2 goto pc+50
   R1_w=pkt(id=0,off=0,r=14,imm=0) R2_w=pkt_end(id=0,off=0,imm=0)
     R3_w=pkt(id=0,off=14,r=14,imm=0)

R1's range actually refers to the relationship to pkt_end, R2 at this
point. So, R1's r=14 carries the same information as R1 + 14 <= R2.

A big difference is that the Linux verifier is very tailored to eBPF. So
it doesn't perform this sort of more complicated tracking for all
registers and slack slots. I suspect that plays a bit role in the lower
performance of PREVAIL.

> 
> 
> (Speaking of kernel verifier implementation)
> 
> > Third, it does not currently support programs with loops.
> 
> It does, and I'm not even talking about bounded loops that are
> basically unrolled as many times as necessary. We have bpf_loop()
> helper calling given callback as many times as requested, but even
> better we now have open-coded iterators. Please check selftests using
> bpf_for() macro.
> 
> Note that Eduard is fixing discovered issues in open-coded iterators
> convergence checks and logic, but other than that BPF does have real
> loops.

I'll fix that. I also wasn't aware of the more recent bpf_for. Nice!

The larger point is that PREVAIL is able to fully verify free-form
loops. It doesn't impose a structure or rely on trusted code (helpers
and kfuncs).
In the end, I don't think it matters much. The amount of trusted code
for this is small and well understood. And we probably don't want
ill-structured loops in our C code anyway. But the lack of loop support
used to take a lot of attention when speaking of the BPF verifier, so I
guess that's why it ended up being a selling point in the paper.

> 
> 
> And about a confusing bit at the end:
> 
> >  0: r0 = 0
> >  1: if r1 > 10 goto pc+4  // r1 ∈ [0; 10]
> >  2: if r2 > 10 goto pc+3  // r2 ∈ [0; 10]
> >  3: r1 *= r2              // r1 ∈ [0; 100]
> >  4: if r1 != 5 goto pc+1
> >  5: r1 /= r0              // Division by zero!
> >  6: exit
> >
> > After instruction 2, both r1 and r2 have abstract value [0; 10].
> > After instruction 3, r1 holds the multiplication of r1 and r2 and
> > therefore has abstract value [0; 100]. When considering the condition at
> >  instruction 4, because 11 ∈ [0; 100], we will walk both paths and hit the
> >  division by zero.
> >
> > Except we know that r1 can never take value 11. The number 11 is a prime
> >  number, so it is not a multiple of any integers between 0 and 10.
> 
> This made me pause for a while. I think you meant to have `4: if r1 !=
> 11 goto pc+1` and then go on to explain that you can't get 11 by
> multiplying numbers in range [0; 10], because 11 is greater than 10
> (so can't be 1 x 11), but also it's a prime number, so you can't get
> it from multiplication of two integers. So please consider fixing up
> the code example, and perhaps elaborate a bit more on why 11 can't
> happen in actuality. This example does look a bit academic, but, well,
> formal methods and stuff, it's fitting! ;)

You're absolutely right. It should be 11 instead of 5. That's what I get
for changing the ranges from [0; 4] to [0; 10] at the last minute.

> 
> 
> > It’s a bit disappointing that the paper doesn’t include any comparison with the Linux verifier on the same corpus of BPF programs.
> 
> Indeed, I concur. It would be interesting to have this comparison as
> of the most recent version of PREVAIL and Linux's BPF verifier.
> 
> 
> Either way, thanks a lot for the very approachable and informative
> blog post, it was a pleasure to read! Great work!

Thanks for the read and the review! I like reading about what academia
is doing around BPF so certainly not my last post on those topics :)

> 
> 
> >
> > > >
> > > > > > 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!
> > >
> > > The current goal is to have this running somewhere regularly (maybe
> > > releases + manual triggers) in a semi-automated fashion. The two
> > > challenges today are the time it takes to run verification (days without
> > > parallelization) and whether the bit of conversion & glue code will be
> > > maintanable long term.
> > >
> > > I'm fairly optimistic on the first as we're already down to hours with
> > > basic parallelization. The second is harder to predict, but I guess your
> > > patches will be a good exercice :)
> > >
> > > I've already ran the verification on v6.0 to v6.3; v6.4 is currently
> > > running. Hari et al. had verified v4.14 to v5.19 before. I'll give it a
> > > try on this patchset afterward.
> >
> > Cool, that's great! The second part of this work will be generalizing
> > this logic in kernel to support range vs range comparisons, so I'd
> > appreciate it if you could validate that one as well. I'm finalizing
> > it, but will wait for this patch set to land first before posting
> > second part to have a proper CI testing runs (and limit amount of code
> > review to be done).

Happy to!

> >
> > BTW, I've since did some more changes to this "selftests" to be a bit
> > more parallelizable, so this range_vs_consts set of tests now can run
> > in about 5 minutes on 8+ core QEMU instance. In the second part we'll
> > have range-vs-range, so we have about 106 million cases and it takes
> > slightly more than 8 hours single-threaded. But with parallelization,
> > it's done in slightly more than one hour.
> >
> > So, of course, still too slow to run as part of normal test_progs run,
> > but definitely easy to run locally to validate kernel changes (and
> > probably makes sense to enable on some nightly CI runs, when we have
> > them).
> >
> > Regardless, my point is that both methods of verification are
> > complementary, I think, and it's good to have both available and
> > working on latest kernel versions.

Completely agree!

> >
> >
> > >
> > > >
> > > > +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.
> > >
> > > This is how much memory the system had, but it didn't use it all :)
> > > When running the solver on a single core, I saw around 1GB of memory
> > > usage. With my changes to run on several cores, it can grow to a few
> > > GBs depending on the number of cores.
> > >
> > > --
> > > Paul