What eBPF Spinlock Bugs Reveal About the Limits of Kernel Static Analysis

The eBPF verifier is the piece of infrastructure that makes eBPF safe. Load a program, and the kernel runs it through a static analysis pass that checks every execution path for memory safety, type correctness, and resource management violations. Only programs that pass this gauntlet run in kernel space. Rohan Varma’s recent article documents fixing spinlock-related bugs in that verifier, and the bugs split into two distinct classes that reveal different things about where static analysis runs into structural limits.

The Verifier Is an Abstract Interpreter

Before getting into spinlocks specifically, it helps to understand what the BPF verifier actually is. It implements abstract interpretation: a technique for analyzing programs by simulating their execution over an abstract domain rather than concrete values. Instead of tracking that a register holds the integer 42, the verifier tracks that it holds a scalar in the range [0, 255], or a pointer to a map value of type X, or the return value of a helper with specific null-check requirements.

The analysis is sound in theory, meaning if the verifier accepts a program, the program is safe under the abstract semantics the verifier uses. But “the abstract semantics the verifier uses” is doing a lot of work in that sentence. The verifier’s safety guarantees are exactly as strong as the model it builds of program state. When that model is incomplete, programs that pass verification can still be unsafe.

What the Verifier Must Track for Spinlocks

bpf_spin_lock was introduced in Linux 5.1 in 2019. The API requires a struct bpf_spin_lock embedded in a BPF map value; programs call bpf_spin_lock() and bpf_spin_unlock() on it:

struct value {
    struct bpf_spin_lock lock;
    int counter;
};

SEC("xdp")
int my_prog(struct xdp_md *ctx)
{
    struct value *v = bpf_map_lookup_elem(&my_map, &key);
    if (!v)
        return XDP_DROP;
    bpf_spin_lock(&v->lock);
    v->counter++;
    bpf_spin_unlock(&v->lock);
    return XDP_PASS;
}

On standard (non-RT) kernels, bpf_spin_lock() is implemented via __bpf_spin_lock_irqsave, which disables local IRQs on the acquiring CPU. Safety comes from IRQ-disable rather than full SMP mutual exclusion: nothing else on that CPU can run while the lock is held.

The verifier must enforce three invariants: a lock cannot be acquired twice without a release, a lock cannot be released without being held, and no lock can be held when the program exits. These are properties that must hold on every possible execution path through the program.

To enforce them, the verifier tracks lock state in bpf_func_state through active_spin_lock, set to the register ID of the lock pointer on bpf_spin_lock() and cleared on bpf_spin_unlock(). A nonzero value at program exit causes rejection. This is implemented in process_spin_lock() in kernel/bpf/verifier.c.

State Pruning and the Gap

Verifying every execution path through a BPF program naively is exponential in the number of branches. The verifier’s primary tool against this is state pruning: when it reaches an instruction it has analyzed before, it checks whether the current abstract state is “more constrained” than a previously cached state at that point. If so, it prunes, concluding that if the cached (less constrained) state was safe, the current (more constrained) state must be too.

The check is implemented in states_equal() and func_state_equal(). Two states are equivalent when register types, value ranges, pointer provenance, and stack contents all match within the partial order the verifier defines. Pruning makes the verifier tractable for production programs; without it, tools like Cilium and Falco would routinely hit verifier complexity limits.

The spinlock bug arises at the intersection of state pruning and lock tracking. Suppose two execution paths reach the same instruction: one with active_spin_lock = 0 (no lock held), one with active_spin_lock nonzero (lock held). The verifier first explores the no-lock path, caches it as verified, then reaches the same instruction via the lock-held path. If states_equal() does not include active_spin_lock in its comparison, it considers the two states equivalent and prunes the lock-held path.

The pruned path carries an obligation, releasing the lock before program exit, that never gets verified. The program passes. At runtime, a carefully constructed execution hits exactly that path and exits with a spinlock held. Local IRQs remain disabled. The CPU stops responding to interrupts until the kernel detects the condition and crashes, or until reboot.

The fix is narrow in code but wide in implications: func_state_equal() must compare active_spin_lock fields so that states differing in lock-held status are never treated as equivalent. The cost is more paths to verify for programs with complex branching near lock boundaries, which means longer verification times and programs closer to hitting the verifier’s instruction limit.

PREEMPT_RT: The Class of Bug Static Analysis Cannot Fix

The second class of spinlock issues is structurally different. On CONFIG_PREEMPT_RT kernels, BPF spinlocks are not implemented with IRQ-disable. They become sleeping locks backed by rtmutex. A BPF program holding a “spinlock” can be preempted.

This breaks the safety model the verifier assumes. If a BPF program acquires a lock and then gets preempted, and another BPF program on the same CPU tries to acquire the same lock, the result is a potential deadlock. The verifier cannot catch this because it has no model of the runtime scheduler. The spinlock API looks identical from the verifier’s perspective regardless of kernel configuration, but the runtime semantics differ in a way that invalidates the verifier’s proofs.

The ongoing BPF + PREEMPT_RT integration effort, discussed in BPF mailing list threads since 2021, addresses this by reworking the underlying lock primitive on RT to use something that preserves non-preemptibility without relying on IRQ-disable. The fix has to happen at the runtime level; the verifier cannot be patched to detect this class of problem because it does not have the information required.

The Recurring Structural Pattern

These two bug classes are each specific to spinlocks, but the underlying patterns repeat with each stateful feature added to BPF. Jakub Kicinski’s referenced objects work in 2018 introduced tracking for open handle-like objects. BPF timers in Linux 5.15 added timer ownership tracking. Typed kernel pointers (kptrs) in 5.19 added typed reference tracking with explicit acquire and release obligations. BPF iterators in 6.4 added open and close state tracking.

Each follows the same arc: implement the runtime primitive, add state tracking to bpf_func_state, update states_equal(), ship, discover a subtle case where the comparison is incomplete, fix it, add a regression test to tools/testing/selftests/bpf/. The regression test encodes the specific program structure that would have triggered the bug, making the coverage concrete and machine-verifiable.

The PREEMPT_RT class has a parallel pattern: each new BPF feature that relies on kernel configuration-dependent runtime behavior has to be audited for correctness across both RT and non-RT kernels. The verifier is not the right tool for catching this; kernel configuration-specific adapter layers are.

What This Means for Trust

The BPF verifier is often described as providing formal safety guarantees. The more precise framing is that it provides strong, systematically enforced safety checks implemented in maintained code, which is not the same thing as a mechanically verified proof. The verifier can have bugs, and it does; spinlocks are not the only example.

This does not make eBPF unsafe in practice. The requirement for CAP_BPF or CAP_SYS_ADMIN to load most BPF program types limits who can trigger verifier bugs, and the kernel security team treats verifier correctness issues seriously. The tools built on eBPF work reliably. But the trust model is “the verifier is correct code we maintain carefully,” and understanding that distinction matters when reasoning about what the safety guarantee actually covers.

The spinlock work in Varma’s article is a clear example of the kernel community doing this well. The bugs are subtle, the analysis is careful, the fixes are minimal, and each fix comes with a test that would have caught the bug. The verifier after the fix is more correct than before. That trajectory, incremental, empirical, test-driven, is how a system this complex improves.