eBPF Verifier

The eBPF verifier is the static-analysis engine inside the Linux kernel that mathematically proves a submitted BPF program is safe to run before it is allowed to run at all. It is the single component that makes the otherwise-reckless sentence “let unprivileged-ish userspace inject and execute its own code in ring 0” into a safe one. Before any extended Berkeley Packet Filter (eBPF) program is JIT-compiled and attached to a kernel hook, the verifier walks every reachable path through the program, simulating execution one instruction at a time, and rejects the program unless it can guarantee four things: the program cannot crash the kernel (no out-of-bounds or wild-pointer access), cannot read uninitialized memory (no information leak from kernel stack/registers), cannot loop forever (it terminates), and cannot violate type or memory-region rules (every pointer is used only where its kind is legal). The verifier lives in kernel/bpf/verifier.c — 22,553 lines in Linux 6.12 LTS, verified by line count of the v6.12 tag — and its entry point is the function bpf_check() (verifier.rst, v6.12; verifier.c, v6.12). This note is the orientation map for the verifier: what it guarantees, the real shape of the algorithm, the whole pass pipeline inside bpf_check(), and the load path — then it dispatches to the deep sub-notes for value tracking, termination, state pruning, and pointer safety.

Kernel version — this note is pinned to an LTS

Every line number, constant, and code path here was read from the Linux 6.12 LTS source tree (released 2024-11-17), fetched from raw.githubusercontent.com/torvalds/linux/v6.12/… during the writing of this note. 6.12 is chosen deliberately: it is a maintained long-term-support branch (still receiving stable releases as of 2026-08), so its behaviour is what a large fraction of production kernels actually run, and it is the pin used across this vault’s eBPF material. Mainline has moved on — the verifier evolves faster than almost any other kernel subsystem — so treat every claim as “as of 6.12 LTS” and re-check anything load-bearing against your own tree. Where something is known to have changed after 6.12, it is called out with its version.

Why a Verifier Exists at All

A loadable kernel module can do anything: dereference a null pointer and panic the box, spin forever with interrupts disabled and hang the CPU, or read arbitrary kernel memory and leak secrets. The whole premise of eBPF is to get most of a kernel module’s reach — attach code to the packet path, to a function’s entry, to a security hook, to the CPU scheduler — without a module’s danger. The verifier is what buys that trade. It is a gatekeeper that runs once, at load time, in the privileged context of the loading process, and produces a binary verdict: accept (the program provably cannot misbehave) or reject (with an error and, optionally, a detailed log explaining the rejection).

Crucially, the verifier is a conservative over-approximation. It does not run your program; it reasons about all possible values your program’s registers and memory could ever hold, and proves that under every such possibility the program stays inside the rules. Because it must be sound (never accept an unsafe program) and must always halt (the kernel cannot afford an analyzer that itself loops forever), it is necessarily incomplete: there exist perfectly safe programs it cannot prove safe and therefore rejects. This incompleteness is the origin of the infamous developer experience of fighting the verifier — see Reading and Debugging Verifier Errors — but it is the correct trade: a false rejection costs a developer some refactoring; a false acceptance costs a kernel exploit.

The choice is easier to see when the alternatives are laid side by side. Every mechanism for running extension code inside an operating-system kernel has to pay for safety somewhere — at build time, at load time, or at run time — and the verifier is a bet that load time is the cheapest place to pay.

Mechanism	When safety is established	Runtime cost	What it can express	Failure mode when it is wrong
Loadable kernel module	Never (trust the author)	Zero	Everything	Kernel panic, silent corruption, root escalation
eBPF + verifier	Load time, by proof	Zero (native JIT-compiled code)	A deliberately restricted subset: no unbounded loops, no arbitrary calls, 512-byte stack	Verifier bug ⇒ the security boundary is gone
Interpreted sandbox / VM	Run time, per operation	High (bounds check on every access)	Broad	Escape bug ⇒ same as a module
Userspace daemon (no kernel code)	N/A — no kernel code	Very high (context switches, copies)	Whatever the syscall API exposes	Just slow
seccomp-BPF	Load time, by a much simpler classic-BPF checker	Near-zero	Only syscall-argument filtering, no general memory model	Filter bypass

The safety-cost matrix for kernel extension mechanisms. What it shows: the four columns are the trade being made — when you pay, how much you pay while running, how much you can say, and what happens when the safety mechanism itself is buggy. The insight to take: eBPF is the only row that gets zero runtime cost and a safety guarantee, and it does so by moving the entire cost to a one-time load-time proof. That is also why a verifier bug is a full kernel-security incident rather than a performance bug: there is no second line of defence behind it.

What the Verifier Guarantees

The verifier’s safety contract has four pillars, each enforced by a distinct part of the analysis, and each surfacing as a distinct family of error messages.

• Memory safety. Every load and store goes through a register whose type the verifier knows (a context pointer, a stack pointer, a map-value pointer, a packet pointer, …) and whose bounds it tracks. A load/store is allowed only if the access stays inside the known-safe range for that pointer type. Out-of-bounds access, dereferencing a possibly-null pointer, and arithmetic that could push a pointer outside its region are all rejected. The pointer-type lattice and the bounds discipline are the subject of Verifier Memory Safety and Pointer Types.
• No uninitialized reads. A register or stack slot may be read only after it has been written. This stops a program from leaking whatever the kernel left in a register or on the stack. The doc states it plainly: a bpf_mov R0 = R2 where R2 was never written “will be rejected, since R2 is unreadable at the start of the program”, and “the verifier will allow eBPF program to read data from stack only after it wrote into it” (verifier.rst, v6.12).
• Termination. The program must provably finish. For an unprivileged loader the control-flow-graph pass rejects any back-edge outright; for a CAP_BPF-capable loader back-edges are permitted and termination is proved later by simulating the loop’s iterations (Linux 5.3 onward), with bpf_loop() and the may_goto instruction as escape hatches. The exact rule is subtler than “loops are banned” and is dissected in the Termination section below and in Verifier Bounded Loops and Termination.
• Bounded analysis (the verifier itself terminates). Separately from your program terminating, the verifier’s own work is capped. It will process at most BPF_COMPLEXITY_LIMIT_INSNS = 1,000,000 simulated instructions — the constant is defined in include/linux/bpf.h with the comment /* yes. 1M insns */ — before giving up with BPF program is too large. Processed %d insn and -E2BIG (verifier.c, v6.12, line 18320). To stay under that budget on real programs with branches, it prunes redundant states — covered in Verifier Complexity Limits and State Pruning.

flowchart TD
  subgraph P["The four pillars"]
    M["Memory safety"]
    U["No uninitialized reads"]
    T["Program terminates"]
    B["Analysis terminates"]
  end
  subgraph MECH["Enforcing machinery in verifier.c"]
    RT["Register type lattice<br/>PTR_TO_CTX, PTR_TO_STACK,<br/>PTR_TO_MAP_VALUE, SCALAR_VALUE, ..."]
    BD["Bounds: 4 min/max pairs<br/>+ tnum bit knowledge"]
    LV["Liveness marks<br/>REG_LIVE_WRITTEN / READ"]
    CFG["check_cfg: DFS edge labelling<br/>tree / back / forward / cross"]
    SIM["do_check: simulate every<br/>loop iteration until states converge"]
    BUDGET["insn_processed counter<br/>+ state pruning"]
  end
  subgraph ERR["What you see when it fails"]
    E1["R2 invalid mem access<br/>'map_value_or_null'"]
    E2["R2 !read_ok"]
    E3["back-edge from insn N to M<br/>infinite loop detected at insn N"]
    E4["BPF program is too large.<br/>Processed 1000001 insn"]
  end
  M --> RT --> E1
  M --> BD --> E1
  U --> LV --> E2
  T --> CFG --> E3
  T --> SIM --> E3
  B --> BUDGET --> E4

From guarantee to mechanism to error message. What it shows: each of the four safety pillars is implemented by specific machinery in kernel/bpf/verifier.c, and each piece of machinery produces a recognisable family of rejection messages. The insight to take: verifier errors are not arbitrary — reading one backwards tells you which guarantee you tripped, which tells you which fix applies. !read_ok is never fixed by adding a bounds check, and a bounds check never fixes too large.

