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通过在操作系统的特征上运行用户开发程序来实现flexflexible和性能。为了确保此类应用程序的安全性，该项目将为BPF程序提供可证明的静态分析仪，保护操作系统免受安全漏洞，拒绝服务的危害和崩溃。该项目将推动最先进的静态分析，程序综合和网络应用程序测试，例如负载平衡器，数据包过滤器和PerformanCemonItors。该项目还将教育毕业生，本科，安哥学校的学生，以了解有关纠正，网络监控和过滤的基础技术。该项目具有三个技术目标。首先是基于通过构造依次正确的抽象解释来开发平均伯克利数据包滤波器（BPF）静态分析仪。该项目将解决涉及BPF指令集和域特异性沙盒属性的正式化的关键知识核能。目前，Anin-Kernel BPF静态分析仪检查了负载的BPF程序的安全性，通过执行范围跟踪，内存安全性和自由泄漏。但是，该分析仪具有缺陷，导致了不安全计划和可剥削漏洞的执行。该项目的第三目标是开发一个可以作为内核的一部分使用的CPROGROGING语言的分析仪，逐步差异分析，程序合成和测试。最终目标是设计一个基于LLVM的经过验证的BPF工具链，拜会从C到BPF Bytecode的经过验证的经过验证的翻译人员。该奖项反映了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