Speaker
Description
Abstract
eBPF provides a safe way to extend the kernel functionality. To ensure safety, the kernel verifies the memory safety and termination of eBPF programs and is thus the security boundary for eBPF. It must accept untrusted programs from userspace and determine, under strict time and memory limits, whether they are safe to execute.
Today, the verifier symbolically executes program paths, tracks abstract register and memory states, and uses state pruning and repeated loop exploration to establish safety. Keeping both proof discovery and proof checking in the kernel has the important advantage that the kernel does not need to trust the compiler or any userspace component.
The cost of this design is that the kernel has to employ a sophisticated analysis capable of reconstructing invariants from eBPF bytecode. Compilers may already discover source-level relationships and loop invariants, but these facts are not normally conveyed to the kernel. When the verifier cannot recover invariants, it must conservatively reject the program. At the same time, the complexity of the analysis makes it difficult to audit and maintain this security boundary, and verifier bugs can result in malicious programs being accepted. Verification failures can also be difficult to predict and relate back to the source program.
We are exploring a proof-carrying verification architecture that separates proof generation from proof checking. An untrusted userspace proof generator analyzes the program, discovers invariants, and uses an SMT solver to discharge safety obligations. If successful, it emits a certificate containing the invariants and proof steps needed to validate the program. If an obligation cannot be proved, the tool can use compiler metadata and solver output to distinguish concrete counterexamples from unsupported reasoning or missing invariants, and produce source-oriented diagnostics.
Inside the kernel, a domain-specific checker validates the program and certificate together. The certificate supplies facts such as basic-block and loop invariants, pointer bounds, and relationships between program values. The checker does not search for invariants or invoke an SMT solver. It validates each claimed state transition and entailment using a restricted set of eBPF-specific reasoning rules.
For example, a loop certificate may provide an invariant relating an induction variable, a packet pointer, and data_end. The checker verifies that the invariant holds on entry, is preserved across the back edge, and is strong enough to justify each memory access. It does not need to infer the invariant or repeatedly explore the loop.
We have built a preliminary end-to-end prototype that generates and checks certificates for a subset of eBPF programs, including examples with control flow, loops, scalar relationships, and memory-safety obligations. Our early experiments indicate that certificate checking can perform particularly well on larger programs for which abstract interpretation requires extensive path exploration, state merging, or repeated loop analysis. In these cases, the checker benefits from being given the required invariants directly and can avoid much of the search performed by the existing verifier. These results are still preliminary and currently apply only to the supported subset. At LPC, we will present the supported feature set, representative examples, and an initial comparison of verification behavior and runtime, together with the cases where the approach does not yet apply.
A central design problem is defining the safety policy shared by the proof generator and checker. This policy must cover instructions, helper calls, kfuncs, program contexts, pointer accesses, and kernel-managed resources, while evolving with eBPF and its kernel interfaces. Its format, maintenance model, and relationship to existing verifier semantics are part of the research question.
The talk will present the architecture, certificate language, prototype, and initial results. We will also discuss certificate size, malformed or adversarial certificates, unsupported features, policy evolution, verifier transformations, and the relationship between checked bytecode and JIT semantics.
We seek feedback from the eBPF community on whether this is a useful and technically plausible way to structure safety checking, which parts of current verifier semantics are hardest to express as explicit proof obligations, and whether a maintainable shared safety policy is possible.
Relation to Prior Work
Proof-carrying verification for eBPF was previously explored by Exoverifier, which separates proof generation from proof checking and emits general proof objects based on a Lean formalization of eBPF semantics. More recently, VEP proposed an annotation-guided toolchain with userspace verification, a specialized compiler, and a lightweight bytecode-level proof checker. BCF takes a hybrid approach: it retains the kernel verifier’s abstract interpretation, while using machine-checkable proofs generated in userspace to guide abstraction refinement and improve precision.
Our work explores another point in this design space. Rather than relying on general theorem-prover objects, source annotations, or refinement of the existing verifier analysis, we are designing a restricted certificate language around eBPF-specific invariants and state transitions. The checker accepts only a fixed set of reasoning steps, with explicit limits on certificate structure and checking work. Our preliminary prototype suggests that this model is sufficient for a useful subset of programs while remaining closely aligned with current eBPF concepts. The talk will compare these approaches and discuss which parts of eBPF verification fit restricted certificate checking and which may require richer reasoning.