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@xxxxxxxx> 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@xxxxxxxxx/ > > 3: https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e > > 4: https://lore.kernel.org/all/1485295229-14081-3-git-send-email-paulmck@xxxxxxxxxxxxxxxxxx/
