Chapter 2: The eBPF Virtual Machine - Verifier, JIT & the Safety Model

“eBPF is not ‘safe because it is simple’. It is safe because a proof checker refuses to load programs it cannot prove safe. The verifier is the product.”

Chapter 1 showed where eBPF hooks live. This chapter opens the box: what an eBPF program actually is, how the kernel proves it safe before it ever runs, how the JIT turns it into native code, and why all of this is the reason you can write kernel code without kernel modules. It is also the chapter where most newcomers get their first rejection - and learning to read a verifier rejection like a compiler error is a skill this book practices from Chapter 3 onward.

2.1 The eBPF Instruction Set: A Register Machine

An eBPF program is a sequence of instructions for a small, formally defined virtual machine. The classic description: 11 general-purpose 64-bit registers (r0 through r10), a program counter, a small set of instruction classes (ALU, jumps, memory, and the two special classes - calls to helpers and returns to the kernel), and no arbitrary memory access: the only memory an eBPF program may touch is its stack, the context passed in by the hook, and the maps it declares. Everything else must be reached through a helper.

The instruction encoding mirrors that of classic BPF (the packet filter language of tcpdump), extended to 64 bits:

Programs are limited in size (BPF_MAXINSNS, one million instructions on 6.x kernels) and, for most program types, may not contain unbounded loops - though bounded loops with an explicit upper bound have been accepted since Linux 5.3. The important consequence for you as a Rust programmer: the verifier must be able to prove that every loop terminates, every memory access is in-bounds, and every pointer stays valid - and it checks this statically, before the program runs.

2.2 Helpers: The Kernel’s Whitelist

An eBPF program cannot call arbitrary kernel functions. It can call only helpers: a curated, versioned list of kernel functions exposed to BPF, each one implemented in kernel/bpf/helpers.c and friends. The helper list is the kernel’s attack surface reduction: instead of giving programs the ability to call anything, the kernel gives them a fixed vocabulary - bpf_map_* for map access, bpf_skb_* and bpf_redirect* for networking, bpf_get_current_* for task introspection, bpf_ktime_get_ns for time - and proves at load time that every call instruction names a valid helper with the right signature.

For Rust users this is a moment of recognition: helpers are the kernel’s trait object for eBPF - a fixed, checked interface between the untrusted program and the trusted kernel. Aya models them as functions in aya_bpf::helpers, each with the exact signature the kernel expects; you call bpf_redirect() the same way you would call any other function, and the verifier checks the arguments at load time.

2.3 Maps: The Only Shared State

Between the kernel side and the userspace side of an eBPF program sits a map: a kernel-allocated data structure with a fixed key/value type, created by the userspace loader and referenced by the program through a file descriptor. Maps are the only state an eBPF program can share - with other programs, with the kernel, and with userspace. The map is also the only persistent thing: when the program that uses a map exits, the map can outlive it, which is how userspace reads counters long after a hook fired.

The map types that matter in this book (full treatment in Chapter 4):

Two map rules govern every design in this book: choose the map for the access pattern (a hot counter is PERCPU_ARRAY, not HASH), and define the key/value layout once, in one place, shared by kernel and userspace - in Rust, one #[repr(C)] struct in a shared module.

2.4 The Verifier: A Proof Checker in the Load Path

When userspace issues bpf(BPF_PROG_LOAD, ...), the kernel does not run the program. It runs the verifier: a static analyser that walks the instruction stream and builds a symbolic execution of the program with a per-register type and value range. The verifier’s checks, roughly in order of fame:

1. Type safety. Every register has a type: scalar, packet pointer, map value pointer, stack pointer, context pointer. Operations are checked against types; a scalar cannot be used as a pointer, and a packet pointer cannot be compared with a map pointer.
2. Bounds. Packet access is allowed only where the verifier can prove ptr + offset <= data_end. Map keys and values are bounds-checked against the map definition. Stack access is checked against the frame.
3. Termination. Loops must have a provable bound; recursion is forbidden entirely (the verifier rejects a program that could call itself).
4. No leaks / no dangling. Pointers that escape the program (e.g. into a map value) must be accompanied by the correct reference count; the verifier tracks references and rejects leaks.
5. Helper argument validation. Every helper call is checked against the helper’s declared argument types.

