TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 21012

Foundations of WebAssembly Cancelled

( Jan 04 – Jan 07, 2021 )

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/21012

Replacement
Dagstuhl Seminar 23101: Foundations of WebAssembly (2023-03-05 - 2023-03-10) (Details)

Organizers

Contact

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.

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

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

Classification
  • Cryptography and Security
  • Logic in Computer Science
  • Programming Languages

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