Even more formal verification for BPF [LWN.net]
LWN<br>.net<br>News from the source
Content Weekly Edition<br>Archives<br>Search<br>Kernel<br>Security<br>Events calendar<br>Unread comments
LWN FAQ<br>Write for us
Edition Return to the Front page
User:<br>Password: |
Log in /<br>Subscribe /<br>Register
Even more formal verification for BPF
Please consider subscribing to LWN
Subscriptions are the lifeblood of LWN.net. If you appreciate this<br>content and would like to see more of it, your subscription will<br>help to ensure that LWN continues to thrive. Please visit<br>this page to join up and keep LWN on<br>the net.
By Daroc Alden<br>August 10, 2026
LSFMM+BPF
BPF offers useful safety guarantees, but Kumar Kartikeya Dwivedi wants BPF<br>programs to be even safer. At the 2026
Linux Storage, Filesystem,<br>Memory-Management, and BPF Summit, he led a session<br>(slides)<br>discussing the possibility<br>of adding domain-specific invariants to BPF programs. It was not a discussion<br>intended to lead to the implementation of any particular kernel feature, but<br>rather an overview of why additional formal verification might be needed, and<br>how it could work with the existing BPF ecosystem.
The BPF verifier ensures that BPF programs cannot violate kernel invariants.<br>They cannot acquire locks in the wrong context, call kernel functions with<br>arguments of the incorrect type, etc. Individual places in the kernel that make<br>use of BPF programs can impose additional requirements. For example,
sched_ext<br>has a watchdog that will kick out a BPF program that does not schedule a<br>runnable task within a certain amount of time. All of this is necessary, but not<br>sufficient, Dwivedi said.
Ensuring that the kernel does not crash is only part of ensuring that an entire<br>Linux system remains usable, he said. BPF programs can still interfere with<br>user-space operations in several ways, which impacts the practical safety of BPF<br>programs, even if the kernel itself always remains available.
At Meta, where Dwivedi works, there are one or two cases every month where the<br>sched_ext watchdog kicks out a scheduler. Usually, this is due to a small corner<br>case affecting a specific combination of hardware and workload that the<br>developers simply didn't anticipate. Worse, some cases cause a performance<br>regression without failing outright, which is harder to detect and<br>diagnose. Many scheduling bugs also occur only under low load, which makes them<br>hard to test for before deployment. He shared a slide (number 6) showing the throughput of<br>a server becoming worse under low load with a prospective scheduler change. That<br>particular bug was caught, but only because an engineer noticed it while<br>experimenting.
Another example of the same problem is BPF programs implementing
express data path (XDP) load balancing. If one<br>of those programs started dropping network traffic, the server could become<br>remotely inaccessible. That isn't an insurmountable obstacle — a daemon can be<br>set up to listen for a heartbeat and kick the XDP programs out of the kernel if<br>network access is cut off — but it's an additional check that is needed for<br>practical safety.
In both of these cases, there are additional domain-specific constraints that<br>are checked at run time. They are not theoretically impossible to verify<br>statically. Scheduler programs could potentially be proven to never leave a CPU<br>idle with runnable tasks available. XDP programs could potentially be proven to<br>always route every packet to some destination. But those kinds of verification<br>are currently out of reach, and not something that the verifier can simply<br>provide. Also, sometimes developers want to deliberately subvert those<br>guarantees. Dwivedi didn't give a specific example, but<br>concurrency-fuzz-scheduler, which is used to<br>expose concurrency bugs by scheduling tasks badly, comes to mind. Which<br>properties of a BPF program are important to correctness can be<br>context-dependent.
BPF programs control system resources, and so we need<br>to have more confidence in them, even without static analysis,<br>lest bugs have a serious impact, Dwivedi said. One audience member asked whether<br>he was saying that performance properties should be considered part of a<br>program's correctness. Dwivedi agreed that he was: "Sometimes<br>performance-related behavior is as much a safety property as other properties, depending<br>on use."<br>Kernel code is reviewed with rigor; the same amount of care should be taken<br>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<br>design of kernel interfaces can have an impact on how easy it is to model, test,<br>and eventually verify useful properties of BPF programs. Frequently, kernel<br>interfaces are not designed with static analysis in mind, and that is something<br>that the BPF subsystem has to live with, he said. Still, there are improvements<br>that can be made.
He gave<br>bpf_obj_new()<br>as an example of an interface that was a bad idea in hindsight. The motivation...