Uncertain

Verify: that all four guarantees and their constants are identical in 6.18 LTS as in 6.12. Reason: constants and code paths here were read from the v6.12 tag; the canonical verifier.rst error-message section was previously confirmed byte-identical in v6.18, but every guard in verifier.c was not diffed between the two tags during this pass. To resolve: diff kernel/bpf/verifier.c and include/linux/bpf.h between v6.12 and v6.18 for BPF_COMPLEXITY_LIMIT_INSNS, BPF_COMPLEXITY_LIMIT_STATES, BPF_COMPLEXITY_LIMIT_JMP_SEQ, BPF_MAXINSNS, MAX_BPF_STACK, MAX_USED_MAPS and the do_check() guards. uncertain

Mental Model: A Sound DFS Over the Control-Flow Graph

The right way to think about the verifier is as a depth-first search over the program’s control-flow graph, carrying an abstract machine state along each path. At every instruction the verifier holds a symbolic picture of all eleven registers and every used stack slot — not concrete values, but each register’s type and the range of values it could hold. It steps the abstract machine forward through each instruction, updating that picture according to the instruction’s semantics, and at every memory access or call it checks the picture against the rules. When it hits a conditional branch, it forks: it pushes one side onto a worklist and continues down the other, refining the value ranges differently on each side (e.g. after if r0 > 8, the true branch knows r0 >= 9). When it reaches BPF_EXIT, that path is done and it pops the next path. The program is accepted only if every path reaches a valid exit without ever breaking a rule.

flowchart TD
  START["bpf() syscall<br/>BPF_PROG_LOAD"] --> CHECK["bpf_check()<br/>allocate bpf_verifier_env"]
  CHECK --> CFG["Pass 1: check_cfg()<br/>DFS edge labelling.<br/>Reject unreachable insns,<br/>out-of-range jumps, and —<br/>only if !bpf_capable —<br/>any back-edge"]
  CFG --> DC["Pass 2: do_check_main()<br/>then do_check_subprogs()<br/>simulate every path"]
  DC --> STEP["At each insn:<br/>update register/stack state,<br/>check memory + type rules"]
  STEP --> BR{"conditional<br/>branch?"}
  BR -->|"yes"| FORK["fork: push not-taken side<br/>onto the state stack,<br/>refine bounds on each side"]
  BR -->|"no"| NEXT["advance to next insn"]
  FORK --> PRUNE{"prune point, and an<br/>explored state that is<br/>at least as general?"}
  PRUNE -->|"yes"| PRUNED["prune: 'N: safe'<br/>proved already"]
  PRUNE -->|"no"| NEXT
  NEXT --> STEP
  STEP -->|"rule broken"| REJECT["reject: -EACCES<br/>+ verifier log"]
  STEP -->|"insn_processed > 1M"| TOOBIG["reject: -E2BIG<br/>'BPF program is too large'"]
  STEP -->|"BPF_EXIT and<br/>state stack empty"| FIXUP["rewrite passes:<br/>convert_ctx_accesses,<br/>do_misc_fixups, ..."]
  FIXUP --> ACCEPT["accept -> hand to JIT"]

The verifier as a path-exploring abstract interpreter. What it shows: loading goes through bpf_check(), which first does a cheap control-flow-graph (CFG) pass to reject malformed and unreachable code, then a path-by-path simulation that tracks register and stack state, forks at branches, and prunes paths it has already proven safe. A rule violation rejects with -EACCES; exhausting the one-million-instruction analysis budget rejects with -E2BIG; if every path reaches a clean exit the program is accepted and handed to the JIT. The insight to take: the verifier does not run your code once — it proves a property over all executions, which is why a branch-heavy program can be rejected for “complexity” even when it is tiny, and why pruning equivalent states is what makes the whole thing feasible.

The Real Pass Pipeline Inside bpf_check()

“Two passes” is the textbook summary and it is what verifier.rst says, but reading bpf_check() in v6.12 top to bottom shows something closer to a small compiler: roughly fifteen ordered phases, of which the path walk is one. Getting this order right matters, because several of the phases modify the program, and a few of them run only for privileged loaders.

flowchart TD
  A0["kvzalloc bpf_verifier_env<br/>vzalloc insn_aux_data, one per insn"] --> A1
  A1["Resolve privilege from the BPF token:<br/>bpf_capable, allow_ptr_leaks,<br/>allow_uninit_stack,<br/>bypass_spec_v1, bypass_spec_v4"] --> A2
  A2["bpf_vlog_init: wire up the caller's<br/>log_buf / log_size / log_level"] --> A3
  A3["if !privileged: mutex_lock(bpf_verifier_lock)<br/>-- unprivileged verification is<br/>serialised system-wide"] --> A4
  A4["kvcalloc explored_states hash table"] --> B0

  subgraph FRONT["Front end -- structure and types"]
    B0["check_btf_info_early()"] --> B1["add_subprog_and_kfunc()"]
    B1 --> B2["check_subprogs()"]
    B2 --> B3["check_btf_info()"]
    B3 --> B4["check_attach_btf_id()"]
    B4 --> B5["resolve_pseudo_ldimm64()<br/>map fd -> real struct bpf_map *"]
    B5 --> B6["check_cfg()<br/>the DAG / reachability pass"]
    B6 --> B7["mark_fastcall_patterns()<br/>(new in 6.12)"]
  end

  B7 --> C0["do_check_main()<br/>then do_check_subprogs()<br/>-- THE path walk"]

  C0 --> D0
  subgraph BACK["Back end -- rewrites, only if the walk passed"]
    D0["remove_fastcall_spills_fills()"] --> D1["check_max_stack_depth()"]
    D1 --> D2["optimize_bpf_loop()<br/>inline bpf_loop into a real loop"]
    D2 --> D3{"privileged?"}
    D3 -->|"yes"| D4["opt_hard_wire_dead_code_branches()<br/>opt_remove_dead_code()<br/>opt_remove_nops()"]
    D3 -->|"no"| D5["sanitize_dead_code()<br/>replace dead insns with traps"]
    D4 --> D6["convert_ctx_accesses()<br/>ctx+off -> real struct offsets"]
    D5 --> D6
    D6 --> D7["do_misc_fixups()<br/>inline map lookups, patch kfuncs,<br/>expand may_goto, insert Spectre masks"]
    D7 --> D8["opt_subreg_zext_lo32_rnd_hi32()"]
    D8 --> D9["fixup_call_args()"]
  end

  D9 --> E0["print_verification_stats()<br/>bpf_vlog_finalize()<br/>commit used_maps / used_btfs<br/>kvfree(env)"]
  E0 --> E1["return 0, or -EACCES / -E2BIG / -EINVAL"]

The actual ordered phases of bpf_check() in Linux 6.12. What it shows: the path walk (do_check_main) sits in the middle of a front end that establishes structure and types and a back end that rewrites the bytecode. Two branches are privilege-dependent: unprivileged verification takes a global mutex, and dead code is neutered rather than removed for unprivileged loaders. The insight to take: “the verifier” is not one algorithm; a rejection can come from any of about fifteen phases, and roughly half of them run after your program has already been proven safe — which is why the bytecode the JIT sees is not the bytecode you submitted.

Mechanical Walk-Through: Inside bpf_check()

The entry point is int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u32 uattr_size) (verifier.c, v6.12, line 22300). It is called from bpf_prog_load() in kernel/bpf/syscall.c, the kernel-side handler for the BPF_PROG_LOAD command of the bpf() syscall. Tracing the function top to bottom is the most honest way to understand what “verification” actually consists of.

1. Allocate the verification environment. bpf_check() allocates a struct bpf_verifier_env with kvzalloc(); the source comment explains why it is not a global — the struct “is not small”, so it is allocated and freed per call. This env is the verifier’s entire scratchpad: the program, the per-instruction auxiliary array (insn_aux_data, one struct bpf_insn_aux_data per instruction, allocated with vzalloc() and each entry seeded with orig_idx = i so later instruction-patching passes can map rewritten instructions back to their originals), the current abstract state (cur_state), the table of already-explored states (explored_states), running counters (insn_processed, peak_states, total_states, max_states_per_insn), and the log buffer.

