CAREER: Principled and practical secure compilation using WebAssembly

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.