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

现代计算应用程序通过协同使用驻留在计算集群中的数千台服务器来处理大量数据。为了支持这样的应用，网络互连服务器和服务器上的分组处理软件应该是快速的（支持高数据速率和低延迟）、灵活的（实现不同的数据处理应用）和安全的（例如，程序必须运行而不崩溃）。Berkeley Packet Filter（BPF）作为一种机制应运而生，以满足这些目标并加速新型高性能数据包处理应用。BPF目前部署在许多生产系统中。BPF通过在操作系统的上下文中运行用户开发的程序来提高灵活性和性能。为了确保这些应用程序的安全性，本项目将为BPF程序开发可证明正确的静态分析器，保护操作系统免受安全漏洞，拒绝服务攻击和崩溃。该项目将推进静态分析、程序综合和测试网络应用程序（如负载平衡器、包过滤器和性能监控器）的最新技术。这个项目也将教育研究生、本科生和高中生关于正确性推理、网络监控和过滤的基础技术。第一个是开发一个经过验证的Berkeley包过滤器（BPF）静态分析器的基础上，一个抽象的解释，是正确的建设。该项目将解决涉及BPF指令集的形式化和特定于域的沙盒属性建模的关键智力挑战。目前，一个内核BPF静态分析器通过执行范围跟踪、内存安全和信息泄漏自由来检查加载的BPF程序的安全性。然而，这种分析器存在缺陷，导致执行不安全的程序和可利用的漏洞。这个项目的第二个目标是开发一个分析器在C编程语言，可以作为内核的一部分，利用差分分析，程序合成和测试。最终目标是设计一个基于LLVM的经过验证的BPF工具链，通过开发从C到BPF字节码的经过验证的翻译器。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.