WebAssembly is a general-purpose low-level virtual machine. It was the first programming language to be introduced to the Web since JavaScript, and has since been adopted in many other environments, such as edge and cloud computing, mobile computing, blockchains, and embedded systems. Unusually for an industrial language, WebAssembly’s normative specification is stated fully in terms of a pen-and-paper formal semantics. In addition, multiple mechanisations of this semantics have been created and used to prove the soundness of the WebAssembly type system.

The rigor of WebAssembly’s semantics presents new opportunities for researchers in Programming Languages to apply their craft to a widely-used industry technology. This WebAssembly Workshop (WAW) intends to create a space where new ideas for such research can be brainstormed, and where ongoing research work related to WebAssembly can be discussed, critiqued, and iterated on. We also hope to familiarize researchers with the successes and challenges of WebAssembly’s design and specification from an industrial point of view, thereby empowering them to influence the future direction of the language.

Supporters

Talks

Participants

This workshop will be centered around a small number of invited talks on some key themes of WebAssembly research and practice, interspersed by broader discussions among the attendees. We also aim to make time for informal lightning talks from any interested attendees. A report summarising the discussions will be prepared and publicly distributed by the organisers shortly after the end of the workshop.

Lightning talks

If you are interested in giving a lightning talk about some piece of WebAssembly-related work, please fill out this Google form.

Lightning talks should be up to 3 minutes long. Note that we can currently only support lightning talks from in-person attendees, and we will do our best to fit in as many speakers as possible.

Luke Wagner

Luke Wagner is an engineer working in the Office of the CTO at Fastly and a co-chair of the W3C WebAssembly Working Group. Before joining Fastly, Luke worked for a decade at Mozilla, where he participated in starting, designing and implementing WebAssembly in Firefox.

What is a WebAssembly component (and why?)

The Component Model is a new proposal being worked on within the W3C WebAssembly Community Group that defines a standard, portable, lightweight, finely-sandboxed, cross-language, compositional module which is layered on top of the existing Core WebAssembly specification and serves as the foundation for other proposed non-browser system interfaces (WASI). This talk will present several high-level motivating use cases for the Component Model, give an overview of the technical design, and describe the current “Preview 2” and upcoming “Preview 3” releases.

Ben L. Titzer

Ben L. Titzer is a Principal Researcher at Carnegie Mellon University. A former member of the V8 team at Google, he co-founded the WebAssembly project, led the team that built the implementation in V8, and led the initial design of V8’s TurboFan optimizing compiler. Prior to that he was a researcher at Sun Labs and contributed to the Maxine Java-in-Java VM. Currently, he is working on a new Wasm research engine and several WebAssembly-related research projects. He is the designer and main implementer of the Virgil programming language.

WALI: A thin Linux kernel interface for WebAssembly

WebAssembly is gaining popularity as a portable binary format targetable from many programming languages. With a well-specified low-level virtual instruction set, minimal memory footprint and many high-performance implementations, it has been successfully adopted for lightweight in-process memory sandboxing in many contexts. Despite these advantages, WebAssembly lacks many standard system interfaces, making it difficult to reuse existing applications.

This talk introduces WALI: The WebAssembly Linux Interface, a thin layer over Linux’s userspace system calls, creating a new class of virtualization where WebAssembly seamlessly interacts with native processes and the underlying operating system. By virtualizing the lowest level of userspace, WALI offers application portability with little effort and reuses existing compiler backends. With WebAssembly’s control flow integrity guarantees, these modules gain an additional level of protection against remote code injection attacks. Furthermore, capability-based APIs like WASI can themselves be virtualized and implemented in terms of WALI, improving reuse and robustness through better layering. We present an implementation of WALI in a modern WebAssembly engine and evaluate its performance on a number of applications which we can now compile with mostly trivial effort.

Amal Ahmed

Amal Ahmed is a Professor at the Khoury College of Computer Sciences at Northeastern University. She received her PhD from Princeton University, where she developed the first step-indexed model of higher-order mutable state, showing how to scale the logical-relations technique to realistic languages. The technique is now widely used for semantic type soundness for numerous languages, verification of shared-memory concurrency, and as a foundation for the Iris program logic. Her interests include type systems and semantics, compiler verification, language interoperability, gradual typing, and compilation of dependent types, with a recent focus on correct and secure compilers that support safe inter-language linking. She served as Program Chair for OOPSLA’22 and POPL’23 and has been a frequent lecturer at the Oregon PL Summer School (OPLSS).

RichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssembly

Safe, shared-memory interoperability between languages with different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result in memory-safety violations. In this talk, I’ll present RichWasm, a higher-level version of WebAssembly with an enriched capability-based type system to support fine-grained type-safe shared-memory interoperability. RichWasm is rich enough to serve as a typed compilation target for both typed garbage-collected languages and languages with an ownership-based type system and manually managed memory. RichWasm takes inspiration from earlier work on languages with linear capability types to support safe strong updates, and adds analogous unrestricted capability types for garbage-collected locations, allowing a module to provide fine-grained memory access to another module, regardless of memory-management strategy. RichWasm types are not intended to be made part of core Wasm; instead we compile RichWasm to core Wasm, allowing for use in existing environments. We have formalized RichWasm in Coq and proved type safety via progress and preservation.

Joint work with: Zoe Paraskevopoulou, Michael Fitzgibbons, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur.

Daniel Hillerström

Daniel Hillerström is a senior researcher at the Computing Systems Laboratory at the Huawei Research Center in Zurich, Switzerland. Previously, he was a research fellow at The University of Edinburgh working on the Effect Handler Oriented Programming project. Daniel Hillerström obtained his PhD from The University of Edinburgh on topic of the foundations of programming and implementing effect handlers.

Stack Switching in WebAssembly with Effect Handlers

WebAssembly is a low-level portable compilation target intended for a variety of programming languages. However, presently, WebAssembly is missing support for efficient compilation of non-local control flow features such as async/await, yield-style generators, lightweight threads, first-class continuations, and so forth. This means source languages with such features have to resort to ceremonious whole program transformations such a continuation-passing style to target WebAssembly. To address this disparity, we present a bespoke instruction set extension based on effect handlers known as WasmFX, where we model stacks as continuations. This extension is minimal as it adds only three main instructions for creating, suspending, and resuming continuations. Moreover, our primitive instructions are type-safe providing typed continuations which synergises well with the stack typing of WebAssembly. This talk will cover the design principles behind WasmFX, demonstrate some of the applications enabled by WasmFX, and discuss potential future extensions of WasmFX.

Philippa Gardner

Philippa Gardner is a professor in the Department of Computing at Imperial College London and and has a UKRI Established Fellowship from 2018–2023. Her current research focusses on program verification: in particular, reasoning about Web programs (JavaScript and DOM); and reasoning about concurrent programs. She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial. Philippa directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC, from 2017 to 2022. She chaired the BCS awards committee, 2013-2018, which decides the Lovelace medal (senior) and Roger Needham award (mid-career) for computer science and engineering.

TBC

Sukyoung Ryu

Sukyoung Ryu is a Professor at Korea Advanced Institute of Science and Technology (KAIST) and the Head of the School of Computing, KAIST. Her research area includes programming languages, software engineering, and information security. She received research awards from Google and Distinguished Paper Awards from ACM SIGSOFT. She is currently an associate editor of IEEE TSE, a member of ACM SIGPLAN EC and ACM SIGPLAN CARES. She holds BS, MS, and PhD, all in Computer Science, from KAIST. Before KAIST, she worked at Sun Microsystems and Harvard University.

Generating Executable Specification from Formal Semantics of WebAssembly

From its inception, WebAssembly (Wasm) was designed and developed with an end-to-end formal specification. For a new feature to be standardized in Wasm, four key artifacts must be presented: a formal (mathematical) specification of the feature, an accompanying prose pseudocode description, an implementation in the official reference interpreter, and a test suite. While this rigorous process can reduce errors, manually generating all the artifacts is labor intensive and error-prone. Recently, researchers have been working on a technology to express the formal specification of Wasm through a domain-specific language (DSL), which allows automatic generation of various artifacts. In this talk, we present an automatic generation of algorithmic artifacts from the definition of the Wasm semantics in the DSL.

Thomas Lively

Thomas is a software engineer on the WebAssembly team at Google. He both works on Wasm tooling and is active in the WebAssembly Community Group, chairing and co-chairing the Garbage Collection and Threads subgroups.

A Brief Tour of Binaryen

Binaryen is an open source WebAssembly optimizer and compiler toolkit used by nearly every toolchain targeting Wasm, making it one of the highest-impact places to experiment with new Wasm features. Join me for a brief tour of Binaryen in which we will discuss the tools it offers, some oddities of its IR, and opportunities for further research and development of its capabilities.