vault

Verifier Complexity Limits and State Pruning

14 min read

Verifier Complexity Limits and State Pruning

Proving a BPF program is safe means exploring every reachable path through it, and a program with n independent conditional branches has up to 2^n paths — so a naive verifier would itself run effectively forever on a program with a few dozen branches. The eBPF Verifier caps its own work with a hard budget — BPF_COMPLEXITY_LIMIT_INSNS, equal to 1000000 (one million) processed instructions in Linux 6.12 (bpf.h, v6.12) — and exceeding it produces the dreaded BPF program is too large rejection. The only way the verifier survives real programs without instantly hitting that wall is state pruning: at chosen “prune points” it remembers the register/stack state in which it has already proven a path safe, and whenever it re-reaches that instruction in a state that is a subset of a remembered one, it stops — the earlier proof already covers the current case (verifier.rst, v6.12). Pruning is implemented in is_state_visited() and is the single mechanism that turns an exponential path explosion into a tractable analysis. This note explains the budget, why path explosion is the enemy, exactly how pruning works, how precision tracking makes pruning far more effective, and why a logically small program can still blow the limit.

This note is about the verifier’s own termination and resource budget — bounding the cost of the static analysis. Its sibling Verifier Bounded Loops and Termination is about proving the analyzed program terminates. They meet at loops: the brute-force way to prove a loop terminates is to simulate every iteration, which directly consumes this budget, so a loop that terminates can still be rejected for being too expensive to verify. The value ranges and types that pruning compares are produced by Verifier Register State Tracking.

Mental Model

Think of the verifier as a depth-first explorer of an execution tree. Every conditional branch is a fork: the verifier must walk both arms, because at load time it does not know which way the branch will go at runtime, so it must prove both are safe. With no other mechanism, the number of paths to walk doubles at every branch — the path explosion problem. Two things keep this finite. First, a brute-force ceiling: a counter (insn_processed) ticks up on every simulated instruction across all paths, and the moment it passes one million the verifier gives up. Second, and far more importantly, state pruning collapses the tree: most branches reconverge at a later instruction in states that are equivalent for the purpose of safety, and the verifier only needs to prove the continuation safe once per distinct equivalence class of state, not once per path.

flowchart TB
  ENTRY["program entry"] --> B1{"branch 1"}
  B1 -->|"taken"| P1["state A"]
  B1 -->|"fall-through"| P2["state B"]
  P1 --> CP["prune point<br/>(checkpoint here)"]
  P2 --> CP
  CP -->|"first arrival:<br/>state A"| EXPLORE["explore continuation,<br/>SAVE checkpoint(A)"]
  CP -->|"second arrival:<br/>state B ⊆ A?"| CHECK{"is_state_visited():<br/>states_equal(B, A)?"}
  CHECK -->|"yes — B is subset of A"| PRUNE["PRUNE:<br/>'N: safe' — stop,<br/>A's proof covers B"]
  CHECK -->|"no — B differs"| EXPLORE2["explore continuation again,<br/>SAVE checkpoint(B)"]
  EXPLORE --> CONT["...rest of program<br/>(verified once)"]

State pruning collapsing a branch. What it shows: two arms of a branch (states A and B) reconverge at a prune point. The first arm to arrive (A) is explored and its state saved as a checkpoint. When the second arm (B) arrives, is_state_visited() asks whether B is “safe-equivalent” to A — whether every register and stack slot in B is at least as constrained as in A. If so, the path is pruned: A’s already-completed proof of the rest of the program applies verbatim to B. The insight to take: without pruning, the continuation after the join is verified 2^(branches) times; with pruning it is verified roughly once per distinct equivalence class. Pruning is not an optimization bolted on — it is what makes verification of any non-trivial program possible at all, and “make my states more equivalent” is the central skill in getting big programs past the verifier.

Mechanical Walk-through

The budget: insn_processed vs BPF_COMPLEXITY_LIMIT_INSNS

