WebAssembly is a modern, portable binary format and execution environment with a formal semantics that enforces safety and isolation. Though initially designed to run native, high-performance applications in Web browsers, WebAssembly is now used in many other applications domains kernels – from CDNs, to serverless, to IoT and smart contracts.

WebAssembly is one of the rare cases where practitioners are collaborating with the semantics and programming languages research community. This was exemplified by the initial design of WebAssembly itself, a collaboration with academia that culminated in a PLDI paper. The popularity of WebAssembly has since been growing exponentially as a platform for new application domains, as a target for compilers and languages, and as a subject of active scientific research – from its future semantics, to its performance, and its use in building verified and secure systems.

The goal of this Dagstuhl Seminar is to bring together leading academics and industry representatives currently involved in the design, implementation and formal study of WebAssembly. By materializing a loose community of academics with related interests, we hope to set new directions for WebAssembly research, while creating a forum to exchange ideas and increase visibility of this nascent field. By bringing in industry experts, we hope to strengthen engagement with academia and renew a fruitful engagement, ensuring the input from formalists keeps informing the ongoing evolutions of Wasm.

We propose to bring the WebAssembly and Formal Methods communities together by focusing this Dagstuhl Seminar around three topics:

Formal methods for WebAssembly will revolve around formalizing, reasoning and proving properties about WebAssembly itself. While the seminal work of Watt is immensely useful, there are many WebAssembly extensions under consideration (e.g., threading, bulk memory operations, and vector instructions) which can benefit from formal semantics. Wasm is not a standalone language though; we need to develop formal methods to reason about its interaction with the operating system, the execution of JITed WebAssembly code, etc. Finally, we need logics that will allow us to formally capture interesting properties beyond what current work handles.

Verified Compilation to WebAssembly will focus on WebAssembly as a target of verified compilation toolchains. We hope to position WebAssembly as a viable candidate for verified and secure compilation, while establishing that the clean design of WebAssembly offers greater simplicity when it comes to verifying a compilation toolchain. We hope that the structure of WebAssembly yields simpler, shorter proofs of compiler correctness.

Verified Compilation of WebAssembly will study the compilation of WebAssembly to native code, i.e., how to securely and correctly compile WebAssembly code to machine code. Since Wasm is growing rapidly, these efforts must not only focus on Wasm as used on the Web, but also embedded systems, edge computing, IoT, and even OS kernels – and on a variety of processors and toolchains.

By bringing together academics and language and compiler designers, we hope to identify grand challenges for formal verification that can be enabled by WebAssembly. At the same time, we hope that bringing academics and industry members together will also identify research problems for the still-evolving bytecode that that industry has not yet solved.

Creative Commons BY 3.0 DE

Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, and Deian Stefan