AxisOps Harbour
Labs

Insights

The eBPF verifier, and what it refuses

eBPF usually gets introduced as a fast packet filter that grew up. That framing buries the achievement, which is this:

The Linux kernel accepts code from userspace and runs it in kernel context on the strength of a proof.

Classic BPF validated kernel-side too, and proof-carrying code is older still. What is new is the scope: running arbitrary programs against kernel data structures rather than filtering packets. The verifier is the proof, and if you want to understand it, look at what it refuses rather than what it permits.

What it checks

Before a program loads, the verifier does the following (LWN's description is the clearest):

  1. Walks the control-flow graph depth-first to establish termination. Unreachable instructions are rejected outright. Loops were forbidden entirely to begin with; bounded loops arrived later, with the verifier proving the bound.
  2. Simulates execution instruction by instruction, tracking the type and value range of every register and stack slot. Out-of-bounds jumps and out-of-range access are rejected.
  3. Rejects reads of uninitialised registers. A register the program has not written is unreadable: R0 and R2 to R5 at entry, since only R1 arrives holding the context, and R1 to R5 again after a helper call, when R0 comes back carrying the return value.
  4. Prunes paths already covered by a previously verified state, which is what keeps the whole thing tractable.
  5. Applies secure mode for a loader without CAP_SYS_ADMIN: pointer arithmetic is prohibited so kernel addresses cannot leak.
  6. Restricts helper calls by program type. A tracing program and an XDP program can call different things.

Why the refusals are the interesting part

The verifier is a conservative static analyser, so it rejects programs that are correct but that it cannot prove correct. Working with eBPF is largely the experience of being told no about something you can see is fine.

That is the real cost of the thing, and you learn from it. Take a pointer dereference the verifier can't bound, because the bound comes from a value it can't track; it gets rejected even though the invariant is sitting there in front of you. So you restructure the code until the invariant is visible to the analyser.

It's the same discipline as satisfying Rust's borrow checker. The work is making the correctness legible to a machine, not making the code correct.

A good exercise: write a program with an unbounded loop, or a map lookup dereferenced without a null check, and then read the verifier log. It prints the state it inferred at each instruction and where that state fell over. Once you learn to read it, it's one of the better error messages in systems software.

The cost model

A hardware boundary charges you on every crossing. The verifier charges once, at load time, and after that the crossing is free even though the work is not: no ring transition, no page table switch, no context switch. The program itself still costs what it costs, as JIT-compiled instructions, helper calls and map lookups on a hot path. What disappears is the price of the boundary, not the price of the check.

It's a bit like paying for a season ticket instead of buying a ticket for every journey. That shift is why eBPF scaled out of packet filtering into tracing, security enforcement and load balancing. The economics of "put a check in this hot path" changed completely.

A verifier willing to say no lets working engineers ask a running system a question it was not built to answer, without restarting it.

That sounds modest. It is the end of a whole genre of outage. The classic shape is a production problem that only appears under real traffic, where the instrumentation you need was not compiled in. The choice is to deploy a debug build and wait for the problem to recur, or to guess. With eBPF you attach a probe to the function you care about, on the box that is currently broken, and you have the answer in a minute. The class of bug that disappears is the unreproducible one, and it disappears because reproduction stops being the price of observation.

Where it goes next is scheduling and policy. Any kernel decision currently hard-coded into a subsystem, chosen by heuristics that accreted over fifteen years, is a candidate for being handed to a verified program that the operator supplies. Our bet is that this is the dominant direction for kernel development over the next five years: the kernel keeps the mechanism and the enforcement, and the policy moves out to code you can iterate on in minutes rather than across release cycles. From packet filtering to choosing which process runs next, with a verifier standing between user code and catastrophe.

The wider benefit is efficiency. Load balancing and packet processing that used to need a dedicated appliance now run on the host that was already there. For anyone running infrastructure on a small budget, in a cupboard, on a connection that comes and goes, the ability to do serious network work on commodity hardware is the difference between a plan and a quotation.

That access creates a quieter chokepoint.

eBPF's security model rests on the verifier being in the kernel you can read, and on you being allowed to load a program into your own machine. Both halves are under gentle pressure, from the direction of signing.

The argument for signed-only BPF is reasonable on its face. A privileged eBPF program is extremely powerful, it is a lovely place to hide, and a vendor shipping a locked-down appliance would rather only its own programs load. Follow that to its conclusion and you get a kernel that runs verified programs only from keys the platform owner trusts, where the platform owner is the hardware vendor or the cloud rather than you. The verifier still works. It just works on behalf of somebody else, and the general-purpose instrumentation capability quietly becomes a vendor feature.

The asymmetry is already visible in managed Kubernetes. Load your own BPF program on your own laptop: trivial. Do it on a managed node pool: that depends on what the provider permits, and increasingly the answer is their agent rather than your program. The capability has not been removed, it has been resold, and what you get back is dashboards rather than access.

This matters more than the average lock-in complaint because the kernel is now the last layer in a modern stack that an operator can inspect. The firmware is signed and closed. The management engine is closed. The accelerator firmware is closed. The hypervisor, if you are renting, is not yours. The Linux kernel is the one place left where you can read the code that is making the decision and, with eBPF, ask it what it is doing right now. That is a position worth defending specifically.

Here at AxisOps we run on hardware where we can load our own programs, and we treat "can I attach a probe to this" as a procurement question rather than a technical one. A system you cannot instrument is a system you are trusting somebody's description of.

What it does not give you

  • No security boundary against a malicious loader holding CAP_SYS_ADMIN. Secure mode is there for unprivileged loading; privileged eBPF is powerful by design.
  • No correctness proof of your logic. It proves memory safety and termination, and says nothing about whether your program does the right thing.
  • No stability across kernels. Verifier behaviour changes, so a program that loads on one kernel can be rejected on another. That's a real operational cost and it routinely gets understated.