The verifier’s main loop (do_check) increments env->insn_processed for every instruction it simulates, on every path. The check that enforces the ceiling, and the error message it produces, are this exact code in v6.12 (verifier.c, v6.12):

if (++env->insn_processed > BPF_COMPLEXITY_LIMIT_INSNS) {
        verbose(env,
                "BPF program is too large. Processed %d insn\n",
                env->insn_processed);
        return -E2BIG;
}

BPF_COMPLEXITY_LIMIT_INSNS is defined with a wry comment confirming the value (bpf.h, v6.12):

#define BPF_COMPLEXITY_LIMIT_INSNS      1000000 /* yes. 1M insns */

The single most important distinction to internalize: insn_processed is not the program’s size. It counts simulated instructions across all explored paths. A program of 500 instructions with several branches and a loop can easily process tens of thousands of instructions; a program that defeats pruning can process a million from a body of a few hundred. The program-text limit — the number of instructions you may submit — is enforced separately and earlier, in the bpf() syscall’s program-load handler (bpf_prog_load in kernel/bpf/syscall.c), with a single privilege-dependent gate (syscall.c, v6.12):

if (attr->insn_cnt == 0 ||
    attr->insn_cnt > (bpf_cap ? BPF_COMPLEXITY_LIMIT_INSNS : BPF_MAXINSNS)) {
        err = -E2BIG;
        goto put_token;
}

This one line pins the whole picture. A privileged loader (bpf_cap, holding CAP_BPF/CAP_SYS_ADMIN) may submit a program of up to BPF_COMPLEXITY_LIMIT_INSNS = 1,000,000 instructions of text; an unprivileged loader is capped at the classic BPF_MAXINSNS = 4096 (syscall.c, v6.12; BPF_MAXINSNS defined in uapi/linux/bpf_common.h, v6.12). Note the value 1000000 is reused for both the privileged text cap here and the processed-instruction budget in verifier.c — they are the same constant serving two different roles. So even a privileged program submitted at the maximum 1M instructions of text would, in the worst case, also have to verify within 1M processed instructions: a program with any non-trivial branching cannot be a million instructions long and verifiable, because pruning would have to fire almost perfectly. This is also why the processed-instruction limit is genuinely necessary and not arbitrary: because the verifier cannot solve the halting problem — Turing proved no general algorithm decides whether an arbitrary program halts, and Rice’s theorem generalizes that no non-trivial semantic property of programs is decidable in general (halting problem) — the million-processed-instruction ceiling is the ultimate backstop that guarantees verification itself terminates (bpf_design_QA.html; LWN 1017116).

At the end of verification the verifier prints its budget usage — the line every BPF developer learns to read (verifier.c, v6.12):

verbose(env, "processed %d insns (limit %d) max_states_per_insn %d "
        "total_states %d peak_states %d mark_read %d\n",
        env->insn_processed, BPF_COMPLEXITY_LIMIT_INSNS,
        env->max_states_per_insn, env->total_states,
        env->peak_states, env->longest_mark_read_walk);

So a successful load reports e.g. processed 12345 insns (limit 1000000) ... total_states 678 peak_states 90. A program near the wall reports processed 998000 insns (limit 1000000) — your cue that you are one refactor away from rejection.

Why path explosion is the enemy

Each conditional branch the verifier reaches forces it to explore both outcomes, because it cannot assume a runtime direction. If those branches are independent, the number of distinct paths to the program’s exit is up to 2^n for n branches — classic combinatorial explosion. The verifier’s insn_processed counter sums work across all of those paths, so without pruning even a modest program with 20–30 independent branches would exhaust the million-instruction budget. The whole architecture of the second verification pass is therefore organized around not re-walking paths that lead to states already proven safe (LWN 982077).

Prune points: where pruning is even attempted

