| Message ID | 20231024000917.12153-1-eddyz87@gmail.com (mailing list archive) |
|---|---|
| Headers | show |
| Series | exact states comparison for iterator convergence checks | expand |
Hello: This series was applied to bpf/bpf-next.git (master) by Alexei Starovoitov <ast@kernel.org>: On Tue, 24 Oct 2023 03:09:10 +0300 you 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. > > [...] Here is the summary with links: - [bpf-next,v3,1/7] bpf: move explored_state() closer to the beginning of verifier.c https://git.kernel.org/bpf/bpf-next/c/3c4e420cb653 - [bpf-next,v3,2/7] bpf: extract same_callsites() as utility function https://git.kernel.org/bpf/bpf-next/c/4c97259abc9b - [bpf-next,v3,3/7] bpf: exact states comparison for iterator convergence checks https://git.kernel.org/bpf/bpf-next/c/2793a8b015f7 - [bpf-next,v3,4/7] selftests/bpf: tests with delayed read/precision makrs in loop body https://git.kernel.org/bpf/bpf-next/c/389ede06c297 - [bpf-next,v3,5/7] bpf: correct loop detection for iterators convergence https://git.kernel.org/bpf/bpf-next/c/2a0992829ea3 - [bpf-next,v3,6/7] selftests/bpf: test if state loops are detected in a tricky case https://git.kernel.org/bpf/bpf-next/c/64870feebecb - [bpf-next,v3,7/7] bpf: print full verifier states on infinite loop detection https://git.kernel.org/bpf/bpf-next/c/b4d8239534fd You are awesome, thank you!
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!
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.
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(-)