2. Resolve privilege from the BPF token. Five separate booleans are read out of the loading process’s credentials, all routed through bpf_token_* so that a BPF token can grant them without full capabilities: env->bpf_capable (CAP_BPF), env->allow_ptr_leaks, env->allow_uninit_stack, env->bypass_spec_v1 and env->bypass_spec_v4. These are not one switch. bpf_capable decides whether loops are allowed through check_cfg() and whether 1M instructions may be submitted; allow_ptr_leaks decides whether a pointer may be compared or spilled in ways that could reveal a kernel address; the bypass_spec_* pair decides whether Spectre-v1 index masking and Spectre-v4 store-bypass mitigations are inserted. A program that verifies for root can be rejected verbatim for an unprivileged loader, and it is worth knowing which of the five knobs was responsible.

3. Initialize the log, and — if unprivileged — take a global lock. bpf_vlog_init() wires up the caller-supplied log_level, log_buf, and log_size from bpf_attr. Then comes a detail that surprises people: if (!is_priv) mutex_lock(&bpf_verifier_lock);. Unprivileged verification is serialised across the entire machine by one mutex, to protect a few verifier globals. Privileged verification runs concurrently. If you are loading many programs at once from an unprivileged context, they queue.

4. Front-end structural and type passes. In order: check_btf_info_early() and check_btf_info() validate the BPF Type Format (BTF) debug data that accompanies the program; add_subprog_and_kfunc() and check_subprogs() discover subprogram boundaries and BPF-to-BPF call targets; check_attach_btf_id() resolves the attach target for fentry/fexit/LSM/struct_ops programs; resolve_pseudo_ldimm64() rewrites the pseudo ld_imm64 instructions that carry map file descriptors into real struct bpf_map * pointers (and it is here, in add_used_map(), that a program referencing more than MAX_USED_MAPS = 64 maps is rejected with “The total number of maps per program has reached the limit of 64”); check_cfg() performs the CFG pass; and mark_fastcall_patterns() — new in 6.12 — identifies calls whose register spills around them can later be elided.

5. The path walk: do_check_main() → do_check_common() → do_check(). do_check_common() allocates a fresh bpf_verifier_state, sets up frame 0 with the program’s input register (R1 = pointer to the context, type PTR_TO_CTX), and calls do_check(). Then do_check_subprogs() runs: global subprograms are additionally verified standalone, entered with unknown arguments, not only inline at their call sites. do_check() itself is an unbounded for (;;) loop, dissected in the next section.

6. Post-verification rewrite passes. A subtle and often-missed point: the verifier does not only judge the program, it rewrites it. remove_fastcall_spills_fills() deletes now-provably-unnecessary spills; check_max_stack_depth() computes the total stack footprint across the call graph (rejecting if it exceeds MAX_BPF_STACK = 512 bytes, or if the call chain exceeds MAX_CALL_FRAMES = 8); optimize_bpf_loop() replaces a bpf_loop() helper call with an inlined loop; the dead-code passes run differently by privilege (removed for privileged loaders, replaced by trapping instructions via sanitize_dead_code() otherwise); convert_ctx_accesses() rewrites every *(ctx + offset) access into the real in-kernel structure offset — this is how a portable skb->len access becomes a concrete load; and do_misc_fixups() does the heavy patching: inlining map lookups, expanding may_goto, patching kfunc calls, and inserting Spectre bounds masks. Then opt_subreg_zext_lo32_rnd_hi32() inserts the zero-extensions some JITs need, and fixup_call_args() finalises BPF-to-BPF call offsets. Only after all of this is the (now-modified) program returned through *prog = env->prog, ready for the BPF JIT Compiler.

7. Finalize and clean up. env->verification_time is recorded, print_verification_stats() emits the famous summary line, bpf_vlog_finalize() flushes the log and reports log_true_size back to userspace, the used-maps and used-BTFs lists are committed into prog->aux, env->prog->aux->verified_insns records the work done, and the environment is freed. The return value is the verdict: 0 for accept, or a negative errno (-EACCES for an unsafe program, -E2BIG for too-large, -EINVAL for malformed) propagated back to the bpf() syscall.

The stats line is worth memorising, because it is the primary instrument for diagnosing complexity problems. Its exact format in v6.12 is:

processed %d insns (limit %d) max_states_per_insn %d total_states %d peak_states %d mark_read %d

processed is env->insn_processed (the analysis budget consumed, not your program’s length); limit is always 1000000; max_states_per_insn is the worst single instruction’s cached-state count; total_states counts every checkpoint ever created and peak_states the high-water mark of live ones; mark_read is longest_mark_read_walk, how far the liveness propagation had to walk. With log_level including BPF_LOG_STATS (bit value 4) you additionally get verification time %lld usec and a stack depth A+B+C breakdown, one number per subprogram.

Inside do_check(): The Per-Instruction Loop

do_check() is where the abstract machine actually steps. Each iteration of its for (;;) loop does the same seven things, in this order.

stateDiagram-v2
  [*] --> Fetch
  Fetch: Fetch insn at env->insn_idx<br/>class = BPF_CLASS(insn->code)
  Fetch --> Budget
  Budget: ++env->insn_processed > 1M ?
  Budget --> Reject_E2BIG: yes
  Budget --> Prune: no
  Prune: is_prune_point(insn_idx) ?<br/>then is_state_visited()
  Prune --> PopNext: equivalent state found<br/>log 'N: safe'
  Prune --> Yield: no equivalent state
  Yield: signal_pending -> -EAGAIN<br/>need_resched -> cond_resched()
  Yield --> Log
  Log: if log_level: print insn +<br/>scratched register state
  Log --> Dispatch
  Dispatch: switch on instruction class
  Dispatch --> ALU: BPF_ALU / BPF_ALU64<br/>check_alu_op()
  Dispatch --> MEM: BPF_LDX / BPF_STX / BPF_ST<br/>check_mem_access()
  Dispatch --> CALL: BPF_JMP + BPF_CALL<br/>check_helper_call / kfunc / subprog
  Dispatch --> JMP: BPF_JMP conditional<br/>check_cond_jmp_op()
  Dispatch --> EXIT: BPF_EXIT
  ALU --> Advance
  MEM --> Advance
  CALL --> Advance
  JMP --> Fork
  Fork: push_stack() the not-taken side<br/>refine bounds on both sides
  Fork --> Advance
  Advance --> Fetch
  EXIT --> PopNext
  PopNext: update_branch_counts()<br/>pop_stack()
  PopNext --> Fetch: another state queued
  PopNext --> [*]: stack empty -> program accepted
  ALU --> Reject_EACCES: rule broken
  MEM --> Reject_EACCES: rule broken
  CALL --> Reject_EACCES: rule broken
  Reject_EACCES --> [*]
  Reject_E2BIG --> [*]

One iteration of do_check(), as a state machine. What it shows: every instruction costs one unit of the million-instruction budget before anything else happens; pruning is attempted only at instructions marked as prune points; and the dispatch is on the instruction class (the low three bits of the opcode byte), each class routing to its own checker. A conditional jump is the only thing that grows the work queue. The insight to take: the budget is consumed per simulated instruction per path, not per instruction in your program — so the cost of a program is (roughly) its instruction count multiplied by the number of distinct states that survive pruning, which is why branchy code is expensive and why push_stack() at conditional jumps is the thing to think about when you are over budget.

Two details in that loop repay attention. First, if (signal_pending(current)) return -EAGAIN; and if (need_resched()) cond_resched(); — verification of a large program can take seconds of CPU, so it is preemptible and interruptible. A Ctrl-C during a slow load really does abort the verifier. Second, the dispatch key is BPF_CLASS(insn->code), which is the low three bits of the first byte of the instruction. That single byte is the reason the verifier can be written as a flat switch:

packet-beta
0-7: "code (opcode: class in bits 0-2)"
8-11: "dst_reg"
12-15: "src_reg"
16-31: "off (s16 branch/memory offset)"
32-63: "imm (s32 immediate)"

