TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 23101

Foundations of WebAssembly

( 05. Mar – 10. Mar, 2023 )

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/23101

Organisatoren

Kontakt

Dagstuhl Seminar Wiki

Gemeinsame Dokumente

Programm
  • Upload (Use personal credentials as created in DOOR to log in)

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 – from CDNs to serverless, IoT, library sandboxing, 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 growing 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 (e.g., bulk memory operations and vector instructions) which can benefit from formal semantics. Since Wasm is not a standalone language, we also 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 – in particular, simpler and shorter proofs of compiler correctness and security.

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 will focus on Wasm as used on the Web and beyond (e.g., embedded systems, edge computing, IoT, and even OS kernels), and across different platforms 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

Teilnehmer

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

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