[$] Even more formal verification for BPF

BPF provides 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 discussed adding domain-specific invariants to BPF programs during a session (slides). The BPF verifier ensures BPF programs cannot violate kernel invariants, such as acquiring locks in the wrong context or calling kernel functions with incorrect types.

Individual kernel uses of BPF programs can impose additional requirements, like a watchdog in sched_ext that will terminate a BPF program if it fails to schedule a runnable task within a certain time. However, BPF programs can still interfere with user-space operations, impacting practical safety even if the kernel remains available.

Meta has experienced issues with the sched_ext watchdog kicking out the scheduler due to specific hardware and workload combinations. Some bugs only appear under low load, making them hard to test before deployment. Dwivedi shared examples of performance regressions caused by scheduler changes, which were only caught after engineers noticed them while experimenting.

Another example is BPF programs implementing express data path (XDP) load balancing, where a dropped network traffic could render a server remotely inaccessible. While these cases have workarounds, additional checks are needed for practical safety. Some domain-specific constraints can be checked at runtime, but verifying them statically is currently unattainable.

Dwivedi suggested that developers sometimes deliberately subvert these guarantees, and that performance properties can sometimes be considered part of a program's correctness. Kernel code is rigorously reviewed, and similar care should be taken with BPF code and user-space code that relies on it. The BPF subsystem cannot solve this unilaterally, but the design of kernel interfaces can impact how easy it is to model, test, and verify BPF programs' properties.

Dwivedi proposed using different forms of automated program verification in different areas. For instance, Verus, a tool for proving properties of Rust programs, could be used to handle critical BPF program properties while allowing early exploration before adding additional safety measures.