The 64-bit struct bpf_insn encoding that do_check() decodes, drawn at bit accuracy. What it shows: one fixed-width 8-byte instruction — an opcode byte, two 4-bit register numbers packed into one byte, a signed 16-bit offset, and a signed 32-bit immediate. BPF_CLASS(code) is code & 0x07, so the instruction family — load, store, ALU, jump — is in the bottom three bits of byte 0 (bpf_common.h, v6.12; bpf.h uapi, v6.12). The insight to take: the fixed 8-byte width and the class-in-low-bits layout are not aesthetic choices — they are what makes a single-pass, single-switch verifier and a nearly one-to-one JIT possible. The one exception is ld_imm64, which occupies two consecutive bpf_insn slots, and check_cfg() explicitly rejects a “jump into the middle of ldimm64 insn”.

The Abstract State: What the Verifier Actually Carries

At the centre of everything is the per-path abstract machine state. It is a three-level structure, and knowing the shape makes verifier log output legible.

classDiagram
  class bpf_verifier_env {
    +bpf_prog* prog
    +bpf_verifier_state* cur_state
    +bpf_verifier_state_list** explored_states
    +bpf_insn_aux_data* insn_aux_data
    +u32 insn_processed
    +u32 total_states
    +u32 peak_states
    +bool bpf_capable
    +bool allow_ptr_leaks
    +bool bypass_spec_v1
  }
  class bpf_verifier_state {
    +bpf_func_state* frame[MAX_CALL_FRAMES=8]
    +bpf_verifier_state* parent
    +u32 branches
    +u32 curframe
    +bool speculative
    +u32 dfs_depth
    +u32 may_goto_depth
    +bpf_jmp_history_entry* jmp_history
  }
  class bpf_func_state {
    +bpf_reg_state regs[MAX_BPF_REG=11]
    +bpf_stack_state* stack
    +u32 callsite
    +u16 subprogno
  }
  class bpf_reg_state {
    +bpf_reg_type type
    +s32 off
    +tnum var_off
    +s64 smin_value / smax_value
    +u64 umin_value / umax_value
    +s32 s32_min_value / s32_max_value
    +u32 u32_min_value / u32_max_value
    +u32 id
    +bool precise
    +bpf_reg_liveness live
    +bpf_reg_state* parent
  }
  class tnum {
    +u64 value
    +u64 mask
  }
  bpf_verifier_env "1" --> "1" bpf_verifier_state : cur_state
  bpf_verifier_state "1" --> "0..8" bpf_func_state : frame[]
  bpf_func_state "1" --> "11" bpf_reg_state : regs[]
  bpf_func_state "1" --> "0..64" bpf_reg_state : spilled stack slots
  bpf_reg_state "1" --> "1" tnum : var_off

The abstract-state object graph in v6.12. What it shows: the environment holds one current state; a state holds up to eight call frames (MAX_CALL_FRAMES); each frame holds eleven registers and the stack slots it has touched (512 bytes / 8 = at most 64 slots); each register carries a type, a fixed offset, four independent min/max pairs, and a tnum. The insight to take: a single verifier “state” is a fairly large object — this is why peak_states matters for memory, why copy_verifier_state() is a real cost, and why the pruning heuristics work so hard to avoid saving checkpoints that will never match.

The register type field is the discriminator. In v6.12 enum bpf_reg_type has 22 base values plus flag-combined variants: NOT_INIT (never written, unreadable), SCALAR_VALUE (a number, not usable as a pointer), and the pointer family — PTR_TO_CTX, CONST_PTR_TO_MAP, PTR_TO_MAP_VALUE, PTR_TO_MAP_KEY, PTR_TO_STACK, PTR_TO_PACKET_META, PTR_TO_PACKET, PTR_TO_PACKET_END, PTR_TO_FLOW_KEYS, PTR_TO_SOCKET, PTR_TO_SOCK_COMMON, PTR_TO_TCP_SOCK, PTR_TO_TP_BUFFER, PTR_TO_XDP_SOCK, PTR_TO_BTF_ID, PTR_TO_MEM, PTR_TO_ARENA, PTR_TO_BUF, PTR_TO_FUNC, CONST_PTR_TO_DYNPTR — each combinable with PTR_MAYBE_NULL to give the *_OR_NULL variants that a map lookup or socket lookup returns (include/linux/bpf.h, v6.12). PTR_TO_ARENA is the newest of these, arriving with BPF_MAP_TYPE_ARENA in Linux 6.9. The pointer-type rules are the subject of Verifier Memory Safety and Pointer Types; the four bound pairs and their interaction are Verifier Register State Tracking. What matters at this altitude is only that the verifier’s “state” is a typed, range-annotated snapshot of all registers and stack, and it carries one such snapshot down every path.

Tnums: The Arithmetic of Partial Knowledge

kernel/bpf/tnum.c is 213 lines and is the most elegant file in the subsystem; reading it is the fastest way to feel how the verifier reasons. A tnum (“tracked” or “tristate” number) represents a set of possible 64-bit values by recording, per bit, whether that bit is known-0, known-1, or unknown. It is two u64s:

struct tnum { u64 value; u64 mask; };

The invariant is that a 1 in mask marks an unknown bit, and value carries the known bits (a bit must never be 1 in both). verifier.rst gives the canonical worked example: read a byte from memory into a register and “the register’s top 56 bits are known zero, while the low 8 are unknown — which is represented as the tnum (0x0; 0xff). If we then OR this with 0x40, we get (0x40; 0xbf), then if we add 1 we get (0x0; 0x1ff), because of potential carries.”

Step	Operation	tnum (value; mask)	Low 9 bits, x = unknown	What the verifier now knows
1	r0 = *(u8 *)(ptr)	(0x0; 0xff)	0 xxxxxxxx	0 ≤ r0 ≤ 255
2	r0 |= 0x40	(0x40; 0xbf)	0 x1xxxxxx	bit 6 is now definitely 1
3	r0 += 1	(0x0; 0x1ff)	x xxxxxxxx	the carry destroyed all bit knowledge

A tnum losing precision across three instructions, from verifier.rst’s own example. What it shows: OR with a constant is precision-preserving (it pins bit 6 to 1), but ADD is not — a carry can propagate arbitrarily far, so the addition of a known 1 to a value with unknown low bits forces the verifier to mark bit 8 unknown too. The insight to take: this is exactly why the verifier “forgets” things you think it should know, and why bitmasking (val &= 0xff) is the standard trick to hand precision back to it. tnum_and() can only narrow the unknown set; tnum_add() can only widen it.

The tnum_add() implementation is five lines and worth walking symbol by symbol, because it shows that this is real abstract interpretation rather than bookkeeping:

struct tnum tnum_add(struct tnum a, struct tnum b)
{
        u64 sm, sv, sigma, chi, mu;
 
        sm = a.mask + b.mask;      /* sum of the unknown-bit masks */
        sv = a.value + b.value;    /* sum of the known parts       */
        sigma = sm + sv;           /* total sum if every unknown bit were 1 */
        chi = sigma ^ sv;          /* bits that DIFFER between the two extremes */
        mu = chi | a.mask | b.mask;/* newly-unknown bits, plus the originally unknown ones */
        return TNUM(sv & ~mu, mu);
}

Reading it: sv is the sum you would get if every unknown bit were zero, and sigma is the sum you would get if every unknown bit were one. Any bit position where those two sums differ (chi) is a position that a carry could have reached, so it must become unknown. mu unions that carry-reachable set with the bits that were already unknown in either operand, and the result keeps only the known bits of sv outside mu. The whole thing is branch-free and costs a handful of ALU operations — which is why the verifier can afford to do it on every arithmetic instruction on every path.

The rest of the file is the same idea applied to the other operators. Four of them deserve names:

