Wasm Research Day 2022

For the 2023 edition, see here.

A Day to discuss research and long-term topics

Wasm Research Day brings together researchers from academia and industry, as well as participants in the CG standards body, to discuss research and long-term topics related to WebAssembly. Co-located with the October 26-27 hybrid Wasm Community Group Meeting, it allows a unique opportunity for participants to discuss ongoing standardization work as well as strategic directions for WebAssembly.

When / Where

When: Tuesday, October 25, 2022, 9:30AM - 4:30PM PST
Where: One Market Plaza, 55 Spear St, San Francisco, CA. (Google)
Signup: here.

Talks

Talks will include a mix of industry partners and academics on topics ranging from extending WebAssembly with new features, verifying security properties of Wasm and its implementations, new languages on Wasm, as well as studying and improving Wasm performance.

Speaker Hailing From Title Abstract
Yuhan Deng Stanford, PhD student Fixpoint: Computation-Centric Networking We propose putting computation at the center of what networked computers and cloud services do for their users. We envision a shared representation of a computation: a deterministic procedure, run in an environment of well-specified dependencies. This suggests an end-to-end argument for serverless computing, shifting the service model from "renting CPUs by the second" to "providing the unambiguously correct result of a computation." Accountability to these higher-level abstractions could permit agility and innovation on other axes. Our framework for computation-centric networking, Fixpoint, is based on a low-level lightweight language of computation on data, Fix. Fix represents computations with WebAssembly modules, and Fixpoint implements a toolchain that compiles Fix into raw machine codelets using wasm2c and libclang. The toolchain allows Fixpoint to invoke computations as virtual function calls, which is about 37x faster than vforking a Linux process based on our preliminary benchmarks.
Amal Ahmed Northeastern University RichWasm: Bringing Type Safe Shared-Memory Interoperability to WebAssembly Though Wasm provides a safe, sandboxed environment for programs to run in, it lacks the facilities to enable safe, shared-memory interoperability between Wasm modules, a feature that we believe is essential for a low-level language in a multi-language world. The problem is that if a Wasm module shares its memory with another module, it ends up sharing all of its memory, potentially allowing adversarial code to access and modify arbitrary parts of that memory. 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 are currently proving its safety via progress and preservation.
Marco Vassena Utrecht University MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code [slides] Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm--and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. The Memory-Safe WebAssembly (MSWasm) proposal extends Wasm with language-level memory-safety abstractions to precisely address this problem. In this paper, we realize the vision of MSWasm. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler--and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Three compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). MSWasm's general design makes it easy to support and swap different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs and leverage fast (especially hardware-based) enforcement techniques as they become available. On the PolyBenchC suite, our evaluation shows that the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 39% when using hardware memory capabilities for spatial safety and pointer integrity.
Conrad Watt University of Cambridge Usefully Mechanising All of WebAssembly This talk will describe WasmCert-Isabelle, a mechanisation of the WebAssembly specification; and recent work on developing WasmRef-Isabelle, a practically-useful reference implementation of WebAssembly that is verified with respect to this mechanisation.
Daniel Hillerström The University of Edinburgh WasmFX: Structured Stack Switching via Effect Handlers in WebAssembly [slides, code, code] Non-local control flow features provide the ability to suspend the current execution context and later resume it. Many industrial-strength programming languages feature a wealth of non-local control flow features such as async/await, coroutines, generators/iterators, effect handlers, call/cc, and so forth. For some programming languages non-local control flow is central to their identity, meaning that they rely on non-local control flow for efficiency, e.g. to support massively scalable concurrency. Currently, WebAssembly lacks support for implementing such features directly and efficiently without a circuitous global transformation of source programs on the producer side. One possible strategy is to add special support for each individual non-local control flow feature to Wasm, but this strategy does not scale to the next 700 non-local control flow features. Instead, the goal of this work is to introduce a unified structured mechanism based on Plotkin and Pretnar's effect handlers which is sufficiently general to cover present use-cases as well as being forwards compatible with future use-cases, whilst admitting efficient implementations.
Chris Woods & Ajay Chhokra Siemens An end-to-end toolchain for evaluating WebAssembly runtimes for CPS-IoT Use cases [slides] There exists several standalone WebAssembly (WASM) runtimes with small footprint, which aim at executing WASM workloads on resource constrained embedded devices. However, there is a lack of universal benchmarking framework and associated tooling infrastructure to gauge and derive the improvements in their performance. Having a well-defined framework along with a comprehensive set of benchmarking applications covering a wide range of domains will allow runtime developers to measure relevant performance characteristics and at the same time allow application developers to choose/ tune runtime(s) as per the constraints imposed by their respective domains, which is essential for safety critical applications running in resource constrained embedded devices. To that end, we propose an end-to-end toolchain for defining and executing various benchmark applications spanning over different runtimes with numerous configuration options as well as visualizing the end results. This toolchain aims at minimizing the time to set-up these runtimes, deploying benchmark applications to target devices and result visualization.
Adam T. Geller University of British Columbia, PhD student A Safe Way of Replacing Dynamic Checks with Static Checks in WebAssembly We present Wasm-check, which introduces variations of existing WebAssembly instructions but without run-time safety checks. To justify the removal of these checks (when possible), Wasm-check uses an indexed type system, which tracks constraints on program values. In this talk, we will first explain Wasm-check and how the type system justifies removing checks. We will then demonstrate how this may improve performance using micro-benchmarks, touch on some metatheoretic properties of Wasm-check, such as type safety and backwards compatibility with WebAssembly, and finally discuss some of the implementation tradeoffs and future work.
Arjun Ramesh & Tianshu Huang & Anthony Rowe Carnegie Mellon University Giving the Cloud an Edge with WASM [slides] The safe, open, portable, polyglot, properties of WebAssembly (WASM) make it appealing for a variety of applications that go beyond the web. In this talk, we discuss an orchestration platform where WASM provides key advantages in the automotive and industrial manufacturing domain. We highlight early work in leveraging WASM for performance metering, bytecode instrumentation, and performance prediction.
Ben L. Titzer Carnegie Mellon University WebAssembly as the Basis for Layered Runtime Systems WebAssembly is a low-level, portable bytecode offering a compilation target with near-native performance. Now a standard feature of all web browsers, Wasm has started to expand to many other applications such as edge computing, distributed cryptographic digital contracts, networking stacks, and more. As Wasm gains features through the standardization process, it becomes a more attractive target for new kinds of languages. In this talk I will fast-forward to look at a whole new set of language runtime system designs that are made possible with some new features that can be added to Wasm. In particular, can we build a *really* fast language implementation without having to write a new JIT compiler? A new code format (with validator)? A new garbage collector? Can we do this without ever having to look at assembly language? I hope so! Let's look at what I've discovered and what I think that means.

