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

点击翻译按钮获取中文摘要

Modern computing applications process vast amounts of data bycollaboratively employing many thousands of server machines residingin computing clusters. To support such applications, the networkinterconnecting servers and the packet-processing software on theservers 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 acceleratenovel high-performance packet-processing applications. BPF iscurrently deployed in many production systems. BPF achievesflexibility and performance by running user-developed programs in thecontext of the operating system. To ensure safety of such applications, this project willdevelop provably-correct static analyzers for BPF programs, protectingthe operating system from security vulnerabilities, denial-of-serviceattacks, and crashes. This project will advance the state-of-the-artin the static analysis, program synthesis, and testing of networkingapplications such as load balancers, packet filters, and performancemonitors. This project will also educate graduate, undergraduate, andhigh-school students on foundational techniques for reasoning aboutcorrectness, network monitoring, and filtering.This project has three technical goals. The first is to develop averified Berkeley Packet Filter (BPF) static analyzer based on an abstract interpretation that iscorrect by construction. The project will address key intellectualchallenges involving the formalization of the BPF instruction set andmodeling of domain-specific sandboxing properties. Currently, anin-kernel BPF static analyzer checks the safety of loaded BPF programsby performing range-tracking, memory safety, and freedom frominformation leaks. However, this analyzer has deficiences, resulting in theexecution of unsafe programs and exploitable vulnerabilities. Thesecond goal of this project is to develop an analyzer in the Cprogramming language that can be usable as part of the kernel, byleveraging differential analysis, program synthesis, and testing. Thefinal goal is to design a verified BPF toolchain based on LLVM, bydeveloping 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.