The Verifier: Why eBPF Doesn't Crash the Kernel
Article 1 ended on a claim: it is precisely the eBPF virtual machine's constraints that let the verifier prove a program safe before allowing it to run. This article stops talking theory and instead lets the verifier reject a real program right in front of us — then fixes it so it passes.
What the verifier is and when it runs
When userspace calls the bpf() syscall to load a program, before the program is allowed to run, the kernel runs it through the verifier. The verifier does not execute the program; it symbolically executes it — walking every possible branch, and at each step tracking the state of each register: does this register hold a number or a pointer? A pointer to where (context, stack, packet, map)? What is the valid read/write range? For every memory-access instruction, it checks whether it is within the proven bounds; for the whole program, it proves there is no infinite loop (always terminates). Only when every branch is safe is the program loaded and JIT-ed.
The clearest way to see it is to make the verifier fail.
A rejected program
Write an XDP program (attached at the packet-receive hook) that reads the first byte of the packet — but forgets the bounds check:
// xdp_bad.bpf.c
SEC("xdp")
int xdp_bad(struct xdp_md *ctx)
{
void *data = (void *)(long)ctx->data;
char first = *(char *)data; // read without checking data_end
return first ? XDP_DROP : XDP_PASS;
}
Compile it to eBPF bytecode then load it with bpftool:
clang -O2 -g -target bpf -I/usr/include/x86_64-linux-gnu -c xdp_bad.bpf.c -o xdp_bad.bpf.o
sudo bpftool prog load xdp_bad.bpf.o /sys/fs/bpf/xdp_bad
libbpf: prog 'xdp_bad': BPF program load failed: -EACCES
libbpf: prog 'xdp_bad': -- BEGIN PROG LOAD LOG --
0: R1=ctx() R10=fp0
; void *data = (void *)(long)ctx->data;
0: (61) r1 = *(u32 *)(r1 +0) ; R1_w=pkt(r=0)
; char first = *(char *)data;
1: (71) r1 = *(u8 *)(r1 +0)
invalid access to packet, off=0 size=1, R1(id=0,off=0,r=0)
R1 offset is outside of the packet
-- END PROG LOAD LOG --
Error: failed to load object file
The load fails with -EACCES, and the verifier log tells exactly the story. Read it:
0: R1=ctx()— on entry to the program,r1is the context pointer (Article 1).- After instruction 0 (
r1 = *(u32 *)(r1 +0), loadingctx->data), the verifier recordsR1_w=pkt(r=0)—r1is now a packet pointer, with a safe read range = 0 bytes. It has not yet been proven to have any readable byte. - Instruction 1 tries to read 1 byte (
r1 = *(u8 *)(r1 +0)). The verifier blocks it:invalid access to packet, off=0 size=1—R1 offset is outside of the packet.
The verifier knows the packet pointer currently has read range 0, so a 1-byte read is over the fence — it does not let it through. It does not guess; it reasons from the register state it tracks.
The fix: give the verifier proof
The problem is not "reading the packet is forbidden" — it is that the verifier does not yet have proof that the read is safe. Give it the proof with a data_end check:
// xdp_good.bpf.c
void *data = (void *)(long)ctx->data;
void *data_end = (void *)(long)ctx->data_end;
if (data + 1 > data_end) // bounds check BEFORE reading
return XDP_PASS;
char first = *(char *)data; // now the verifier knows: safe
Loading this version passes:
sudo bpftool prog load xdp_good.bpf.o /sys/fs/bpf/xdp_good
sudo bpftool prog show pinned /sys/fs/bpf/xdp_good
3783: xdp name xdp_good tag b631b1acd6a53b63 gpl
loaded_at 2026-05-24T02:27:18+0000 uid 0
Inspect the bytecode to see what the check became:
sudo bpftool prog dump xlated pinned /sys/fs/bpf/xdp_good
1: (79) r2 = *(u64 *)(r1 +8) # r2 = data_end
2: (79) r1 = *(u64 *)(r1 +0) # r1 = data
3: (bf) r3 = r1
4: (07) r3 += 1 # r3 = data + 1
5: (2d) if r3 > r2 goto pc+3 # if data+1 > data_end then jump (skip the read)
Instruction 5: if r3 > r2 goto is exactly the check. The verifier uses it to narrow the range: on the not-taken branch (i.e. data+1 <= data_end), it can prove there is at least 1 byte safe to read, so the subsequent read instruction is valid. The data_end check in eBPF is not defensive ritual — it is how the programmer hands proof to the verifier. Without it the verifier cannot infer it on its own, so it rejects.
The verifier is a safety tool, not a security tool
A point easily misunderstood (Article 0 noted it): the verifier proves the program is "safe to run" — does not crash the kernel, does not read memory wrongly, always terminates. It does not consider the program's intent. A program perfectly valid to the verifier could still, for example, count packets to spy on traffic. The verifier guards "can this break the kernel," while "is this allowed to do this" is the business of eBPF load privileges (CAP_BPF) and system policy — a topic we will meet again in the security part.
🧹 Cleanup
sudo rm -f /sys/fs/bpf/xdp_good /sys/fs/bpf/xdp_bad # unpin -> free the program
rm -f /tmp/xdp_*.bpf.*
Unpinning frees the program; the node returns to 140 programs (Cilium only). The clang/libbpf-dev installed in this article is kept for Part III. Source code is at github.com/nghiadaulau/ebpf-from-scratch, directory 02-verifier.
Wrap-up
The verifier runs at load time (inside the bpf() syscall), before the program is allowed to run: it symbolically executes every branch, tracks each register's state (number/pointer, pointer to where, valid range), checks every memory access, and proves the program terminates. We saw it for real: an XDP reading a packet without checking data_end was rejected with -EACCES, with a log pointing right at R1_w=pkt(r=0) then R1 offset is outside of the packet — the verifier knows the packet pointer has read range 0. Adding a data_end check (which becomes the if r3 > r2 goto instruction) gives the verifier proof to narrow the range, and the program loads. The verifier is a safety tool (does not crash the kernel), not a security tool (does not consider intent) — this is the foundational reason eBPF can load foreign code into the kernel without being like a kernel module.
Article 3 moves to maps: an eBPF program runs and shuts off per event, keeping no variables between runs — maps are how it remembers state and talks to userspace.