The Linux eBPF Verifier

The eBPF Verifier is the gatekeeper of the Linux kernel. It is a static analysis engine built directly into the kernel that inspects every byte of eBPF bytecode loaded via the bpf() system call before permitting it to execute.

Because eBPF programs run directly inside the kernel's address space with supervisor CPU privileges, an unverified program with an out-of-bounds pointer or an infinite loop could crash the entire operating system kernel. The verifier mathematically guarantees that:

Memory Safety: Programs cannot access arbitrary, unmapped, or unauthorized kernel memory.
Termination: Programs are guaranteed to finish execution; infinite loops are strictly impossible.
Type Safety: Pointers cannot be leaked or fabricated out of raw integer registers.

       [ eBPF Bytecode from LLVM/Clang ]
                       │
                       ▼ bpf(BPF_PROG_LOAD)
┌────────────────────────────────────────────────────────┐
│                   eBPF VERIFIER                        │
│                                                        │
│  Phase 1: Control Flow Graph (DAG) Analysis            │
│  - Detects unreachable dead code                       │
│  - Rejects unbounded cycles and backward branches      │
│                                                        │
│  Phase 2: Abstract Interpretation & State Tracking     │
│  - Simulates every instruction along all paths         │
│  - Tracks register types (SCALAR vs PTR_TO_MAP_VALUE)  │
│  - Tracks pointer bounds (min_value <= offset <= max)  │
│  - Enforces NULL checks before pointer dereference     │
└──────────────────────────┬─────────────────────────────┘
                           │ Passed
                           ▼
┌────────────────────────────────────────────────────────┐
│                  JIT (Just-In-Time) Compiler           │
│        Converts verified bytecode to native x86/ARM    │
└────────────────────────────────────────────────────────┘

How the Verifier Works: Two-Pass Analysis

Pass 1: Control Flow Graph (CFG) Analysis

The verifier constructs a Directed Acyclic Graph (DAG) of the program's basic blocks:

Scans for unreachable instructions (dead code is rejected).
Checks instruction boundaries and valid jump offsets.
Ensures the program terminates with a valid exit instruction (BPF_EXIT_INSN).

Pass 2: Abstract Interpretation and State Tracking

The verifier simulates the execution of the program step-by-step along every possible branch:

Register State Tracking: The verifier maintains a virtual model of the 10 BPF registers (R0–R9, plus stack frame pointer R10). Each register is tagged with a precise type (e.g. NOT_INIT, SCALAR_VALUE, PTR_TO_STACK, PTR_TO_MAP_VALUE, PTR_TO_PACKET).
Range & Value Tracking: When arithmetic is performed (e.g. r1 += 4), the verifier updates upper and lower bounds (umin_value, umax_value, smin_value, smax_value).
Pruning: To prevent state space explosion, the verifier caches visited register states. If a branch reaches an identical or safer state already analyzed, the verifier prunes that branch.

Core Verifier Rules & Constraints

1. Pointer Dereferences Require Explicit Bounds

The verifier will instantly reject code that accesses memory based on dynamic offsets unless the offset has been explicitly checked against the buffer boundary:

// When inspecting network packets in XDP:
void *data = (void *)(long)ctx->data;
void *data_end = (void *)(long)ctx->data_end;

struct ethhdr *eth = data;

// COMPILER/VERIFIER REQUIREMENT:
// You MUST check if data + sizeof(*eth) exceeds data_end BEFORE dereferencing!
if ((void *)(eth + 1) > data_end) {
    return XDP_DROP; // Bounds check passed; verifier allows access
}

// Now the verifier knows eth->h_proto is safe to read
__u16 h_proto = eth->h_proto;

Without the (eth + 1) > data_end check, the verifier rejects the load with: invalid access to packet, off=0 size=14, R1(id=0,off=0,r=0) R1_p=14.

2. Mandatory NULL Checks on Map Lookups

bpf_map_lookup_elem() returns a pointer to the value inside a BPF map, or NULL if the key does not exist. The verifier assigns this return value the type PTR_TO_MAP_VALUE_OR_NULL.

Attempting to dereference the pointer before checking for NULL fails verification immediately:

__u32 *count = bpf_map_lookup_elem(&my_map, &key);

// REQUIRED NULL CHECK:
if (!count) {
    return 0; // Abort; key not found
}

// Verifier converts register type from PTR_TO_MAP_VALUE_OR_NULL to PTR_TO_MAP_VALUE
(*count)++;

3. Bounded Loops

Historically, eBPF banned all loops. Linux 5.3 introduced bounded loop support:

Loops must have an upper bound proven at compile time (e.g., #pragma unroll or loops whose iteration counter has provable ranges).
The verifier caps the total number of simulated instructions per program at 1,000,000 instructions (raised from 4,096 in older kernels).

Debugging: The Verifier Log Buffer

When the verifier rejects a program, it writes a detailed register trace into the user-supplied log buffer:

0: (bf) r6 = r1                       ; R6_w=ctx(off=0,imm=0)
1: (18) r1 = 0xffff88810234a000       ; R1_w=map_ptr(off=0,ks=4,vs=8,imm=0)
3: (85) call bpf_map_lookup_elem#1    ; R0_w=map_value_or_null(off=0,ks=4,vs=8,imm=0)
4: (61) r1 = *(u32 *)(r0 +0)
R0 invalid mem access 'map_value_or_null'
processed 5 insns (limit 1000000) max_states_per_insn 0 total_states 0 peak_states 0 mark_read 0

The log clearly pinpoints the error at instruction 4: register R0 is still map_value_or_null because the code failed to check if (!r0) before reading offset 0.

Frequently Asked Questions (FAQ)

Why does the eBPF verifier reject pointer arithmetic on stack pointers?

The verifier tracks exact stack offsets (PTR_TO_STACK) to prevent stack overflow and out-of-bounds reads into adjacent kernel memory frames. If code performs variable or unconstrained arithmetic on the stack pointer (R10), the verifier can no longer prove at compile time that the resulting address stays within the 512-byte eBPF stack limit, and rejects the program for safety.

What causes the "program too large" or "1000000 insn limit reached" error?

This error occurs when the verifier analyzes too many branch paths, exceeding the 1,000,000 instruction verification limit even if the actual bytecode is only a few hundred instructions. Complex nested loops, excessive inlining, or insufficient branch pruning force the verifier to simulate every possible permutation. Structuring code with helper functions, using bounded variables, or leveraging BPF-to-BPF function calls reduces verification complexity.

Does the eBPF verifier run when the program executes in production?

No. Verification happens only once, in user space during the bpf(BPF_PROG_LOAD) system call. Once the verifier approves the bytecode, the kernel's JIT compiler translates it into native machine code (x86-64 or ARM64) that executes at bare-metal speed with zero verification overhead during runtime events.