On Sat, Nov 11, 2023 at 05:06:03PM -0800, Andrii Nakryiko wrote: > Add test to validate BPF verifier's register range bounds tracking logic. > > 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. > > 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 without parallelization. But we also split > those tests by init/cond numeric types, which allows to rely on > test_progs's parallelization of tests with `-j` option, getting run time > down to about 5 minutes on 8 cores. It's still something that shouldn't > be run during normal test_progs run. But we can run it a reasonable > time, and so perhaps a nightly CI test run (once we have it) would be > a good option for this. > > We also add a small set of tricky conditions that came up during > development and triggered various bugs or corner cases in either > selftest's reimplementation of range bounds logic or in verifier's logic > itself. These are fast enough to be run as part of normal test_progs > test run and are great for a quick sanity checking. > > Let's take a look at test output to understand what's going on: > > $ sudo ./test_progs -t reg_bounds_crafted > #191/1 reg_bounds_crafted/(u64)[0; 0xffffffff] (u64)< 0:OK > ... > #191/115 reg_bounds_crafted/(u64)[0; 0x17fffffff] (s32)< 0:OK > ... > #191/137 reg_bounds_crafted/(u64)[0xffffffff; 0x100000000] (u64)== 0:OK > > Each test case is uniquely and fully described by this generated string. > E.g.: "(u64)[0; 0x17fffffff] (s32)< 0". This means that we > initialize a register (R6) in such a way that verifier knows that it can > have a value in [(u64)0; (u64)0x17fffffff] range. Another > register (R7) is also set up as u64, but this time a constant (zero in > this case). They then are compared using 32-bit signed < operation. > Resulting TRUE/FALSE branches are evaluated (including cases where it's > known that one of the branches will never be taken, in which case we > validate that verifier also determines this as a dead code). Test > validates that verifier's final register state matches expected state > based on selftest's own reg_state logic, implemented from scratch for > cross-checking purposes. > > These test names can be conveniently used for further debugging, and if -vv > verboseness is requested we can get a corresponding verifier log (with > mark_precise logs filtered out as irrelevant and distracting). Example below is > slightly redacted for brevity, omitting irrelevant register output in > some places, marked with [...]. > > $ sudo ./test_progs -a 'reg_bounds_crafted/(u32)[0; U32_MAX] (s32)< -1' -vv > ... > VERIFIER LOG: > ======================== > func#0 @0 > 0: R1=ctx(off=0,imm=0) R10=fp0 > 0: (05) goto pc+2 > 3: (85) call bpf_get_current_pid_tgid#14 ; R0_w=scalar() > 4: (bc) w6 = w0 ; R0_w=scalar() R6_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) > 5: (85) call bpf_get_current_pid_tgid#14 ; R0_w=scalar() > 6: (bc) w7 = w0 ; R0_w=scalar() R7_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) > 7: (b4) w1 = 0 ; R1_w=0 > 8: (b4) w2 = -1 ; R2=4294967295 > 9: (ae) if w6 < w1 goto pc-9 > 9: R1=0 R6=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) > 10: (2e) if w6 > w2 goto pc-10 > 10: R2=4294967295 R6=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) > 11: (b4) w1 = -1 ; R1_w=4294967295 > 12: (b4) w2 = -1 ; R2_w=4294967295 > 13: (ae) if w7 < w1 goto pc-13 ; R1_w=4294967295 R7=4294967295 > 14: (2e) if w7 > w2 goto pc-14 > 14: R2_w=4294967295 R7=4294967295 > 15: (bc) w0 = w6 ; [...] R6=scalar(id=1,smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) > 16: (bc) w0 = w7 ; [...] R7=4294967295 > 17: (ce) if w6 s< w7 goto pc+3 ; R6=scalar(id=1,smin=0,smax=umax=4294967295,smin32=-1,var_off=(0x0; 0xffffffff)) R7=4294967295 > 18: (bc) w0 = w6 ; [...] R6=scalar(id=1,smin=0,smax=umax=4294967295,smin32=-1,var_off=(0x0; 0xffffffff)) > 19: (bc) w0 = w7 ; [...] R7=4294967295 > 20: (95) exit > > from 17 to 21: [...] > 21: (bc) w0 = w6 ; [...] R6=scalar(id=1,smin=umin=umin32=2147483648,smax=umax=umax32=4294967294,smax32=-2,var_off=(0x80000000; 0x7fffffff)) > 22: (bc) w0 = w7 ; [...] R7=4294967295 > 23: (95) exit > > from 13 to 1: [...] > 1: [...] > 1: (b7) r0 = 0 ; R0_w=0 > 2: (95) exit > processed 24 insns (limit 1000000) max_states_per_insn 0 total_states 2 peak_states 2 mark_read 1 > ===================== > > Verifier log above is for `(u32)[0; U32_MAX] (s32)< -1` use cases, where u32 > range is used for initialization, followed by signed < operator. Note > how we use w6/w7 in this case for register initialization (it would be > R6/R7 for 64-bit types) and then `if w6 s< w7` for comparison at > instruction #17. It will be `if R6 < R7` for 64-bit unsigned comparison. > Above example gives a good impression of the overall structure of a BPF > programs generated for reg_bounds tests. > > In the future, this "framework" can be extended to test not just > conditional jumps, but also arithmetic operations. Adding randomized > testing is another possibility. > > Some implementation notes. We basically have our own generics-like > operations on numbers, where all the numbers are stored in u64, but how > they are interpreted is passed as runtime argument enum num_t. Further, > `struct range` represents a bounds range, and those are collected > together into a minimal `struct reg_state`, which collects range bounds > across all four numberical domains: u64, s64, u32, s64. > > Based on these primitives and `enum op` representing possible > conditional operation (<, <=, >, >=, ==, !=), there is a set of generic > helpers to perform "range arithmetics", which is used to maintain struct > reg_state. We simulate what verifier will do for reg bounds of R6 and R7 > registers using these range and reg_state primitives. Simulated > information is used to determine branch taken conclusion and expected > exact register state across all four number domains. > > Implementation of "range arithmetics" is more generic than what verifier > is currently performing: it allows range over range comparisons and > adjustments. This is the intended end goal of this patch set overall and verifier > logic is enhanced in subsequent patches in this series to handle range > vs range operations, at which point selftests are extended to validate > these conditions as well. For now it's range vs const cases only. > > Note that tests are split into multiple groups by their numeric types > for initialization of ranges and for comparison operation. This allows > to use test_progs's -j parallelization to speed up tests, as we now have > 16 groups of parallel running tests. Overall reduction of running time > that allows is pretty good, we go down from more than 30 minutes to > slightly less than 5 minutes running time. > > Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> > Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx> Acked-by: Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx>
