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

FMITF：第一轨：经过正式验证的数据包处理程序沙盒

• 批准号: 2019302
• 负责人: Srinivas Narayana
• 金额: $ 74.94万
• 依托单位: Rutgers University New Brunswick
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019302&HistoricalAwards=false
• 关键词: FMitF; Track; Formally; Verified; Sandboxing

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.

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

项目成果

Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers

用三态数进行可靠、精确、快速的抽象解释

• DOI: 10.1109/cgo53902.2022.9741267
• 发表时间: 2022
• 期刊: CGO '22: Proceedings of the 20th IEEE/ACM International Symposium on Code Generation and Optimization
• 作者: Vishwanathan, Harishankar;Shachnai, Matan;Narayana, Srinivas;Nagarakatte, Santosh
• 通讯作者: Nagarakatte, Santosh

Verifying the Verifier: eBPF Range Analysis Verification

验证验证器：eBPF 范围分析验证

• 发表时间: 2023
• 期刊: Computer Aided Verification (CAV
• 作者: Vishwanathan, Harishankar;Shachnai, Matan;Narayana, Srinivas;Nagarakatte, Santosh
• 通讯作者: Nagarakatte, Santosh