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 #1 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 #1 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 first loop iteration and use it as precise on
a second (for iterator based loops).
I urge people to at least skim over the commit message for patch #1.
Patches are organized as follows:
- patch #1: introduces exact mode for states comparison and adds
widening heuristic;
- patch #2: adds test-cases that demonstrate why the series is
necessary;
- patch #3: extends patch #1 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 #4: adds a test-case that demonstrates a program
which requires loop entry tracking for correct verification;
- patch #5: 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].
[1] https://lore.kernel.org/bpf/97a90da09404c65c8e810cf83c94ac703705dc0e.camel@xxxxxxxxx/
Eduard Zingerman (5):
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 | 440 ++++++++++++-
tools/testing/selftests/bpf/progs/iters.c | 620 ++++++++++++++++++
.../selftests/bpf/progs/iters_task_vma.c | 1 +
4 files changed, 1043 insertions(+), 34 deletions(-)
--
2.42.0
