Inside the eBPF Verifier: Ensuring Program Safety and Complexity Bounds

At 3 AM, your XDP packet filter starts rejecting packets after a deployment. The verifier log shows “math between pkt pointer and register with unbounded min value is not allowed” buried in 50,000 lines of state exploration. You’ve just hit the eBPF verifier’s safety guarantees the hard way.

Why Loading Code Into the Kernel Is Terrifying

Running user code in kernel space is inherently dangerous. One null pointer dereference crashes the entire system. An infinite loop freezes the machine. Arbitrary memory access compromises security. Before eBPF, kernel modules could do all of this, requiring complete trust in the code.

The eBPF verifier solves this through static analysis that proves program safety before a single instruction executes. It’s not optional runtime checking—if the verifier can’t prove your program is safe, it never reaches the JIT compiler. This is why eBPF can safely run untrusted code at kernel privilege with near-native performance.

Two-Pass Verification: Building Proofs from Bytecode

The verifier runs two passes over your eBPF bytecode. First pass builds a directed acyclic graph to detect unreachable code and validate the control flow structure. No backward jumps were allowed before kernel 5.3—loops required explicit unrolling. Modern kernels permit bounded loops with provable iteration limits.

Second pass simulates program execution symbolically, tracking register state at every instruction. Each of the 11 eBPF registers (R0-R10) gets a type and value range. R1 starts as a context pointer, R10 is the stack pointer, R0 holds return values. The verifier explores every possible execution path, maintaining abstract state for each register.

Here’s what kills most programs: state explosion. Every conditional branch doubles the state space. A program with 10 branches has 1,024 possible paths. The verifier must explore each one, proving memory safety at every access. It prunes equivalent states aggressively—if register state at instruction N matches a previously seen state, that path terminates early.

Complexity Bounds: The 1 Million Instruction Wall

The verifier enforces hard limits: 1 million instructions maximum (including unrolled loops), 4,096 complexity units per path, 512-byte stack size, 32 tail call depth. These aren’t arbitrary—they prevent verification from taking minutes and guarantee bounded execution time in production.

Complexity accounting is multiplicative. A simple if-else adds minimal complexity. Nested conditionals inside a loop that runs 1,000 times? You’ll hit the limit fast. LinkedIn’s XDP programs had to restructure packet parsing loops to add explicit bounds checks every 100 iterations, resetting the verifier’s path complexity counter.

At Netflix, we hit stack limits in tracing programs. The verifier counted every inlined function’s stack frame. We moved large structs to per-CPU maps instead of stack variables, trading pointer indirection for verification success.

Register State Tracking: How Pointer Math Gets Proven Safe

Every pointer access requires proof of safety. For packet parsing, this means explicit bounds checking before every read. The verifier tracks pointer arithmetic symbolically:

R1 = pkt_start (packet pointer, unknown range)
R2 = pkt_end (packet end, known constant offset)
R3 = R1 + 14 (Ethernet header, unbounded)
if R3 > R2 goto reject (NOW R3 is bounded: pkt_start to pkt_start+14)
Read from R3 (SAFE - verifier proved bounds)

Skip the comparison? Verifier rejects with “invalid read from stack.” The error message references the abstract state where safety couldn’t be proven, not where your code looks obviously wrong.

Helper function arguments get type-checked strictly. bpf_map_lookup_elem expects ARG_CONST_MAP_PTR for arg 1 and ARG_PTR_TO_MAP_KEY for arg 2. Pass a packet pointer as the key? Rejected. The verifier maintains a whitelist of allowed helpers per BPF program type—XDP programs can’t call tracing-only helpers.

Production Reality: Reading Verifier Logs

When Cloudflare’s DDoS mitigation programs started failing verification, the default 16KB log buffer showed only “program too large.” We increased the buffer to 16MB via bpf_prog_load syscall to see the actual failure: register spilling exceeded limits. Solution: aggressive register reuse and reducing local variable count.

