FMitF: Track I: Formally Verified Sandboxing for Packet-Processing Programs

Modern computing applications process vast amounts of data by collaboratively employing many thousands of server machines residing in computing clusters. To support such applications, the network interconnecting servers and the packet-processing software on the servers should be fast (supporting high data rates and low delays), flexible (enabling diverse data-processing applications), and safe (e.g., programs must run without crashing). Berkeley Packet Filter (BPF) has emerged as a mechanism to meet these goals and accelerate novel high-performance packet-processing applications. BPF is currently deployed in many production systems. BPF achieves flexibility and performance by running user-developed programs in the context of the operating system. To ensure safety of such applications, this project will develop provably-correct static analyzers for BPF programs, protecting the operating system from security vulnerabilities, denial-of-service attacks, and crashes. This project will advance the state-of-the-art in the static analysis, program synthesis, and testing of networking applications such as load balancers, packet filters, and performance monitors. This project will also educate graduate, undergraduate, and high-school students on foundational techniques for reasoning about correctness, network monitoring, and filtering. This project has three technical goals. The first is to develop a verified Berkeley Packet Filter (BPF) static analyzer based on an abstract interpretation that is correct by construction. The project will address key intellectual challenges involving the formalization of the BPF instruction set and modeling of domain-specific sandboxing properties. Currently, an in-kernel BPF static analyzer checks the safety of loaded BPF programs by performing range-tracking, memory safety, and freedom from information leaks. However, this analyzer has deficiences, resulting in the execution of unsafe programs and exploitable vulnerabilities. The second goal of this project is to develop an analyzer in the C programming language that can be usable as part of the kernel, by leveraging differential analysis, program synthesis, and testing. The final goal is to design a verified BPF toolchain based on LLVM, by developing validated translators from C to BPF bytecode. 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.