SaTC: CORE: Medium: Secure and Formally-verified Low-level Languages

我们的现代计算基础设施，包括互联网和在我们的手机和数据中心运行的大量应用程序，依赖于许多低级软件系统才能正常运行。低级软件包括操作系统和编程语言编译器等工具，软件开发人员使用这些工具来构建这些应用程序。低级软件的设计缺陷或实施中的错误可能会导致系统崩溃、安全漏洞或不正确的结果，这可能会给个人、企业以及科学或教育机构带来非常高昂的代价。作为该项目的一部分进行的研究将调查如何提高低级软件的安全性和可靠性。该研究集中于现代软件基础设施的特定部分(称为LLVMIR，工业级别的编译器基础设施，在工业界和学术界广泛使用)，并开发其行为的正式的、计算机可检查的数学模型。该模型将被用来发现基础设施中的缺陷，并作为使用它的正确系统的辅助。由于这样的系统无处不在，提高它们的安全性和可靠性可能会对整个社会产生重大的积极影响。该项目还将开发适合于向使用该基础设施的软件开发人员教授基本理论和技术的教育资源。该项目将建立并扩展Vellvm的能力--“经过验证的LLVM IR”--在Coq交互定理证明器中实现的LLVM编译器基础设施的形式化。因为LLVM生态系统支持许多源语言(C、C++、Rust、Haskell等)和目标平台(包括几乎所有的现代处理器)，所以它是扩大正式建模和验证工作的影响的自然支点。这里进行的研究将有三个主要方面：(1)通过扩展支持的LLVM IR构造套件、开发新的内存模型和支持优化先前不可用的并发语义来提高Vellvm相对于LLVM IR的保真度和完整性；(2)设计促进LLVM IR程序的关系推理的抽象。这些抽象将采取领域特定逻辑的集合的形式，用于在不同抽象级别上对LLVMIR代码进行推理；(3)应用Vellvm框架来构建工具，帮助识别未定义的行为并减轻LLVMIR程序中的安全漏洞。为了实现这些目标，拟议的研究将开发适用于低级别程序语义的新的推理和证明自动化技术。所有的发展都将使用CoQ交互定理证明器进行实施和验证，对结果产生高度的信心。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Our modern computing infrastructure, including the Internet and multitude of applications that run on our phones and in data centers, relies on many low-level software systems to function correctly. Low-level software includes things like operating systems and the tools, such as programming language compilers, that are used by software developers to build those applications. Flaws in the design of low-level software, or bugs in its implementation, can lead to system crashes, security vulnerabilities, or incorrect results that can be very costly to individuals, businesses, and scientific or educational institutions. The research conducted as part of this project will investigate how to improve the security and reliability of low-level software. The research focuses on a specific piece of the modern software infrastructure (something called LLVM IR, an industrial-strength bit of compiler infrastructure that is widely used in industry and academia), and develop a formal, computer-checkable, mathematical model of its behaviors. That model will be used to uncover flaws in the infrastructure, and as an aid to implementing correct systems using it. Because such systems are ubiquitous, improving their security and reliability can potentially have significant positive impact for society as a whole. This project will also develop educational resources suitable for teaching the underlying theory and techniques to software developers who use this infrastructure.The project will build on and extend the capabilities of Vellvm--the "Verified LLVM IR"--a formalization of the LLVM compiler infrastructure implemented in the Coq interactive theorem prover. Because the LLVM ecosystem supports many source languages (C, C++, Rust, Haskell, among others) and target platforms (including almost all modern processors), it is a natural fulcrum to amplify the impact of formal modeling and verification efforts. The research conducted here will have three main thrusts: (1) Improving Vellvm's fidelity and completeness with respect to the LLVM IR by extending the suite of supported LLVM IR constructs, developing a new memory model, and concurrency semantics that enable optimizations unavailable previousl; (2) Designing abstractions that facilitate relational reasoning about LLVM IR programs. These abstractions will take the form of a collection of domain-specific logics for reasoning about LLVM IR code at various levels of abstraction; (3) applying the Vellvm framework to build tools that help identify undefined behaviors and mitigate security vulnerabilities in LLVM IR programs. To achieve these goals, the proposed research will develop novel reasoning and proof automation techniques that are applicable to low-level program semantics. All of the developments will be implemented and verified using the Coq interactive theorem prover, yielding a high-degree of confidence in the results.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.