bpf: bpf_scc_visit instance and backedges accumulation for bpf_loop()

Calls like bpf_loop() or bpf_for_each_map_elem() introduce loops that
are not explicitly present in the control-flow graph. The verifier
processes such calls by repeatedly interpreting the callback function
body within the same verification path (until the current state
converges with a previous state).

Such loops require a bpf_scc_visit instance in order to allow the
accumulation of the state graph backedges. Otherwise, certain
checkpoint states created within the bodies of such loops will have
incomplete precision marks.

See the next patch for an example of a program that leads to the
verifier accepting an unsafe program.

Fixes: 96c6aa4c63af ("bpf: compute SCCs in program control flow graph")
Fixes: c9e31900b54c ("bpf: propagate read/precision marks over state graph backedges")
Reported-by: Breno Leitao <leitao@debian.org>
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Tested-by: Breno Leitao <leitao@debian.org>
Link: https://lore.kernel.org/r/20251229-scc-for-callbacks-v1-1-ceadfe679900@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 2de1a736ef69514fcf599de498aae56eaf24fe33..0baae7828af220accd4086b9bad270e745f4aff9 100644 (file)
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -19830,8 +19830,10 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
                                }
                        }
                        if (bpf_calls_callback(env, insn_idx)) {
-                               if (states_equal(env, &sl->state, cur, RANGE_WITHIN))
+                               if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
+                                       loop = true;
                                        goto hit;
+                               }
                                goto skip_inf_loop_check;
                        }
                        /* attempt to detect infinite loop to avoid unnecessary doomed work */
@@ -25071,15 +25073,18 @@ dfs_continue:
                        }
                        /*
                         * Assign SCC number only if component has two or more elements,
-                        * or if component has a self reference.
+                        * or if component has a self reference, or if instruction is a
+                        * callback calling function (implicit loop).
                         */
-                       assign_scc = stack[stack_sz - 1] != w;
-                       for (j = 0; j < succ->cnt; ++j) {
+                       assign_scc = stack[stack_sz - 1] != w;  /* two or more elements? */
+                       for (j = 0; j < succ->cnt; ++j) {       /* self reference? */
                                if (succ->items[j] == w) {
                                        assign_scc = true;
                                        break;
                                }
                        }
+                       if (bpf_calls_callback(env, w)) /* implicit loop? */
+                               assign_scc = true;
                        /* Pop component elements from stack */
                        do {
                                t = stack[--stack_sz];