On Fri, Oct 20, 2023 at 10:37 AM Srinivas Narayana Ganapathy <sn624@xxxxxxxxxxxxxx> 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@xxxxxxxxx> wrote: > > > > On Thu, Oct 19, 2023 at 12:52 AM Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> 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@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx/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 ;) > 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! > > Thanks, > > -- > Srinivas > The fastest algorithm can frequently be replaced by one that is almost as fast and much easier to understand. >
