Congratulations to Profs. Srinivas Narayana and Santosh Nagarakatte, who have received an NSF Formal Methods in the Field Track I grant for their project titled "Formally Verified Sandboxing of Packet-Processing Programs", for an amount of $749,356, covering a four-year period starting from 10/01/2020.
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 servers and the packet-processing software on them should be fast (support high data rates), flexible (enable diverse data-processing applications), and safe (program 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, which protects the operating system from security vulnerabilities, denial-of-service attacks, and crashes. This project will advance the state-of-the-art in static analysis, program synthesis, and testing of networking applications such as load balancers, packet filters, and performance monitors. The project will also educate graduate, undergraduate, and high school students on foundational techniques for reasoning about correctness, network monitoring, and filtering.
The project has three technical goals. The first goal is to develop a verified BPF static analyzer based on abstract interpretation 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 ensures the safety of loaded BPF programs by performing range-tracking, memory safety checks, and checks for information leakage. However, this analyzer's deficiencies have resulted in the execution of unsafe programs with exploitable vulnerabilities. The second goal of this project is to develop an analyzer in the C programming language that can be incorporated into the kernel by leveraging differential analysis, program synthesis, and testing. The third goal is to design a verified BPF tool chain based on LLVM by developing validated translators from C to BPF bytecode.
More details can be found on the National Science Foundation's webpage at https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019302