The verifier log shows every state transition: “R1=pkt(id=0,off=0,r=14), R2=pkt_end(id=0,off=0)” means R1 points into the packet with a 14-byte proven range, R2 marks packet end. Understanding this notation is critical for debugging complex programs.

Facebook runs millions of eBPF programs simultaneously. Verifier correctness is non-negotiable—one missed vulnerability in verification affects every program. This conservative analysis causes false rejections of safe programs, but that’s the tradeoff for kernel safety guarantees.

What You Can Verify Right Now

Load an eBPF program with full verifier logging:

attr.log_buf = log_buffer;
attr.log_size = 16 * 1024 * 1024; // 16MB log
attr.log_level = 2; // Detailed state tracking
bpf_prog_load(BPF_PROG_TYPE_XDP, &attr);

Use bpftool prog dump xlated id <ID> to see verified bytecode with register annotations. The output shows exactly what the verifier proved at each instruction.

For complexity issues, count your branches and loop iterations. Structure code to minimize state explosion—early returns reduce path count, bounded loops with explicit counters verify faster than complex exit conditions.

The verifier isn’t magic. It’s a conservative static analyzer that rejects programs it can’t prove safe. Understanding its perspective—abstract interpretation, symbolic execution, state pruning—transforms cryptic errors into actionable fixes. Your 3 AM debugging sessions get a lot shorter.

---

Building Your Own eBPF Programs

Github Link:

https://github.com/sysdr/howtech/tree/main/eBPF/ebpf_verifier

Let’s write actual code that demonstrates these concepts. You’ll create two programs: one that passes verification and one that fails, so you can see exactly how the verifier thinks.

Setting Up Your Environment

You’ll need a Linux system with kernel 5.3 or later (for bounded loop support) and these tools:

# Install required packages
sudo apt-get update
sudo apt-get install clang llvm gcc make libbpf-dev linux-headers-$(uname -r) bpftool

Create a project directory:

mkdir ebpf-verifier-demo
cd ebpf-verifier-demo
mkdir -p src/{passing,failing}

Program 1: Passing Verification (The Right Way)

Create src/passing/simple_pass.c:

// Simple XDP program that PASSES verification
// Key: explicit bounds check BEFORE memory access

#include <linux/bpf.h>
#include <linux/if_ether.h>
#include <linux/ip.h>
#include <bpf/bpf_helpers.h>

SEC("xdp")
int xdp_pass_simple(struct xdp_md *ctx) {
    void *data_end = (void *)(long)ctx->data_end;
    void *data = (void *)(long)ctx->data;
    
    // Calculate Ethernet header end
    struct ethhdr *eth = data;
    
    // CRITICAL: Bounds check BEFORE access
    // This is what the verifier needs to see
    if ((void *)(eth + 1) > data_end)
        return XDP_DROP;
    
    // Now safe to access - verifier has proven:
    // data <= eth < eth+1 <= data_end
    if (eth->h_proto == __builtin_bswap16(0x0800)) { // IPv4
        return XDP_PASS;
    }
    
    return XDP_DROP;
}

char _license[] SEC("license") = "GPL";

Why this passes: The verifier can prove that when we access eth->h_proto, the pointer is definitely within bounds. The if statement creates a guaranteed safe zone.

Program 2: Failing Verification (Common Mistake)

Create src/failing/no_bounds_check.c:

// XDP program that FAILS verification
// Missing the critical bounds check

#include <linux/bpf.h>
#include <linux/if_ether.h>
#include <linux/ip.h>
#include <bpf/bpf_helpers.h>

SEC("xdp")
int xdp_fail_no_check(struct xdp_md *ctx) {
    void *data_end = (void *)(long)ctx->data_end;
    void *data = (void *)(long)ctx->data;
    struct ethhdr *eth = data;
    
    // Missing bounds check here!
    // Should have: if ((void *)(eth + 1) > data_end) return XDP_DROP;
    
    // Direct access without verification - REJECTED
    if (eth->h_proto == __builtin_bswap16(0x0800)) {
        return XDP_PASS;
    }
    
    return XDP_DROP;
}