Function	Role	Precision behaviour
tnum_range(min, max)	Build the tightest tnum covering an interval	Uses fls64(min ^ max) to find the highest differing bit and marks everything below it unknown — so tnum_range(0, 255) is exact but tnum_range(0, 200) widens to 0–255
tnum_and / tnum_or / tnum_xor	Bitwise ops	and and or can gain knowledge (a known 0 in either operand of and forces a known 0 out); xor never gains
tnum_mul	Multiplication	Shift-and-add over the multiplier’s bits. The comment cites the algorithm’s source paper directly: arXiv:2105.05398, “Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers” (Vishwanathan, Shachnai, Narayana, Nagarakatte, 2021) — the verifier’s multiplication was replaced by a formally verified algorithm from a paper, which is unusual and worth knowing
tnum_in(a, b)	“Is every value in b also in a?”	The subset test that state pruning depends on — see below

tnum_is_aligned() is the other one you meet in practice: !((a.value | a.mask) & (size - 1)) — a pointer’s alignment is provable exactly when neither its known nor its unknown bits reach below the alignment boundary. That single expression is what produces misaligned access off 4 size 8.

The tnum is only one of the verifier’s abstract domains; it runs alongside four independent min/max interval pairs (smin/smax, umin/umax, s32_min/s32_max, u32_min/u32_max) that cross-inform each other. That interplay, and its failure modes, is the subject of Verifier Register State Tracking and, from a program-analysis-theory angle, The eBPF Verifier as a Static Analyzer.

Termination: Back-Edges, Bounded Loops, and the may_goto Escape Hatch

The sentence “eBPF programs cannot have loops” was true until Linux 5.3 and is now wrong in an interesting way. What v6.12 actually does depends on privilege, and the split lives in one function.

check_cfg() is a straightforward iterative depth-first search over the instruction graph, labelling edges exactly as the textbook algorithm in the source’s own comment block does: tree-edge, back-edge, forward/cross-edge, with per-instruction states DISCOVERED = 0x10 and EXPLORED = 0x20. The decisive lines are in push_insn():

} else if ((insn_state[w] & 0xF0) == DISCOVERED) {
        if (env->bpf_capable)
                return DONE_EXPLORING;          /* privileged: allow the back-edge */
        verbose(env, "back-edge from insn %d to %d\n", t, w);
        return -EINVAL;                          /* unprivileged: reject outright */
}

So: an unprivileged loader still gets no loops at all, with the classic back-edge from insn N to M message. A CAP_BPF-capable loader has the back-edge waved through, and termination becomes the path walk’s problem. Andrii Nakryiko’s commit message for the fix that produced this shape says it plainly — an earlier attempt tried to allow only some back-edges and got it wrong, so “instead of trying to detect back edges in privileged mode, just assume every back edge is valid and let subsequent BPF verification prove or reject bounded loops” (commit 10e14e9652bf, 2023-11-09).

How does do_check() then prove termination? By brute force, moderated by pruning. Alexei Starovoitov’s original bounded-loops commit describes the mechanism in one sentence: “Allow the verifier to validate the loops by simulating their execution. Existing programs have used #pragma unroll to unroll the loops by the compiler. Instead let the verifier simulate all iterations of the loop.” The machinery he added was a parentage chain of bpf_verifier_state plus a branches counter recording how many child paths are still unexplored (commit 2589726d12a1, 2019-06-15). That counter is what makes loop detection possible: a cached state with branches > 0 is one the walk has not finished, so re-arriving at it means the search went round a cycle. If the re-arrival is exactly equal, the loop cannot make progress and the verifier emits infinite loop detected at insn %d. If it is merely equivalent, the loop has converged and can be pruned.

flowchart TD
  SRC["for (i = 0; i &lt; n; i++)"] --> CFG{"check_cfg sees<br/>a back-edge"}
  CFG -->|"!bpf_capable"| REJ1["-EINVAL<br/>'back-edge from insn N to M'"]
  CFG -->|"bpf_capable"| WALK["do_check simulates<br/>iteration 1, 2, 3, ..."]
  WALK --> CMP{"state at loop head<br/>seen before?"}
  CMP -->|"exactly equal,<br/>branches &gt; 0"| REJ2["-EINVAL<br/>'infinite loop detected at insn N'"]
  CMP -->|"equivalent<br/>(RANGE_WITHIN)"| CONV["converged -&gt; prune<br/>loop proved terminating"]
  CMP -->|"different"| BUDGET{"insn_processed<br/>&gt; 1,000,000 ?"}
  BUDGET -->|"yes"| REJ3["-E2BIG<br/>'BPF program is too large'"]
  BUDGET -->|"no"| WALK
  CONV --> OK["accepted"]

  ALT1["bpf_loop&#40;n, cb, ctx, 0&#41;<br/>since 5.17"] -.->|"verifier checks the<br/>callback ONCE, the count<br/>is a runtime argument"| OK
  ALT2["may_goto / cond_break<br/>since 6.10"] -.->|"hidden 8-byte stack counter<br/>initialised to BPF_MAX_LOOPS"| OK
  ALT3["open-coded iterators<br/>bpf_for/bpf_repeat, since 6.4"] -.->|"iter state ACTIVE -&gt; DRAINED<br/>proves eventual exit"| OK

The four routes a loop can take through the v6.12 verifier. What it shows: an unprivileged program’s loop dies immediately at check_cfg(); a privileged program’s loop is simulated iteration by iteration until either it converges (accept), it provably cannot progress (reject as infinite), or it burns the million-instruction budget (reject as too large). The three dotted paths are the escape hatches that turn an unbounded loop into a verifier-tractable one. The insight to take: “the verifier rejected my loop” has four completely different causes with four different fixes — raise privilege, reduce per-iteration state so it converges, add cond_break, or restructure into bpf_loop.

The may_goto instruction (Alexei Starovoitov, merged for 6.10, commit 011832b97b31) is the most interesting of the three because it is a compilation trick, not an analysis one. From the verifier’s point of view may_goto is a jump that might be taken; from the runtime’s point of view it must eventually be taken. do_misc_fixups() makes that true by reserving eight extra bytes of stack per subprogram, seeding them in the prologue, and expanding each may_goto into four real instructions:

/* subprogram prologue, inserted by the verifier: */
*(u64 *)(fp - stack_depth) = BPF_MAX_LOOPS;   /* 8 * 1024 * 1024 = 8,388,608 */
 
/* each `may_goto +off` becomes: */
r_AX = *(u64 *)(fp - stack_depth);            /* load the hidden counter   */
if (r_AX == 0) goto +off;                     /* exhausted -> take the jump */
r_AX -= 1;                                    /* otherwise burn one tick    */
*(u64 *)(fp - stack_depth) = r_AX;            /* store it back              */

The counter uses BPF_REG_AX, the hidden auxiliary register the JIT reserves, so it costs no user-visible register. The commit message is candid about the limits: cond_break (the C macro wrapping may_goto) “is not a full substitute for bpf_for()”, and a loop written with a literal for (i = 0; i < 100; cond_break, i++) still fails to converge because the verifier tracks i as a precise constant on every iteration; the documented workaround is to seed the induction variable from a global so it starts imprecise. That is a wonderfully concrete illustration of the general rule that precision is the enemy of convergence in this verifier.

bpf_loop() (Linux 5.17) attacks the problem from the other side: the loop count becomes a runtime argument, and the verifier checks the callback body exactly once. optimize_bpf_loop() then rewrites the helper call into a real inlined loop when the callback subprogram is statically known, with a runtime guard if (r1 > BPF_MAX_LOOPS) return -E2BIG at the top — so BPF_MAX_LOOPS is simultaneously the may_goto seed and the bpf_loop ceiling. Full treatment in Verifier Bounded Loops and Termination and, for the theory of why simulation rather than widening was chosen, The eBPF Verifier as a Static Analyzer.

The Analysis Budget and How Pruning Pays For It

Six constants govern how much work the verifier will do. They are scattered across three headers, and mixing them up is the single most common source of confusion about -E2BIG.

