Wasm has the potential to completely change how we build secure systems. Next generation systems using Wasm as an intermediate representation can have unprecedented guarantees rooted in formal methods. (Some already do.) For this to be meaningful in practice, though, we need to actually deliver on Wasm’s semantics—and this means removing the (huge) compiler and the (even bigger) runtime from the trusted computing base (TCB), while delivering on real world scaling and performance needs.

In this talk I will describe our efforts to reduce Wasm’s TCB—and in particular our work on the WaVe verified runtime—and our efforts to improve Wasm’s scalability, performance, and security with simple hardware extensions.