Dagstuhl-Seminar 25241
Utilising and Scaling the WebAssembly Semantics
( 09. Jun – 13. Jun, 2025 )
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/25241
Organisatoren
- Amal Ahmed (Northeastern University - Boston, US)
- Andreas Rossberg (München, DE)
- Deian Stefan (University of California - San Diego, US)
- Conrad Watt (Nanyang TU - Singapore, SG)
Kontakt
- Andreas Dolzmann (für wissenschaftliche Fragen)
- Simone Schilke (für administrative Fragen)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Gemeinsame Dokumente
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Programm
- Upload (Use personal credentials as created in DOOR to log in)
WebAssembly (Wasm) is a safe and portable code format used in a broad variety of computational environments, such as Web browsers, cloud, edge, IoT, embedded systems, and blockchains. As a low-level programming language its instruction set is close to that of physical hardware, yet its semantics enforces memory safety, isolation, and the absence of undefined behavior. A distinguishing feature of Wasm is that its official specification contains a complete formal semantics, based directly on techniques developed and established by the scientific community, and proved sound with machine-verified proofs. Its popularity as a technology for both practically building and theoretically investigating verified and secure systems has hence been growing rapidly.
With this Dagstuhl Seminar, we intend to bring together all sides interested in Wasm, its formal semantics, and its application to verification and generation techniques. By including academics and industry representatives involved in Wasm, both as designers, implementers or clients of the technology (e.g., compiler writers), we hope to initiate discussion and new research about evolving the specification, as well as utilizing it for implementing verified systems, programming languages, and new forms of tooling. We intend to place particular focus on the following topics:
Tools for formal specification. Maintaining the current level of rigor in Wasm's specification is an ongoing challenge. While many new features have been proposed for Wasm, the risk is that either the formal specification gets in the way of evolving the language, or that the formalization falls behind.
Verified compilation. We believe that Wasm's formal semantics is an excellent starting point for performing verification in depth for systems built around the language. This applies both to compilation from source languages to Wasm, and compilation from Wasm to native code as it occurs in Wasm engines and their just-in-time compilers.
Software fault isolation. Software fault isolation can be implemented at various granularities and using different techniques, ranging from inline software checks to hardware-based isolation. Such techniques can inform both Wasm's design and its implementations. Wasm can also serve as a vehicle for lightweight isolation, from sandboxing libraries to more ambitious projects, such as a hypervisor or an embedded execution environment.
Language interoperability. In Wasm multi-language interoperation can occur in two ways: first, as the interaction between a language compiled to Wasm and the language in which the host environment operates, and second between multiple different languages compiled to Wasm.
Creative Commons BY 4.0
Amal Ahmed, Andreas Rossberg, Deian Stefan, and Conrad Watt
Please log in to DOOR to see more details.
- Amal Ahmed
- Léo Andrès
- Alexander Bai
- Sandrine Blazy
- Andrew Brown
- Zilin Chen
- Lawrence Chonavel
- Diego Cupello
- Ryan Doenges
- Sébastien Doeraene
- Chris Fallin
- Philippa Gardner
- Tal Garfinkel
- Daniel Hillerström
- Daniel Lehmann
- Sam Lindley
- Thomas Lively
- Brianna Marshall
- Francis McCabe
- Lucy Menon
- Marco Patrignani
- Jean Pichon-Pharabod
- Michael Pradel
- Xiaojia Rao
- Andreas Rossberg
- Claudio Russo
- KC Sivaramakrishnan
- Ralph Squillace
- Yulia Startsev
- Deian Stefan
- Michelle Thalakottur
- Ben L. Titzer
- Thomas Trenner
- Alexa VanHattum
- Marco Vassena
- Jérôme Vouillon
- Andrew Wagner
- Conrad Watt
- Guannan Wei
- Chris Woods
- Dongjun Youn
Verwandte Seminare
- Dagstuhl-Seminar 23101: Foundations of WebAssembly (2023-03-05 - 2023-03-10) (Details)
Klassifikation
- Cryptography and Security
- Logic in Computer Science
- Programming Languages
Schlagworte
- WebAssembly
- formal methods
- software verification
- compilers
- proof assisteants
