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）使用新的抽象（例如，（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.