On Mon, Oct 23, 2023 at 5:09 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > Iterator convergence logic in is_state_visited() uses state_equals() > for states with branches counter > 0 to check if iterator based loop > converges. This is not fully correct because state_equals() relies on > presence of read and precision marks on registers. These marks are not > guaranteed to be finalized while state has branches. > Commit message for patch #3 describes a program that exhibits such > behavior. > > This patch-set aims to fix iterator convergence logic by adding notion > of exact states comparison. Exact comparison does not rely on presence > of read or precision marks and thus is more strict. > As explained in commit message for patch #3 exact comparisons require > addition of speculative register bounds widening. The end result for > BPF verifier users could be summarized as follows: > > (!) After this update verifier would reject programs that conjure an > imprecise value on the first loop iteration and use it as precise > on the second (for iterator based loops). > > I urge people to at least skim over the commit message for patch #3. > > Patches are organized as follows: > - patches #1,2: moving/extracting utility functions; > - patch #3: introduces exact mode for states comparison and adds > widening heuristic; > - patch #4: adds test-cases that demonstrate why the series is > necessary; > - patch #5: extends patch #3 with a notion of state loop entries, > these entries have to be tracked to correctly identify that > different verifier states belong to the same states loop; > - patch #6: adds a test-case that demonstrates a program > which requires loop entry tracking for correct verification; > - patch #7: just adds a few debug prints. > > The following actions are planned as a followup for this patch-set: > - implementation has to be adapted for callbacks handling logic as a > part of a fix for [1]; > - it is necessary to explore ways to improve widening heuristic to > handle iters_task_vma test w/o need to insert barrier_var() calls; > - explored states eviction logic on cache miss has to be extended > to either: > - allow eviction of checkpoint states -or- > - be sped up in case if there are many active checkpoints associated > with the same instruction. > > The patch-set is a followup for mailing list discussion [1]. > > Changelog: > - V2 [3] -> V3: > - correct check for stack spills in widen_imprecise_scalars(), > added test case progs/iters.c:widen_spill to check the behavior > (suggested by Andrii); > - allow eviction of checkpoint states in is_state_visited() to avoid > pathological verifier performance when iterator based loop does not > converge (discussion with Alexei). > - V1 [2] -> V2, applied changes suggested by Alexei offlist: > - __explored_state() function removed; > - same_callsites() function is now used in clean_live_states(); > - patches #1,2 are added as preparatory code movement; > - in process_iter_next_call() a safeguard is added to verify that > cur_st->parent exists and has expected insn index / call sites. > > [1] https://lore.kernel.org/bpf/97a90da09404c65c8e810cf83c94ac703705dc0e.camel@xxxxxxxxx/ > [2] https://lore.kernel.org/bpf/20231021005939.1041-1-eddyz87@xxxxxxxxx/ > [3] https://lore.kernel.org/bpf/20231022010812.9201-1-eddyz87@xxxxxxxxx/ > > Eduard Zingerman (7): > bpf: move explored_state() closer to the beginning of verifier.c > bpf: extract same_callsites() as utility function > bpf: exact states comparison for iterator convergence checks > selftests/bpf: tests with delayed read/precision makrs in loop body > bpf: correct loop detection for iterators convergence > selftests/bpf: test if state loops are detected in a tricky case > bpf: print full verifier states on infinite loop detection > > include/linux/bpf_verifier.h | 16 + > kernel/bpf/verifier.c | 475 ++++++++++-- > tools/testing/selftests/bpf/progs/iters.c | 695 ++++++++++++++++++ > .../selftests/bpf/progs/iters_task_vma.c | 1 + > 4 files changed, 1133 insertions(+), 54 deletions(-) > > -- > 2.42.0 > Thanks a lot for working on this and getting it to the end despite many setbacks and ambiguity, great work!
