What the eBPF Verifier Actually Guarantees

Every kernel extension mechanism before this one asked you to trust the author of a module, because a module runs with the kernel's own privileges and a bug in it is a bug in your machine. eBPF inverted that: it accepts foreign code into the kernel and refuses to run it until a static analyser has proved a short list of properties. That verifier, not the instruction set, is why the technology escaped the networking niche and became infrastructure.

The instruction set is almost incidental: a small register machine with a calling convention into kernel helpers is not novel. What was missing was an answer to "why should the kernel execute this and not a module?" The answer is that the verifier walks every reachable path before the program is jitted, and a program it cannot convince itself about never runs.

The Verifier Is the Product

The properties the verifier establishes are narrow and concrete. Every memory access must be to a region the program can prove it owns: its own 512-byte stack, a map value of a known size, a packet buffer inside the bounds the program has already checked. Pointer arithmetic is tracked by type, so an integer cannot be laundered into a pointer. Loops must be bounded so the analysis terminates. Helper calls are restricted to an allowlist for that program type, and the argument types are checked against each helper's signature.

That last constraint explains a lot of the ergonomics. A 512-byte stack is small, so anything resembling a buffer goes in a map. A loop must have a provable bound, so parsing a variable-length header means either a bounded counter or a lot of careful masking. And the instruction limit means the analysis has a ceiling, which is why very large generated programs hit a wall that has nothing to do with what the CPU can execute.

What it does not establish matters as much. It does not prove your program is correct, that its logic matches your intent, or that its map updates are race-free across CPUs. It proves bounds are finite, not that the program finishes quickly. It proves memory safety in a narrow sense and leaves the semantics of the data to you.

Why Observability Won, Not Filtering

Packet filtering was the first use and it is not the one that made eBPF ubiquitous. Observability did, for a reason that has nothing to do with performance: it required no change to the application. Attaching a probe to a kernel function, a tracepoint or a user-space symbol gives you data the application never agreed to emit, on a system you did not have to rebuild, and it can be turned off again in one command. That is a categorically different sales pitch from "rewrite your packet path."

The economics compound. Instrumentation used to mean a kernel module — a build, a signing story, a support contract — or a recompile with tracing baked in. eBPF meant a script on the machine you already have. When the cost of asking a question collapses, people ask questions they would never have budgeted for, and that is where most of the value came from.

Portability was the other half. The compiled-in struct offsets that make kernel modules fragile are solved by compiling once against BTF type information and letting the loader relocate field accesses at load time. You still need BTF on the target and a kernel new enough for the hooks, but it turned "works on our golden image" into "works on the fleet."

The Networking Case Is Real, and Narrower Than the Hype

In the packet path, eBPF's advantage is structural rather than incremental. Classic firewall rules are ordered lists, so cost scales with rule count: a thousand-rule chain is a thousand comparisons per packet. A map lookup is a hash or trie walk, so policy cost stops scaling with policy size. That is why the Kubernetes networking stack moved off long iptables chains.

XDP goes further by running before the kernel allocates a socket buffer, at the driver's receive hook, so a packet that is going to be dropped can be dropped at line rate without ever becoming an skb. That only works if the driver supports the hook and the program stays inside its per-packet budget. The moment you need to fragment, reassemble or track connection state across packets, you are back in the stack with maps holding the state, and the cost curve looks familiar again.

Where the Model Stops Being Cheap

The verifier is a static analyser with a combinatorial worst case. Programs with many branches and many distinct pointer states explode into states to explore, and the loader fails with a message about complexity rather than about a bug. That shapes design: unroll small loops, factor helper logic, avoid parsing the same header twice. You optimise for the analyser as well as the CPU.

The rest of the bill is operational. Your programs run in kernel context, so a logic error that writes past a map value is a kernel crash, not a segfault — the verifier prevents most of that, but the verifier itself is a large, security-critical piece of C with a history of CVEs, and it is the thing parsing untrusted input. Unprivileged loading is disabled by default on most distributions for exactly this reason, which means the tooling needs privilege even when the program does not.

Then there is the ordinary cost of running code in the hot path: per-CPU maps to avoid contention, attention to which NUMA node a map's memory lives on, and a tail-call ceiling that constrains how modular a program can be. None of it is a dealbreaker, and all of it is invisible until you are debugging an incident inside a program you cannot attach a debugger to.

What I Think

eBPF is the most consequential kernel interface of the last decade and it earned that by being boring about safety: it does not grant capability, it grants a proof obligation. The mistake teams make is treating the verifier as a formality between them and their program, when it is the specification. If you cannot express your intent so the analyser can bound it, that is information about your design.

My worry is the opposite of the usual one. The ecosystem is drifting toward ever more privileged agents with ever more hooks, each one individually verified and collectively unaudited, and the sum of them is a second kernel whose behaviour nobody can describe. Verification is a per-program property. It says nothing about what a fleet of six hundred programs does together, and that is the part of this model nobody has solved.