char _license[] SEC("license") = "GPL";

The verifier will reject this with an error like “invalid read from stack” or “R1 invalid mem access” because it can’t prove eth points to valid memory.

Compiling Your Programs

Create a Makefile:

CLANG := clang
ARCH := $(shell uname -m | sed 's/x86_64/x86/' | sed 's/aarch64/arm64/')

BPF_CFLAGS := -O2 -target bpf -D__TARGET_ARCH_$(ARCH)
BPF_CFLAGS += -Wall -Wextra

all: passing failing

passing:
	$(CLANG) $(BPF_CFLAGS) -c src/passing/simple_pass.c -o simple_pass.o

failing:
	-$(CLANG) $(BPF_CFLAGS) -c src/failing/no_bounds_check.c -o no_bounds_check.o

clean:
	rm -f *.o

Build them:

make all

The passing program compiles successfully. The failing program might compile but will be rejected when you try to load it into the kernel.

Testing with bpftool

Load the passing program:

sudo bpftool prog load simple_pass.o /sys/fs/bpf/simple_pass type xdp

This should succeed. Check the loaded program:

sudo bpftool prog show

Try the failing program:

sudo bpftool prog load no_bounds_check.o /sys/fs/bpf/no_bounds type xdp

This will fail with detailed verifier output showing exactly where and why it was rejected.

Reading Verifier Output

When the verifier rejects a program, it tells you exactly what went wrong. Look for lines like:

0: (61) r1 = *(u32 *)(r1 +0)
invalid bpf_context access off=0 size=4

This means: at instruction 0, you tried to read memory but the verifier couldn’t prove it was safe.

For the passing program, use:

sudo bpftool prog dump xlated id <ID>

Replace <ID> with the program ID from bpftool prog show. You’ll see annotations showing what the verifier learned at each step.

Experimenting Further

Try these modifications to understand the verifier better:

1. Add a bounded loop (kernel 5.3+):

for (int i = 0; i < 16; i++) {
    if ((void *)(eth + 1 + i) > data_end)
        break;
    // Process data
}

1. Remove the bounds check from the passing program and watch it fail

2. Add debug output using bpf_printk() to see execution flow

3. Increase complexity by adding nested conditionals and watch the verifier’s path explosion

What You’ve Learned

By building these programs, you’ve seen:

• How explicit bounds checking makes programs verifiable

• What verifier error messages actually mean

• The difference between compile-time (clang) and verification-time (kernel verifier) checks

• Why the verifier is conservative—it rejects anything it can’t prove safe

The key insight: the verifier doesn’t run your program. It mathematically proves that every possible execution path is safe. That’s why it’s so strict about bounds checks and why errors reference abstract states rather than obvious bugs.

Quick Reference: Common Verifier Errors

Error Message What It Means How to Fix “math between pkt pointer and unbounded register” Pointer arithmetic without proving bounds Add if (ptr + offset > pkt_end) check “invalid read from stack” Memory access before bounds proof Check bounds before accessing “program too large” Too many instructions (>1M) Simplify loops, reduce complexity “R0 !read_ok” Return value not set on all paths Ensure all branches set R0 “back-edge from insn X to Y” Unbounded loop (pre-5.3 kernels) Unroll loop or use kernel 5.3+

Going Further

The complete working demonstration with automated setup, multiple examples, and verification log analysis is available in the demo files. Run ./demo.sh to see all these concepts in action with color-coded output and real-time verification tracking.

Remember: the verifier is your friend. It prevents kernel crashes and security vulnerabilities by rejecting unsafe code before it ever runs. Learning to work with it—rather than against it—is essential for writing production eBPF programs.

Working Code Demo: