https://www.dagstuhl.de/21012

04. – 07. Januar 2021, Dagstuhl-Seminar 21012

Foundations of WebAssembly

Organisatoren

Karthikeyan Bhargavan (INRIA – Paris, FR)
Jonathan Protzenko (Microsoft Research – Redmond, US)
Andreas Rossberg (Dfinity – Zürich, CH)
Deian Stefan (University of California – San Diego, US)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Simone Schilke zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Dokumente

Programm des Dagstuhl-Seminars (Hochladen)

(Zum Einloggen bitte persönliche DOOR-Zugangsdaten verwenden)

Motivation

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.

Motivation text license
  Creative Commons BY 3.0 DE
  Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, and Deian Stefan

Classification

  • Cryptography And Security
  • Logic In Computer Science
  • Programming Languages

Keywords

  • WebAssembly
  • Software Verification
  • Software-fault Isolation
  • Just-in-Time Compilers
  • Formal Methods

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.