CAREER: Principled and practical secure compilation using WebAssembly

如今，构建安全的计算机系统很难：程序员编写的源代码或他们用来生成机器代码的编译器中的一个漏洞就可能使系统暴露在攻击之下。安全编译是从一开始就构建具有端到端安全保证的系统的一种有原则的方法。在编译代码时，安全编译器确保将高级代码的安全属性保留到机器代码级别。不幸的是，安全编译的理论和实践之间的差距是巨大的。特别是，现有的真实工业编译器不是安全的编译器。该项目的目标是通过将工业WebAssembly字节码扩展为统一的、原则性的、实用的安全编译抽象来弥合这一差距。为此，该项目将开发(1)新的技术和原则，作为端到端安全系统的基础，以及(2)允许程序员建立新的安全系统并验证现有系统的安全性的新工具。该项目的结果可能会使数亿用户更加安全：端到端的安全保证可以防止从Web浏览器到下一代云平台的广泛使用的系统中的漏洞利用。该项目还将有助于大学生和高中生的教育，并培训下一代工程师如何构建端到端安全系统。这个项目采取了一种原则性和实用性的方法来构建安全系统，将WebAssembly转变为安全编译中间表示(IR)：高级语言的安全编译器的目标IR，以及安全编译器到机器代码的源IR。将WebAssembly转变为一个安全的汇编IR需要在两个方面解决研究挑战。首先，WebAssembly目前不公开任何抽象概念，用于推理高级安全属性，如内存安全或常量时间。这使得为WebAssembly构建安全的编译器变得困难。其次，WebAssembly的现有编译器没有被证明能够在机器代码级别保留任何安全属性；编译器和微体系结构细节中的错误都可能破坏WebAssembly的安全保证(从而破坏依赖这些保证的系统的安全)。该项目通过以下方式解决这些挑战：(1)将WebAssembly的安全编译器开发到本机平台，(2)使用新的抽象(例如，针对内存安全和常量时间)扩展WebAssembly，使构建到WebAssembly的安全编译器成为可能，以及(3)构建从高级语言到WebAssembly的安全编译器，这些编译器保留了内存安全和常量时间端到端的属性。该项目将在形式推理方面产生新的创新，并在实际安全系统建设方面取得进展。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Building secure computer systems today is hard: a single bug in the source code that programmers write or in the compilers they use to generate machine code could expose systems to attack. Secure compilation is a principled approach to building systems with end-to-end security guarantees from the start. When compiling code, secure compilers ensure that the security properties of high-level code are preserved down to the machine code level. Unfortunately, the gap between the theory of secure compilation and practice is huge. In particular, existing real-world industrial compilers are not secure compilers. The goal of this project is to bridge this gap by extending the industrial WebAssembly bytecode into a unifying principled and practical abstraction for secure compilation. To this end, this project will develop (1) novel techniques and principles which will serve as foundations for end-to-end secure systems and (2) new tools that will allow programmers to build new secure systems and verify the security of existing ones. The results of this project could make hundreds of millions of users safer: end-to-end security guarantees can prevent exploits in widely-used systems, from web browsers to next generation cloud platforms. The project will also contribute to the education of both college and high school students, and train the next generation engineers how to build end-to-end secure systems. This project takes a principled and practical approach to building secure systems by turning WebAssembly into a secure compilations intermediate representation (IR): a target IR for secure compilers from high-level languages and as a source IR for secure compilers to machine code. Turning WebAssembly into a secure compilation IR requires addressing research challenges on two fronts. First, WebAssembly currently does not expose any abstractions for reasoning about high-level security properties, like memory-safety or constant-time. This makes it hard to build secure compilers to WebAssembly. Second, existing compilers of WebAssembly are not proven to preserve any security properties at the machine code level; bugs in compilers and microarchitectural details could both undermine WebAssembly's security guarantees (and thus the security of the systems that rely on these guarantees). This project tackles these challenges by (1) developing secure compilers of WebAssembly to native platforms, (2) extending WebAssembly with new abstractions (e.g., for memory-safety and constant-time) that make it possible to build secure compilers to WebAssembly, and (3) building secure compilers from high-level languages to WebAssembly that preserve properties like memory-safety and constant-time end-to-end. The project will yield both new innovations in formal reasoning and advances in practical secure systems building.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.