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