Even more formal verification for BPF

BPF offers useful safety guarantees, but Kumar Kartikeya Dwivedi wants BPF programs to be even safer. At the 2026 Linux Storage, Filesystem, Memory-Management, and BPF Summit, he led a session (slides) discussing the possibility of adding domain-specific invariants to BPF programs. It was not a discussion intended to lead to the implementation of any particular kernel feature, but rather an overview of why additional formal verification might be needed, and how it could work with the existing BPF ecosystem.

The BPF verifier ensures that BPF programs cannot violate kernel invariants. They cannot acquire locks in the wrong context, call kernel functions with arguments of the incorrect type, etc. Individual places in the kernel that make use of BPF programs can impose additional requirements. For example, sched_ext has a watchdog that will kick out a BPF program that does not schedule a runnable task within a certain amount of time. All of this is necessary, but not sufficient, Dwivedi said.

Ensuring that the kernel does not crash is only part of ensuring that an entire Linux system remains usable, he said. BPF programs can still interfere with user-space operations in several ways, which impacts the practical safety of BPF programs, even if the kernel itself always remains available.

At Meta, where Dwivedi works, there are one or two cases every month where the sched_ext watchdog kicks out a scheduler. Usually, this is due to a small corner case affecting a specific combination of hardware and workload that the developers simply didn't anticipate. Worse, some cases cause a performance regression without failing outright, which is harder to detect and diagnose. Many scheduling bugs also occur only under low load, which makes them hard to test for before deployment. He shared a slide (number 6) showing the throughput of a server becoming worse under low load with a prospective scheduler change. That particular bug was caught, but only because an engineer noticed it while experimenting.

Another example of the same problem is BPF programs implementing express data path (XDP) load balancing. If one of those programs started dropping network traffic, the server could become remotely inaccessible. That isn't an insurmountable obstacle — a daemon can be set up to listen for a heartbeat and kick the XDP programs out of the kernel if network access is cut off — but it's an additional check that is needed for practical safety.

In both of these cases, there are additional domain-specific constraints that are checked at run time. They are not theoretically impossible to verify statically. Scheduler programs could potentially be proven to never leave a CPU idle with runnable tasks available. XDP programs could potentially be proven to always route every packet to some destination. But those kinds of verification are currently out of reach, and not something that the verifier can simply provide. Also, sometimes developers want to deliberately subvert those guarantees. Dwivedi didn't give a specific example, but concurrency-fuzz-scheduler, which is used to expose concurrency bugs by scheduling tasks badly, comes to mind. Which properties of a BPF program are important to correctness can be context-dependent.

BPF programs control system resources, and so we need to have more confidence in them, even without static analysis, lest bugs have a serious impact, Dwivedi said. One audience member asked whether he was saying that performance properties should be considered part of a program's correctness. Dwivedi agreed that he was: "Sometimes performance-related behavior is as much a safety property as other properties, depending on use." Kernel code is reviewed with rigor; the same amount of care should be taken with BPF code — and with the user-space code that it relies on to make decisions.

This is not something that the BPF subsystem can solve unilaterally, but the design of kernel interfaces can have an impact on how easy it is to model, test, and eventually verify useful properties of BPF programs. Frequently, kernel interfaces are not designed with static analysis in mind, and that is something that the BPF subsystem has to live with, he said. Still, there are improvements that can be made.

He gave bpf_obj_new() as an example of an interface that was a bad idea in hindsight. The motivation behind it was to let BPF programs compose their own data structures, but it implicitly inherited constraints related to handling the lifetime of kernel objects. Those constraints ended up propagating through the program, which made the API difficult to use. Simpler interfaces, that provide less flexible features but therefore require the verifier to perform fewer checks, are easier to work with.

Maybe the correct solution, he proposed, is to use different forms of automated program-verification in different areas. For example, Verus is a tool for automatically proving properties of Rust programs. Perhaps it could be used to handle properties that are critical to the overall function of a BPF program, but not to the safety of the kernel, per se. That is also a benefit to development speed: allowing early exploration before layering on additional safety once a solution has been identified.

To illustrate his point, Dwivedi talked through (without any actual code) how Verus could be used to prove that a scheduler has the property he proposed above: never leaving a CPU idle when a runnable task exists. The proof is based on work by researchers from Inria, the University of Sydney, and other institutions on formally verifiable scheduling. The core idea is to implement a simplified interface that is just powerful enough to accomplish the task in question, while still being amenable to formal verification. The simplified interface only has two queue-manipulation functions: push() and pop().

If one can prove that those two functions maintain the core invariant, and there is no other way to move tasks between queues, then no matter what the main scheduler logic does the invariant will be maintained. For push(), that is done by ensuring that, when asked to push a task onto a CPU's queue, either that CPU was already idle, or no other idle CPU exists. If there is an idle CPU, push() puts the task on its queue instead. The case for pop() is symmetrical. The original proof in the paper is more complicated, because it handles concurrency, but the overall structure of the proof is the same, Dwivedi said.

Alexei Starovoitov asked what it means for Verus to be a static-verification tool that operates on top of Rust. Dwivedi explained that the programmers behind Verus had previously worked on static analysis systems for other languages, but found it difficult, because those languages had many properties that made it hard to do local reasoning about program behavior, such as pointer aliasing. That made sense to Starovoitov, but he still wanted to clarify how Verus would interact with BPF.

The idea is that one would write a simplified Rust wrapper for the interface that a subsystem like sched_ext exposes, Dwivedi explained. That simplified wrapper would be annotated with Verus proofs about its behavior, which can be composed to cover the behavior of the whole program. Verus would check these proofs at compile time, rustc would produce BPF bytecode in the normal way, and then the in-kernel verifier would check the normal safety properties of BPF code. Starovoitov wasn't convinced that operating two separate static analysis pipelines in parallel would be doable, but agreed that he didn't see a problem with what Dwivedi was proposing so far.

Amery Hung asked what kinds of wrappers would be needed; Dwivedi explained that the answer would vary for different subsystems, but that sched_ext schedulers, for example, could likely share similar code. At that point the session ran out of time. It seemed that some BPF developers were unconvinced, but given that additional static verification can be adopted on a project-by-project basis, perhaps we will see more BPF programs analyzed by Verus or similar technologies.