WebAssembly is a modern sandboxing technology that has both well-specified formal semantics – interesting to verification researchers – and a blossoming ecosystem of industrial virtual-machine implementations (host-side) and language runtimes and compilers (guest-side). The formal semantics provide significant value today, especially as an oracle for testing, but are far from a panacea if one’s goal is full correctness of the stack, from Wasm-guest source language to machine code with sandboxing and full correctness guarantees.

In this talk, I will discuss several of my efforts across the stack consisting of a JavaScript guest runtime, the Wasmtime virtual machine, and the Cranelift JIT compiler to improve correctness. I’ll discuss an approach to generate compiled Wasm bytecode automatically from an interpreter, removing a common source of bugs in language runtimes, and outline a path toward semantics-preserving optimizations. I’ll discuss efforts to verify stages of the Cranelift compiler, so Wasm bytecode is faithfully translated to correct machine code. And I’ll present some work-in progress results on translation validation via proof-carrying code to provide a true guarantee of sandbox isolation in Wasmtime, discussing both what works and what remains an unsolved challenge. In all three areas my focus is on pragmatic, incremental progress in a real-world software stack, with tools and technologies that are usable in production.

Chris Fallin is a senior architect at F5, where he works on WebAssembly-related compiler tooling, continuing work he has done at Fastly and Mozilla on SpiderMonkey, the Cranelift JIT compiler (tech lead for three years), and the Wasmtime virtual machine. Prior to those positions, he has worked at Google and Intel. He completed his PhD in compilers at Carnegie Mellon University.