The verifier is a static checker: it does not run your program with test data, it proves properties over all possible executions. When it fails, it emits a rejection log - the invalid access to packet, off=42 size=4, R4=... messages that Chapter 14 teaches you to read like compiler errors.

# A real rejection (simplified), from bpftool prog load:
# libbpf: prog 'xdp_parse': BPF program load failed: Permission denied
# R2=pkt(id=0,off=14,r=14,imm=0) R2_w=pkt(off=14,r=14,imm=0) R10=fp0
# 12: (71) r1 = *(u8 *)(r2 + 20)     ; access beyond data_end
# invalid access to packet, off=20 size=1, R2 has 14 bytes of readable data

Read that message carefully: off=14 is where the packet pointer was, r=14 says only 14 bytes (the Ethernet header) are known readable, and the program tried to read byte 20 without first checking data_end. The fix - the one Chapter 5 makes second nature - is the explicit bounds check before every header field access.

2.5 The JIT: From Verification to Native Code

Verification is the price of safety; the JIT is the refund. After the verifier accepts a program, the kernel’s BPF JIT compiler translates the eBPF instructions into native instructions for the host architecture (x86-64, arm64, riscv, s390, and others). The JIT output runs with the same privileges as kernel code - which is precisely why verification is non-negotiable - and at the same speed as hand-written kernel code. For network programs the JIT output is what executes per packet; a well-shaped XDP program is, after JIT, a few dozen native instructions.

The two-step pipeline - verify, then JIT - is the architectural answer to a question that predates eBPF: how do you get kernel performance without kernel risk? Modules answer “trust the author”. eBPF answers “prove the program, then let it run”. For the systems engineer, the practical consequence is a new failure mode: a program can be syntactically valid Rust, semantically what you meant, and still rejected at load time because the verifier cannot prove a bound. Chapter 14 is devoted to this class of bug.

2.6 BTF and CO-RE: Programs That Survive Kernel Upgrades

There is one more piece of the model you will meet constantly: BTF (BPF Type Format), a compact type graph the kernel can emit for its own data structures, and CO-RE (Compile Once, Run Everywhere), the relocation system that lets one compiled program adapt to different kernels at load time. The problem: an eBPF program that reads struct task_struct directly would break when the kernel changes the struct. With CO-RE, the compiled program records which fields it needs as relocations; the loader rewrites the offsets against the running kernel’s BTF before the verifier sees the program. Aya and bpf-linker handle CO-RE relocations for you; the practical effect is that your Rust eBPF programs do not need to be recompiled for each kernel - only BTF-enabled.

BTF also gives you a debugging superpower: bpftool btf dump and pahole let you inspect kernel struct layouts precisely, which is how you write correct kprobe programs (Chapter 7) without guessing field offsets.

2.7 The Lifecycle: Load, Attach, Run, Unload

Put the pieces together and the lifecycle of an eBPF program is:

1. Compile (Chapter 3): Rust kernel-side code is compiled with the bpfel-unknown-none target and bpf-linker into a single ELF object containing the programs and their map definitions.
2. Load: the userspace side (Aya’s Ebpf::load) reads that ELF, creates the maps, and issues BPF_PROG_LOAD for each program. The verifier runs now - this is where rejections happen.
3. Attach: the program is attached to its hook (an interface for XDP, a qdisc for tc, a cgroup, a function for kprobes).
4. Run: the kernel invokes the program per event - per packet, per syscall, per event. It may read and write maps, and it returns an action the kernel obeys (XDP_DROP, TC_ACT_OK, …).
5. Unload: when the userspace process exits (or an explicit detach runs), the links are torn down and the programs and maps are freed.

Everything after step 3 is per packet or per event; everything before is control plane. Keeping those two planes separate - no map updates on the hot path, no loading on the hot path - is the discipline Chapter 13 turns into a performance methodology.

Source: code/ch02_ebpf_vm/verifier_notes.rs