Constant	Value (v6.12)	Defined in	What it actually limits
BPF_MAXINSNS	4,096	include/uapi/linux/bpf_common.h	Program length submitted by an unprivileged loader
BPF_COMPLEXITY_LIMIT_INSNS	1,000,000	include/linux/bpf.h	Two things: program length for a CAP_BPF loader, and the analysis budget (insn_processed) during the walk
BPF_COMPLEXITY_LIMIT_STATES	64	kernel/bpf/verifier.c	Max cached states per instruction, unprivileged only (if (!env->bpf_capable && states_cnt > …))
BPF_COMPLEXITY_LIMIT_JMP_SEQ	8,192	kernel/bpf/verifier.c	Depth of the pending-state stack (env->stack_size)
MAX_BPF_STACK	512 bytes	include/linux/filter.h	Per-frame stack; check_max_stack_depth() sums across frames
MAX_CALL_FRAMES	8	include/linux/bpf_verifier.h	BPF-to-BPF call nesting depth
MAX_USED_MAPS	64	include/linux/bpf_verifier.h	Distinct maps a single program may reference
MAX_TAIL_CALL_CNT	33	include/linux/bpf.h	Runtime tail-call chain depth (not a verifier limit — enforced by the JIT)

The verifier’s hard limits at v6.12, with the header each is defined in. What it shows: the same number, 1,000,000, does double duty — a static cap on insn_cnt checked in bpf_prog_load() (syscall.c line 2695) and a dynamic cap on insn_processed checked inside do_check() (line 18320). The insight to take: a 200-instruction program can absolutely fail the 1M check. When you see Processed 1000001 insn, your program is not too long; your program has too many distinct reachable states, and the fix is to reduce branching or help pruning, not to delete lines.

The 1M figure is not original to bounded loops. It arrived in Linux 5.2, as a consequence of a separate round of verifier-performance work: LWN’s account of the period notes that “one important outcome of this work was increasing the size limitation for BPF programs in the 5.2 kernel; instead of 4096 instructions, a program can execute up to one million”, and that this headroom is precisely what made the brute-force loop-simulation approach practical a release later (Rybczyńska, LWN, 2019-07-31).

Pruning is what keeps insn_processed under the cap. At designated prune points, is_state_visited() compares the current state against every cached state recorded for that instruction; if a cached state is at least as general, the current path is already proven and is abandoned with a N: safe log line. “At least as general” is states_equal() → regsafe() per register, and for scalars it bottoms out in exactly the two functions you would hope: range_within(rold, rcur) && tnum_in(rold->var_off, rcur->var_off) — the new register’s interval must sit inside the old one, and its bit knowledge must be a superset. That is the payoff for building the abstract domains in the first place.

The heuristics around it are unusually frank about being heuristics. Checkpoints are only created once the walk has seen “at least 2 jumps and at least 8 instructions” since the last one, a rule the source justifies with measurements: “In tests that amounts to up to 50% reduction into total verifier memory consumption and 20% verifier time speedup.” Cached states that keep failing to match are evicted once sl->miss_cnt > sl->hit_cnt * n + n with n = 3 normally and 64 at forced checkpoints. And inside a loop, new checkpoints are throttled further — the comment does the arithmetic out loud for the worst case, r1 += 1; if r1 < 1000000 goto pc-2: “1M insn_processed limit / 100 == 10k peak states.” LWN’s contemporaneous reporting supplies the empirical motivation: analysis of real networking BPF programs found that “80% of the saved states will never be matched and, thus, will never prune a future search.”

The mechanics are the subject of Verifier Complexity Limits and State Pruning; what belongs here is the shape of the trade — the verifier spends memory on checkpoints to buy back time, and every heuristic in is_state_visited() is tuning that exchange rate.

The Verifier Is Also a Compiler Pass

The most under-appreciated fact about bpf_check() is that a successful verification changes your program. Three of the back-end passes matter enough to name.

convert_ctx_accesses() rewrites every access to the program’s context. A tracing program that writes skb->len compiles to a load at some BTF-derived offset; the verifier replaces it with a load at the offset the running kernel’s struct sk_buff actually uses, via the program type’s convert_ctx_access() callback. This is how one compiled object stays correct across kernel layouts, and it is the kernel-side half of the story CO-RE (Compile Once Run Everywhere) tells from the loader side.

do_misc_fixups() inlines helper calls. The most instructive case is bpf_map_lookup_elem() on an array map, which array_map_gen_lookup() in kernel/bpf/arraymap.c replaces with straight-line code — no function call survives:

/* the call `r0 = bpf_map_lookup_elem(map, key)` becomes, for an array map: */
r1 += offsetof(struct bpf_array, value);  /* r1 now points at element 0      */
r0 = *(u32 *)(r2 + 0);                    /* load the index from *key        */
if (r0 >= map->max_entries) goto +4;      /* out of range -> return NULL     */
r0 &= array->index_mask;                  /* Spectre-v1 mask (unless bypassed)*/
r0 <<= ilog2(elem_size);                  /* or `r0 *= elem_size` if not pow2 */
r0 += r1;                                 /* r0 = &array->value[index]        */
goto +1;
r0 = 0;                                   /* the NULL path                    */

Seven or eight instructions, no call, no locking. This is the concrete reason an array-map lookup in a hot XDP path costs almost nothing — and the index_mask line is the concrete reason an array map’s max_entries is silently rounded up to a power of two unless the loader has bypass_spec_v1 (see BPF and Spectre Hardening, and Hash and Array Maps for the map side of it).

sanitize_ptr_alu() and friends insert Spectre mitigations during the walk itself, recording an alu_state and alu_limit in insn_aux_data that do_misc_fixups() later expands into masking instructions. Related: the verifier explores speculative paths — a bpf_verifier_state carries a speculative flag, and states_equal() contains the rule “Verification state from speculative execution simulation must never prune a non-speculative execution one.” The verifier is modelling the branch predictor.

The Load Path End to End

sequenceDiagram
    autonumber
    participant App as Userspace app
    participant Lib as libbpf
    participant Sys as bpf() syscall<br/>(syscall.c)
    participant Ver as bpf_check()<br/>(verifier.c)
    participant JIT as arch JIT
    participant Hook as Attach point

    App->>Lib: bpf_object__load(obj)
    Lib->>Sys: BPF_MAP_CREATE (per map) -> map fds
    Lib->>Lib: apply CO-RE relocations,<br/>patch map fds into ld_imm64
    Lib->>Sys: BPF_PROG_LOAD {prog_type, insns,<br/>insn_cnt, license, log_*}
    Sys->>Sys: insn_cnt > (bpf_cap ? 1M : 4096) ? -> -E2BIG
    Sys->>Sys: privilege gates: CAP_BPF /<br/>CAP_NET_ADMIN / CAP_PERFMON
    Sys->>Sys: security_bpf_prog_load() (LSM hook)
    Sys->>Ver: bpf_check(&prog, attr, uattr)
    Ver->>Ver: front end: BTF, subprogs,<br/>resolve map fds, check_cfg
    Ver->>Ver: do_check_main + do_check_subprogs
    alt a rule is violated
        Ver-->>Sys: -EACCES + filled log_buf
        Sys-->>Lib: errno = EACCES
        Lib-->>App: load failed, print the log
    else budget exhausted
        Ver-->>Sys: -E2BIG "program is too large"
    else proven safe
        Ver->>Ver: back end: rewrite ctx accesses,<br/>inline helpers, patch may_goto
        Ver-->>Sys: 0, *prog = rewritten program
        Sys->>JIT: bpf_prog_select_runtime()
        JIT-->>Sys: native machine code
        Sys-->>Lib: prog fd
        Lib->>Hook: BPF_LINK_CREATE / type-specific attach
        Hook-->>App: running
    end

The full journey from bpf_object__load() to a running program. What it shows: three separate gates stand between userspace and execution — a size/privilege check in bpf_prog_load(), the Linux Security Module hook security_bpf_prog_load(), and then bpf_check() itself; and the program handed to the JIT is the verifier’s rewritten output, not the loader’s input. The insight to take: the verifier is the third gate, not the first. An EPERM before verification and an EACCES from verification are different problems, and neither is fixed by looking at the verifier log — which only exists for the EACCES case.

In practice almost nobody fills bpf_attr by hand, but seeing it once makes the sequence above concrete:

