Re: [PATCH bpf-next v3 0/7] exact states comparison for iterator convergence checks

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2023-10-23 at 22:58 -0700, Andrii Nakryiko wrote:
> On Mon, Oct 23, 2023 at 5:09 PM Eduard Zingerman <eddyz87@gmail.com> 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@gmail.com/
> > [2] https://lore.kernel.org/bpf/20231021005939.1041-1-eddyz87@gmail.com/
> > [3] https://lore.kernel.org/bpf/20231022010812.9201-1-eddyz87@gmail.com/
> > 
> > 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!

Thank you and Alexei for working on it as well.
We'll see if this patch-set is good enough or the idea with
computing fixed point for read and precision marks has to be finalized.