// code/ch02_ebpf_vm/verifier_notes.rs
// Chapter 2 demo - the verifier's mental model, in Rust shapes.
// Portable: compiles and runs anywhere.
// Build: rustc verifier_notes.rs && ./verifier_notes
#![allow(dead_code)] // the demo only constructs Packet; keep the model complete

#[derive(Clone, Copy, Debug, PartialEq)]
enum RegType {
    Scalar,              // a plain number, no memory behind it
    Packet(u64),         // pointer into packet memory + known readable bytes
    MapValue,            // pointer into a map value
    Stack,               // pointer into the program's own stack frame
    Context,             // the hook-provided context pointer
}

struct Reg {
    ty: RegType,
    val: i64,   // known value (or the range bound the verifier tracks)
}

/// The check the verifier applies to a memory access: the requested extent
/// must fit inside the pointer's known-readable region.
fn check_read(reg: Reg, offset: u64, size: u64) -> Result<(), String> {
    match reg.ty {
        // A scalar has no memory: using it as a pointer is a type error.
        RegType::Scalar => Err("scalar register cannot be dereferenced".into()),
        // Packet pointers carry a 'readable bytes' count (r=... in logs).
        RegType::Packet(readable) => {
            let end = offset.checked_add(size).ok_or("offset overflow")?;
            if end <= readable {
                Ok(())
            } else {
                Err(format!("invalid access to packet, off={offset} size={size}, only {readable} bytes readable"))
            }
        }
        // Map/stack/context pointers are checked against their own sizes
        // at load time; nothing to prove here for the demo.
        RegType::MapValue | RegType::Stack | RegType::Context => Ok(()),
    }
}

fn main() {
    // The exact rejection from Section 2.4: byte 20 read when only the
    // 14-byte Ethernet header is known readable.
    let eth_only = Reg { ty: RegType::Packet(14), val: 0 };
    let rejection = check_read(eth_only, 20, 1).unwrap_err();
    println!("verifier: {rejection}");

    // The fix: prove data_end - data >= 24 BEFORE reading off=20 size=4.
    let checked = Reg { ty: RegType::Packet(24), val: 0 };
    match check_read(checked, 20, 4) {
        Ok(()) => println!("accepted after bounds check (r=24, off=20, size=4)"),
        Err(e) => println!("verifier: {e}"),
    }
}

The demo compiles and runs anywhere - the verifier it models only exists in the kernel. But the shape is the point: an eBPF program’s correctness is decided by what the verifier can prove, and the verifier’s vocabulary is types, readable ranges, and bounds. Every program in this book is written so that vocabulary is satisfied.

Hands-On Lab

# 1. Run the verifier-model demo: one rejection, one acceptance.
rustc code/ch02_ebpf_vm/verifier_notes.rs && ./verifier_notes

# 2. Meet the real verifier. Install bpftool, then try loading a
#    deliberately-bad program and read the log like a compiler error
#    (Chapter 14 decodes these lines).
sudo bpftool prog loadall /dev/null /sys/fs/bpf/demo 2>&1 | head

# 3. One-liner tracing: prove the hooks exist with bpftrace.
sudo bpftrace -e 'tracepoint:syscalls:sys_enter_execve { @[comm] = count(); }'

The skill to practise: reading invalid access to packet, off=N size=M, R2 has K bytes readable and knowing the fix is a bounds check before the read - it is the single most common eBPF rejection you will ever see.

Summary

• An eBPF program is a register-machine program with no arbitrary memory access: stack, context, maps, and helpers are its entire world.
• Helpers are the whitelist of kernel functions programs may call; the verifier checks every call at load time.
• Maps are the only shared state - with other programs, the kernel, and userspace - and the map type must match the access pattern.
• The verifier proves type safety, bounds, termination, and reference correctness statically, then the JIT compiles the program to native code. Load is the moment of judgment; runtime is native speed.
• BTF + CO-RE let one compiled program relocate against the running kernel’s type information - no per-kernel recompiles.
• The lifecycle is compile, load, attach, run, unload - and the load step is where the verifier lives.

Next: Chapter 3 brings it to Rust - the Aya toolchain, the project layout, and the load/attach lifecycle in code you can actually run.