union bpf_attr attr = {
    .prog_type = BPF_PROG_TYPE_XDP,   /* chosen type fixes the rules + ctx shape */
    .insns     = (__u64)(unsigned long)insns,
    .insn_cnt  = n_insns,             /* <= 4096 unprivileged, <= 1,000,000 with CAP_BPF */
    .license   = (__u64)(unsigned long)"GPL",
    .log_level = 1,                   /* 1 = normal, 2 = per-state, +4 = stats */
    .log_buf   = (__u64)(unsigned long)log,
    .log_size  = sizeof(log),
};
int prog_fd = syscall(__NR_bpf, BPF_PROG_LOAD, &attr, sizeof(attr));

Line by line, and what happens on the kernel side:

• prog_type is chosen at load and is load-bearing: it selects which bpf_verifier_ops table governs the program — which fields of the context it may touch (via the is_valid_access() callback), which helpers it may call (get_func_proto()), and what return values are legal. The same bytecode is verified differently as an XDP program versus a tracing program. verifier.rst states the design goal directly: unlike classic BPF, which bolted a second checker onto the first for seccomp, “in case of eBPF one configurable verifier is shared for all use cases”.
• insn_cnt is checked first, in bpf_prog_load() (syscall.c, v6.12, line 2695): attr->insn_cnt == 0 || attr->insn_cnt > (bpf_cap ? BPF_COMPLEXITY_LIMIT_INSNS : BPF_MAXINSNS) returns -E2BIG. This is the program-size cap, distinct from the analysis-budget cap of the same number checked later inside do_check().
• log_level/log_buf/log_size request the verifier’s reasoning trace. Per the bpf(2) man page, log_buf receives “a multi-line string that can be checked by the program author in order to understand how the verifier came to the conclusion that the eBPF program is unsafe”, with the explicit warning that “the format of the output can change at any time as the verifier evolves”; log_level 0 means no log, and then log_buf must be NULL and log_size zero; if the buffer is too small the call fails with -ENOSPC (bpf(2)). A rejected-but-well-formed program returns -EACCES; a malformed one returns -EINVAL.
• The bpf() multiplexer dispatches BPF_PROG_LOAD to bpf_prog_load(), which copies in the instructions, applies the per-type capability gates, runs the LSM hook, and calls bpf_check(). If that returns 0, the program is JIT-compiled and a file descriptor is returned; userspace attaches it via a BPF link or a type-specific attach call.

The man page is older than the kernel it documents

bpf(2) still shows the pre-5.x bpf_attr layout (it lists kern_version, describes a bpf_create_map() wrapper, and truncates the program-type enum with “see /usr/include/linux/bpf.h for the full list”). It is authoritative for the shape of the interface and for the log_buf semantics quoted above, but for current fields and commands read include/uapi/linux/bpf.h from your kernel and The bpf() Syscall.

See libbpf and the BPF Loader for what actually fills bpf_attr, and Reading and Debugging Verifier Errors for how to decode the log_buf it fills.

Program Type Parameterizes Everything

One verifier, many rule sets. The prog_type field selects a struct bpf_verifier_ops whose callbacks are consulted throughout the walk.

Callback	Called from	What it decides
is_valid_access()	every PTR_TO_CTX load/store	Which byte ranges of the context struct this program type may read or write, and at what widths
convert_ctx_access()	convert_ctx_accesses()	How a logical context field maps onto the real in-kernel struct offset
get_func_proto()	check_helper_call()	Which of the ~200 helpers this program type may call, and each one’s argument and return types
gen_prologue()	convert_ctx_accesses()	Instructions injected at program entry (e.g. loading skb->data)
gen_ld_abs()	do_misc_fixups()	Legacy LD_ABS/LD_IND expansion for socket-filter-style programs
btf_struct_access()	PTR_TO_BTF_ID access	Whether a field of a kernel struct may be read or written by this program type

The per-program-type verifier hooks. What it shows: the same bytecode is checked against a different context layout, a different helper allowlist, and a different set of writable kernel fields depending on the prog_type chosen at load. The insight to take: “the verifier rejected this” is always relative to a program type. Moving a function from a kprobe program to an fentry program, or from tc to XDP, genuinely changes what verifies — which is why copying a snippet between program types so often fails.

There are further type-driven gates outside the ops table. check_map_prog_compatibility() refuses bpf_spin_lock, bpf_timer, bpf_wq, bpf_list_head and bpf_rb_root fields in maps used by tracing programs, and restricts sleepable programs to sixteen map types (array, hash, LRU, their per-CPU variants, ring buffers, local-storage, queue, stack, arena) with the message “Sleepable programs can only use array, hash, ringbuf and local storage maps” — see BPF Maps for that list in full. See also BPF Program Types.

Reading the Verifier Log

At log_level = 1 the log is a disassembly interleaved with register state, printed only for instructions whose state has changed since the last print. verifier.rst carries a worked rejection that is worth internalising because it is the single most common mistake in BPF:

0: (7a) *(u64 *)(r10 -8) = 0
1: (bf) r2 = r10
2: (07) r2 += -8
3: (b7) r1 = 0x0
4: (85) call 1                       ; bpf_map_lookup_elem
5: (7a) *(u64 *)(r0 +0) = 0
R0 invalid mem access 'map_value_or_null'

Reading it: instructions 0–3 build a key on the stack and load the map pointer; instruction 4 calls bpf_map_lookup_elem, which sets R0 to type PTR_TO_MAP_VALUE_OR_NULL; instruction 5 dereferences R0 without a null check, and the type name in the error message is the diagnosis. Inserting if (r0 == 0) goto exit; converts R0 to PTR_TO_MAP_VALUE on the fall-through path and the program verifies. The _OR_NULL suffix in a verifier error always means the same thing: you skipped a null check.

The other messages you will meet, mapped to their causes:

Message	Pillar	Usual cause
R2 !read_ok	uninitialized read	Reading a register or stack slot never written on some path
invalid indirect read from stack off -8+0 size 8	uninitialized read	Passing a stack pointer to a helper without filling the whole region first
R0 invalid mem access 'map_value_or_null'	memory safety	Missing null check after a lookup
misaligned access off 4 size 8	memory safety	tnum_is_aligned() failed — the offset’s low bits are not provably zero
invalid access to packet, off=... size=...	memory safety	Missing or insufficient data + N > data_end check
Unreleased reference id=1, alloc_insn=7	resource safety	A refcounted pointer (socket, dynptr, ringbuf record) leaked on some path
back-edge from insn 12 to 8	termination	A loop in an unprivileged program
infinite loop detected at insn 8	termination	A loop whose state does not change between iterations
BPF program is too large. Processed 1000001 insn	analysis budget	State explosion, not program length
fd 0 is not pointing to valid bpf_map	structural	Map fd not patched in — a loader bug, not a program bug

Full treatment, including log_level=2 state dumps and veristat, is in Reading and Debugging Verifier Errors.

The Honest Limits

The verifier’s incompleteness is not a rough edge; it is the daily experience of writing BPF, and being clear-eyed about it is more useful than any workaround list.

It rejects correct programs, by construction. Soundness plus decidability forces it. Any static analyzer that never accepts an unsafe program and always halts must reject some safe ones; the only question is which ones, and that is a moving target set by whichever abstract domains the current kernel implements. A program that fails on 6.1 may pass on 6.12 with no source change, and the reverse has also happened.

Precision and convergence pull in opposite directions. The verifier tracks scalars precisely when it must (to resolve branches) and imprecisely when it can (to make states match). A loop over a precisely-known induction variable creates a fresh, distinct state per iteration and blows the budget; the same loop over an imprecise variable converges in two or three. This is why the documented may_goto workaround is to make a variable less known — genuinely counter-intuitive advice that follows directly from how pruning works.

Refactoring changes verifiability in ways that feel arbitrary. Hoisting a bounds check out of a branch, inlining a function, or reordering two independent checks can all move a program across the accept/reject line, because they change where prune points land and which states are comparable. Cilium’s datapath is architected around this: programs are deliberately split with tail calls and subprograms so that no single verification unit approaches the complexity limit.