The verifier does not try to prune at every instruction — that would be wasteful. During the check_cfg pass (see Verifier Bounded Loops and Termination), it pre-marks specific instructions as prune points via mark_prune_point(), recorded in insn_aux_data[idx].prune_point (verifier.c, v6.12). The prune points are exactly the control-flow merge candidates — branch targets, instructions after calls, points around iterator next() calls (mtardy, prune points). The verifier comment notes that “bpf progs typically have pruning point every 4 instructions” (verifier.c, v6.12). In do_check, the gate is:

if (is_prune_point(env, env->insn_idx)) {
        err = is_state_visited(env, env->insn_idx);
        ...
        if (err == 1) {
                /* found equivalent state, can prune the search */
                ... verbose(env, "%d: safe\n", env->insn_idx); ...
                goto process_bpf_exit;
        }
}

That N: safe line in verifier output is a successful prune: the verifier reached instruction N in a state equivalent to one already proven, and skipped re-verifying the rest.

is_state_visited(): the pruning decision

is_state_visited() walks the list of previously saved states (checkpoints) recorded for this instruction. For each, it calls states_equal() to ask whether the current state is “safe-covered” by the saved one. The verifier documentation defines the test precisely (verifier.rst, v6.12):

For each new branch to analyse, the verifier looks at all the states it’s previously been in when at this instruction. If any of them contain the current state as a subset, the branch is ‘pruned’ — that is, the fact that the previous state was accepted implies the current state would be as well.

“Contains as a subset” is the crucial relation, implemented in regsafe() per register and states_equal() for the whole state. The example the docs give: if previously r1 held a packet-pointer, and now r1 holds a packet-pointer “with a range as long or longer and at least as strict an alignment,” the current r1 is safe — anything the continuation could legally do with the old, weaker r1 it can also do with the new, stronger one (verifier.rst, v6.12). Likewise a register that was NOT_INIT (uninitialized) in the saved state can hold anything in the current state and still be safe, because a NOT_INIT value provably was never read on any continuation from that point. The comparison spans registers and the stack, including spilled registers — every slot must be safe for the branch to be pruned. On a hit, is_state_visited() returns 1 and the path is pruned; on a miss it records the current state as a new checkpoint (subject to heuristics) so that future arrivals can be pruned against it.

Precision tracking: making more states equivalent

Naive equivalence is too strict: if the verifier insisted that the exact value of every scalar match, almost nothing would be equivalent and pruning would rarely fire. Precision tracking (also called liveness tracking and chain precision, merged in Linux 5.3) fixes this by computing, for each register, whether its precise value actually matters to the safety of the continuation (LWN 795367; verifier.rst, v6.12). The mechanism, mark_chain_precision(), works by backtracking: when the verifier finds that a register’s exact value is needed for a safety decision (e.g. it is used as a bounded array index), it walks backward through the state chain marking the parent states “needs precision” for that register (LWN 795367). Registers not so marked are compared loosely — only their type and broad properties must match, not their exact value. The verifier documentation’s worked example: at a checkpoint reached with either r0=1,r1=0 or r0=0,r1=0, only r1 is read by the continuation; liveness tracking spots that r0’s value is irrelevant, so both arrival states are deemed equivalent and one is pruned (verifier.rst, v6.12). As LWN puts it, the checkpoint cache “is made more useful by only comparing values that are actually used, so that incidental changes don’t affect the result” (LWN 982077). Without precision tracking, large programs that load fine today would be rejected; it is one of the load-bearing scalability mechanisms.

The unprivileged state cap: BPF_COMPLEXITY_LIMIT_STATES

There is a second, much smaller limit that applies only to unprivileged programs. is_state_visited() ends with (verifier.c, v6.12):

if (!env->bpf_capable && states_cnt > BPF_COMPLEXITY_LIMIT_STATES)
        return 0;

with #define BPF_COMPLEXITY_LIMIT_STATES 64 (verifier.c, v6.12). For a non-bpf_capable program, if more than 64 states have accumulated at a single instruction the verifier stops saving new checkpoints there — a tight guard that, combined with the 64-state count, sharply constrains how complex an unprivileged program can be before it fails to verify. Privileged (bpf_capable) programs are bounded only by the one-million-instruction ceiling.

