FMitF: Track II: Formally-Verified eBPF Verifier in the Linux Kernel

The extended Berkeley Packet Filter (eBPF) adds dynamism to the Linux operating system kernel by allowing user-space programs to be executed in the kernel upon specific events. Such dynamism enables the development of novel applications for networking, system security, and performance profiling. eBPF-based applications have seen widespread practical deployment in the industry. To ensure the safety and security of executing user-developed programs in the operating system context, the Linux kernel implements algorithms for static program analysis through abstract interpretation, encapsulated into an in-kernel component called the eBPF verifier. Given that Linux is a widely used operating system, a bug in the eBPF verifier can compromise the safety and security of all devices using it. This project's novelty is in the design of new automated techniques to prove the correctness of the abstract interpretation algorithms in the eBPF verifier. This project's key impact is the development of a provably sound eBPF verifier, with the potential to make widely deployed eBPF software and the Linux kernel much more secure and reliable. This project will educate and train graduate and undergraduate students on formal methods and networking, through the development of curricular materials and research projects.This project advances formal verification of low-level systems and networking software by (i) developing and enhancing a software pipeline to automatically check the soundness of abstract interpretation operators in the Linux kernel directly from C source code; (ii) introducing techniques to modularize and parallelize verification tasks to improve the feasibility of verifying every kernel commit; (iii) producing high-quality bug reports through differential synthesis of programs that demonstrate mismatches between concrete execution and abstract interpretation; and (iv) pursuing collaborations with Linux kernel developers to increase the likelihood of deploying formal checking in the Linux kernel’s continuous integration (CI) infrastructure.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.