Speaker	Hailing From	Title	Abstract
Yuhan Deng	Stanford, PhD student	Fixpoint: Computation-Centric Networking	We propose putting computation at the center of what networked computers and cloud services do for their users. We envision a shared representation of a computation: a deterministic procedure, run in an environment of well-specified dependencies. This suggests an end-to-end argument for serverless computing, shifting the service model from "renting CPUs by the second" to "providing the unambiguously correct result of a computation." Accountability to these higher-level abstractions could permit agility and innovation on other axes. Our framework for computation-centric networking, Fixpoint, is based on a low-level lightweight language of computation on data, Fix. Fix represents computations with WebAssembly modules, and Fixpoint implements a toolchain that compiles Fix into raw machine codelets using wasm2c and libclang. The toolchain allows Fixpoint to invoke computations as virtual function calls, which is about 37x faster than vforking a Linux process based on our preliminary benchmarks.
Amal Ahmed	Northeastern University	RichWasm: Bringing Type Safe Shared-Memory Interoperability to WebAssembly	Though Wasm provides a safe, sandboxed environment for programs to run in, it lacks the facilities to enable safe, shared-memory interoperability between Wasm modules, a feature that we believe is essential for a low-level language in a multi-language world. The problem is that if a Wasm module shares its memory with another module, it ends up sharing all of its memory, potentially allowing adversarial code to access and modify arbitrary parts of that memory. 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 are currently proving its safety via progress and preservation.
Marco Vassena	Utrecht University	MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code [slides]	Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm--and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. The Memory-Safe WebAssembly (MSWasm) proposal extends Wasm with language-level memory-safety abstractions to precisely address this problem. In this paper, we realize the vision of MSWasm. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler--and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Three compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). MSWasm's general design makes it easy to support and swap different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs and leverage fast (especially hardware-based) enforcement techniques as they become available. On the PolyBenchC suite, our evaluation shows that the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 39% when using hardware memory capabilities for spatial safety and pointer integrity.
Conrad Watt	University of Cambridge	Usefully Mechanising All of WebAssembly	This talk will describe WasmCert-Isabelle, a mechanisation of the WebAssembly specification; and recent work on developing WasmRef-Isabelle, a practically-useful reference implementation of WebAssembly that is verified with respect to this mechanisation.
Daniel Hillerström	The University of Edinburgh	WasmFX: Structured Stack Switching via Effect Handlers in WebAssembly [slides, code, code]	Non-local control flow features provide the ability to suspend the current execution context and later resume it. Many industrial-strength programming languages feature a wealth of non-local control flow features such as async/await, coroutines, generators/iterators, effect handlers, call/cc, and so forth. For some programming languages non-local control flow is central to their identity, meaning that they rely on non-local control flow for efficiency, e.g. to support massively scalable concurrency. Currently, WebAssembly lacks support for implementing such features directly and efficiently without a circuitous global transformation of source programs on the producer side. One possible strategy is to add special support for each individual non-local control flow feature to Wasm, but this strategy does not scale to the next 700 non-local control flow features. Instead, the goal of this work is to introduce a unified structured mechanism based on Plotkin and Pretnar's effect handlers which is sufficiently general to cover present use-cases as well as being forwards compatible with future use-cases, whilst admitting efficient implementations.
Chris Woods & Ajay Chhokra	Siemens	An end-to-end toolchain for evaluating WebAssembly runtimes for CPS-IoT Use cases [slides]	There exists several standalone WebAssembly (WASM) runtimes with small footprint, which aim at executing WASM workloads on resource constrained embedded devices. However, there is a lack of universal benchmarking framework and associated tooling infrastructure to gauge and derive the improvements in their performance. Having a well-defined framework along with a comprehensive set of benchmarking applications covering a wide range of domains will allow runtime developers to measure relevant performance characteristics and at the same time allow application developers to choose/ tune runtime(s) as per the constraints imposed by their respective domains, which is essential for safety critical applications running in resource constrained embedded devices. To that end, we propose an end-to-end toolchain for defining and executing various benchmark applications spanning over different runtimes with numerous configuration options as well as visualizing the end results. This toolchain aims at minimizing the time to set-up these runtimes, deploying benchmark applications to target devices and result visualization.
Adam T. Geller	University of British Columbia, PhD student	A Safe Way of Replacing Dynamic Checks with Static Checks in WebAssembly	We present Wasm-check, which introduces variations of existing WebAssembly instructions but without run-time safety checks. To justify the removal of these checks (when possible), Wasm-check uses an indexed type system, which tracks constraints on program values. In this talk, we will first explain Wasm-check and how the type system justifies removing checks. We will then demonstrate how this may improve performance using micro-benchmarks, touch on some metatheoretic properties of Wasm-check, such as type safety and backwards compatibility with WebAssembly, and finally discuss some of the implementation tradeoffs and future work.
Arjun Ramesh & Tianshu Huang & Anthony Rowe	Carnegie Mellon University	Giving the Cloud an Edge with WASM [slides]	The safe, open, portable, polyglot, properties of WebAssembly (WASM) make it appealing for a variety of applications that go beyond the web. In this talk, we discuss an orchestration platform where WASM provides key advantages in the automotive and industrial manufacturing domain. We highlight early work in leveraging WASM for performance metering, bytecode instrumentation, and performance prediction.
Ben L. Titzer	Carnegie Mellon University	WebAssembly as the Basis for Layered Runtime Systems	WebAssembly is a low-level, portable bytecode offering a compilation target with near-native performance. Now a standard feature of all web browsers, Wasm has started to expand to many other applications such as edge computing, distributed cryptographic digital contracts, networking stacks, and more. As Wasm gains features through the standardization process, it becomes a more attractive target for new kinds of languages. In this talk I will fast-forward to look at a whole new set of language runtime system designs that are made possible with some new features that can be added to Wasm. In particular, can we build a really fast language implementation without having to write a new JIT compiler? A new code format (with validator)? A new garbage collector? Can we do this without ever having to look at assembly language? I hope so! Let's look at what I've discovered and what I think that means.

Round-table discussion

In addition to the research talks listed above, we'll include a roundtable discussion of strategic research questions for WebAssembly, including:

How can research best collaborate with the Wasm CG standards body?
What shared research infrastructure would benefit the community best?
How can research help improve the Wasm ecosystem?

Organization and Support

The WebAssembly Research Day is organized by Ben L. Titzer and Keith Winstein and partially supported by grants #2229731 and partnership with the DFinity Foundation, as well as a venue generously provided by Google.