Proof-Carrying-BPF Programs Aim to Expand eBPF Verifier Acceptance

A paper accepted to SOSP '26 introduces proof-carrying-BPF programs, a technique designed to let the Linux kernel's eBPF verifier accept a larger class of programs without growing more complex. The approach pairs a userspace copy of the kernel verifier with the BPF compiler backend: when the in-kernel verifier can't prove a program's safety on its own, the backend uses symbolic evaluation to generate a formal proof. The kernel then checks that proof with a lightweight in-kernel checker and accepts the program only if the proof is valid.

This tight coupling between the userspace verifier and the compiler backend is meant to fix shortcomings of the earlier BCF framework, notably the latency caused by repeated kernel-to-userspace round trips and the verifier sitting idle during userspace-side checks. In evaluation, the authors' prototype successfully verified all 360 objects in the BCF benchmark suite — drawn from Calico and Cilium datapaths, BCC, and Inspektor Gadget — that the standard kernel verifier had previously rejected.

For engineers building eBPF-based networking, observability, or security tooling, this work points toward fewer verifier rejections for legitimate complex programs, achieved without adding risk or bloat to the in-kernel verifier itself.