Debugging eBPF Programs: Tracing Verifier Failures and Map Interactions
The eBPF verifier is not a sandbox. It is a theorem prover — a static analysis engine that either constructs a proof that your program is safe, or rejects it. If you treat it as a runtime guard you can negotiate with, you will spend hours confused. If you treat it as a formal type checker with specific rules about pointer provenance and value ranges, debugging becomes systematic.
The Verifier’s Mental Model
The verifier performs a single-pass, depth-first traversal of your program’s control-flow graph. At each instruction, it maintains abstract state: for every register, it tracks whether the value is a scalar (unknown integer), a known constant, a pointer to a map value, a pointer to the packet context, or one of about a dozen other types. The moment you touch memory through a pointer, the verifier checks that the pointer type permits that access and that the offset is within bounds. It does this statically — no execution, no sampling.
What trips engineers is that the verifier does not track semantic equivalence across branches. After a
bpf_map_lookup_elemcall, the return value in R0 is typedPTR_TO_MAP_VALUE_OR_NULL. If you checkif (val == NULL) return;, the verifier splits state: on the fall-through path, R0 becomesPTR_TO_MAP_VALUEwith a defined size. On the taken path, execution terminates. Miss that null check, dereference R0 directly, and you get:
R0 invalid mem access 'map_value_or_null'
That message means the verifier still sees R0 as nullable. The fix is always the same: prove to the verifier that the pointer is non-null before the dereference. What changes is where you place that proof. A conditional that checks
val != NULLthree instructions earlier, with abpf_map_update_elemcall in between, does not help — helper calls clobber R1 through R5, and the verifier resets the abstract state for caller-saved registers at every call site.