Failure Modes and How They Read

  • BPF program is too large. Processed N insn — the headline -E2BIG. You burned the million-instruction budget. The cause is almost never that the program text is literally too long; it is that pruning is not firing, so paths are being re-walked. Common triggers: a loop whose body perturbs tracked state on every iteration (each iteration is a new, non-equivalent state); nested loops (multiplicative); a function __always_inlined into a loop so its whole body counts every iteration; or a scalar that lost precision and now forces the verifier to treat many values as distinct (LWN 1017116). Read the trailing total_states/peak_states numbers — high peak_states says pruning is failing.
  • too many states to verify / state-count rejection (unprivileged) — you hit BPF_COMPLEXITY_LIMIT_STATES (64) on an unprivileged load. The program is too branchy for unprivileged BPF; it needs CAP_BPF (see CAP_BPF and BPF Privilege Model) or simplification.
  • A logically tiny program that nonetheless fails — the canonical surprise. Verification cost is not program length; it is the number of distinct states explored. A short program with a handful of independent conditions and a loop can explore tens of thousands of states. The fix is to make states more equivalent: hoist invariant computations out of loops, keep loop-carried scalars bounded and precise, and prefer bpf_loop/iterators (trip-count-independent verification) over raw bounded loops (LWN 1017116; see Verifier Bounded Loops and Termination).
  • Adding a line made it stop verifying — a tiny change can flip a register from “imprecise, prunable” to “precise, not prunable,” collapsing pruning across the whole program and tipping insn_processed over the limit. This non-locality is why verifier debugging is famously frustrating; see Reading and Debugging Verifier Errors.

Alternatives and When to Choose Them

State pruning is not optional — it is intrinsic to how the verifier works — so the “alternatives” are really strategies for staying under the budget. Use global (non-static) functions, which the verifier checks once, independently of calling context, so their body counts toward the limit a single time rather than per call site (LWN 1017116). Drop unnecessary __always_inline (unneeded since ~2017, and actively harmful when it inlines a body into a loop) (LWN 1017116). Replace raw bounded loops with bpf_loop or open-coded iterators, whose verification cost is independent of the trip count (detailed in Verifier Bounded Loops and Termination). For deliberately open-ended loops, may_goto/can_loop lets the runtime — not the verifier’s simulation — enforce the bound. The proposal in 2025 to “take BPF programs beyond one million instructions” notably did not simply raise the constant; the consensus was that better-structured code (global functions, iterators) is the right answer, with the limit raised only as a fallback (LWN 1017116).

Both 6.12 and 6.18 LTS define BPF_COMPLEXITY_LIMIT_INSNS as exactly 1000000 — verified by fetching include/linux/bpf.h at both the v6.12 and v6.18 tags (bpf.h, v6.12; bpf.h, v6.18). The 2025 “beyond one million” discussion (LWN 1017116) pushed restructuring (global functions, iterators) rather than raising the constant, and as of 6.18 the limit is unchanged.

Production Notes

Real large programs — Cilium’s eBPF datapath, complex bpftrace scripts, security-monitoring agents — routinely live near the million-instruction wall, and “the program got too complex to verify” is a recurring production incident when a new feature adds branches (LWN 1017116). The practical toolkit: load with BPF_LOG_LEVEL verbose logging and read the processed N insns / peak_states line to see headroom; use bpftool prog and the verifier log to find which subprogram dominates; convert hot inlined helpers to global functions; and prefer iterators over unrolled loops. The deeper lesson — repeated across LWN’s verifier coverage — is that verification cost is a property of state diversity, not code size: two programs of identical length can differ by orders of magnitude in insn_processed purely based on how well their branches reconverge into prunable states (LWN 982077; mtardy, prune points). Writing “verifier-friendly” BPF is largely the craft of keeping state equivalent so pruning fires.

See Also

Graph View