The verifier itself has been the vulnerability. Every soundness bug in a transfer function — a bounds calculation that is too optimistic, a missing _OR_NULL transition, a Spectre gadget the masking missed — is a full kernel compromise, because there is no runtime check behind it. That is the reason sysctl kernel.unprivileged_bpf_disabled defaults to on across mainstream distributions, and the reason allow_ptr_leaks, bypass_spec_v1 and bypass_spec_v4 exist as separate privileged relaxations rather than one flag. See Unprivileged BPF and Its Restrictions and BPF and Spectre Hardening.

There has been a serious argument that this whole design is wrong. The alternative — ship a proof with the program and have the kernel merely check the proof, rather than reconstruct it — is the proof-carrying-code idea, and it has been raised repeatedly in the BPF community precisely because a 22,000-line trusted analyzer in the kernel is a large attack surface. It has not been adopted; the verifier’s incremental, heuristic approach has instead absorbed one improvement after another. It remains the most interesting open question about the design.

Uncertain

Verify: the current state of the “move verification out of the kernel” debate, and whether any proof-carrying-code or userspace-verifier proposal has landed since 6.12. Reason: LWN’s coverage of this question (Articles/795037) could not be retrieved during this pass — lwn.net returned HTTP 429 rate limiting repeatedly under fleet load, so the argument above is stated from the kernel source’s own framing rather than from the discussion record. To resolve: read lwn.net/Articles/795037 (“Should verification be done in the kernel?”) and lwn.net/Articles/1017116 (“Taking BPF programs beyond one-million instructions”) when the rate limit clears, and check lore.kernel.org/bpf for follow-up threads. uncertain

Common Misunderstandings

• “The verifier runs my program.” No — it never executes your code. It simulates it abstractly over all possible inputs. A value the verifier prints as R0=scalar(umax=255) is not a value your program had; it is the set of values the verifier proved your program could have at that point.
• “Loops are banned.” Outdated, and the correct statement is privilege-dependent. Unprivileged loaders still get back-edge from insn N to M from check_cfg(). Privileged loaders have had bounded loops since Linux 5.3, plus bpf_loop() (5.17), open-coded iterators (6.4) and may_goto/cond_break (6.10). What is still banned for everyone is an unbounded loop the verifier cannot prove terminates.
• “-E2BIG means my program has too many instructions.” Maybe, but usually not. There are two different 1M checks: a static one on insn_cnt in bpf_prog_load(), and a dynamic one on insn_processed during the walk. The second fires when branching makes the verifier explore too many states — a few-hundred-instruction program hits it routinely.
• “The verifier only checks; it doesn’t change my program.” False, and consequentially so. convert_ctx_accesses(), do_misc_fixups(), optimize_bpf_loop() and the dead-code passes all rewrite the bytecode; an array-map lookup does not even survive as a function call. The instruction indices in a JIT dump will not match the indices in your verifier log.
• “If it’s safe, the verifier accepts it.” Not guaranteed. The verifier is sound but incomplete: it conservatively rejects some safe programs it cannot prove safe. This is a feature (soundness over completeness), and the everyday cost of it is fighting the verifier.
• “Verification is a fixed cost.” It is not, and it is not even parallel for everyone: unprivileged verification takes bpf_verifier_lock, a machine-wide mutex, so concurrent unprivileged loads serialise.
• “The verifier proves my program is correct.” It proves your program is safe — bounded, typed, terminating. It says nothing about whether your program does what you meant. A program that drops every packet verifies perfectly.

Alternatives and When to Choose Them

The verifier is one point on a spectrum of “how do you run extension code safely in a kernel”, laid out in the table at the top of this note. Three of the rows deserve a sentence about when you would actually pick them.

• Loadable kernel modules trust the code completely — no verification, full power, full danger. Choose these when you need capabilities eBPF cannot express (unbounded loops over unbounded data, arbitrary kernel API calls, your own locking discipline) and you fully own the code and the risk. The cost is that you now own crash-safety too.
• A runtime sandbox / interpreter confines code while it runs, paying a per-operation cost. eBPF’s own interpreter still exists as a fallback, but on modern hardened kernels CONFIG_BPF_JIT_ALWAYS_ON disables it and the verifier-plus-JIT path is mandatory — see BPF Interpreter vs JIT. The verifier’s load-time proof is exactly what lets eBPF skip the runtime sandbox.
• seccomp-BPF, the other in-kernel BPF, uses the much simpler classic-BPF checker (no general memory model, only the M[0-15] scratch slots) because its programs only filter syscall arguments. Choose it when that is all you need: it is far easier to reason about and available to unprivileged processes. See seccomp and Syscall Filtering and Seccomp and seccomp-BPF.

Production Notes

The verifier is simultaneously eBPF’s greatest strength and its most cited pain point, and the operational patterns that have grown around it are worth knowing before you meet them.

Complexity budgeting is an architectural constraint, not a tuning knob. Cilium — the largest production eBPF deployment — ships verifier-aware coding guidance because real datapath programs routinely approach the complexity limit. The standard mitigation is decomposition: split a large program into tail-called stages, each verified independently, or into global subprograms, which do_check_subprogs() verifies once standalone rather than re-verifying at every call site. Both trade a small runtime cost for a large verification-cost reduction.

Verification time is a real deployment risk. A program that verifies in 50 ms on your laptop can take seconds on a machine with a different Clang version, because register-spill decisions change how many states are created — LWN documents exactly this interaction, noting that newer Clang versions “spill fewer variables onto the stack, reducing state pruning”. Watch processed N insns in CI, not just pass/fail; veristat exists to diff that number across kernel and compiler versions.

Kernel upgrades change what verifies, in both directions. The verifier’s accept set grows with better bounds tracking and shrinks when a soundness fix removes an over-permissive path. Programs pinned to an LTS kernel are testing against a moving target every time that LTS takes a stable backport of a verifier fix.

The verifier is the security boundary, and it has been breached. Several Spectre-class and bounds-tracking bugs have allowed crafted programs to defeat the proof. The response has been layered: allow_ptr_leaks, bypass_spec_v1/v4 as separate privileged relaxations; unprivileged BPF disabled by default; the global bpf_verifier_lock for unprivileged loads; and speculative-path simulation inside the verifier itself. See BPF and Spectre Hardening and CAP_BPF and BPF Privilege Model.

The improvement loop is real and continuous. Every historical complaint about the verifier rejecting safe programs has driven a specific feature: spilled-variable tracking, register-to-register comparison, precise-scalar backtracking, bounded loops, bpf_loop, open-coded iterators, may_goto, fastcall spill elimination. If a pattern does not verify today, checking whether a newer kernel accepts it is a genuinely productive first move.

See Also

• BTF (BPF Type Format) — the type information the verifier reads to understand kernel structures; named five times above but never linked until now

• Verifier Register State Tracking — how the verifier knows each register’s type and value range (tnums, the four bound pairs, precision)

• Verifier Memory Safety and Pointer Types — the pointer-type lattice and the bounds/null discipline behind every load and store

• Verifier Bounded Loops and Termination — back-edges, bounded loops since 5.3, bpf_loop, open-coded iterators, may_goto

• Verifier Complexity Limits and State Pruning — the 1M instruction budget, state pruning, liveness, and regsafe()/states_equal()

• The eBPF Verifier as a Static Analyzer — the same machine viewed through the abstract-interpretation literature: domains, soundness, incompleteness, widening

• Reading and Debugging Verifier Errors — the developer’s-eye view: getting and decoding the verifier log

• The bpf() Syscall — the BPF_PROG_LOAD command that triggers verification

• libbpf and the BPF Loader — what actually fills bpf_attr and calls bpf()

• BPF JIT Compiler — what happens to a program after the verifier accepts it

• BPF Program Types — how the chosen type parameterizes the verifier’s rules

• BPF Maps — the map objects resolve_pseudo_ldimm64() binds into the program, and the per-type rules the verifier enforces on them

• BPF and Spectre Hardening — the speculative-execution mitigations the verifier inserts

• CAP_BPF and BPF Privilege Model — the five privilege booleans bpf_check() reads, and where they come from

• Linux eBPF MOC — the parent map; the verifier is the keystone of §2