| Time | Speaker | Format | Affiliation | Title | Abstract |
|---|---|---|---|---|---|
| 9:00-9:15 (15 mins) |
Elizabeth Gilbert | Carnegie Mellon University | Research Day Introductions | ||
| 9:15-9:45 (30 mins) |
Andrew Brown & Andrew Tolmach | remote | Portland State University | Meta-tracing Interpreters in WebAssembly | We will describe work in progress on constructing a meta-tracing JIT compiler to improve the performance of interpreted programs within WebAssembly. Our framework combines a set of independent tools that capture WebAssembly traces, identify loops in user programs, reconstruct optimized trace fragments, and transfer control from fragments via on-stack replacement. |
| 9:45-10:15 (30 mins) |
Guannan Wei | remote | INRIA-ENS; Tufts University | Reconstructing Continuation-Passing Semantics for WebAssembly | WebAssembly is now a popular low-level intermediate representation (IR) and compilation target. The official specification of WebAssembly provides a small-step reduction semantics. Unlike other common low-level IRs, WebAssembly provides structured control-flow constructs, whose reduction rules are complicated by additional administrative instructions in the reference semantics. In this talk, we will present an alternative semantics in continuation-passing style (CPS) that is concise, compositional, and tail-recursive. The CPS semantics can be implemented straightforwardly as an interpreter. Using continuations from the meta-language eliminates the need to introduce administrative instructions. We will further demonstrate that the CPS semantics can be extended to support other forms of control abstractions, such as effect handlers. |
| 10:15-10:45 (30 mins) |
Naomi Smith | in-person | UC San Diego | Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution | Just-in-time (JIT) compilers make JavaScript run efficiently by replacing slow JavaScript interpreter code with fast machine code. However, this efficiency comes at a cost: bugs in JIT compilers can completely subvert all language-based (memory) safety guarantees, and thereby introduce catastrophic exploitable vulnerabilities. We present Icarus: a new framework for implementing JIT compilers that are automatically, formally verified to be safe, and which can then be converted to C++ that can be linked into browser runtimes. Crucially, we show how to build a JIT with Icarus such that verifying the JIT implementation statically ensures the security of all possible programs that the JIT could ever generate at run-time, via a novel technique called symbolic meta-execution that encodes the behaviors of all possible JIT-generated programs as a single Boogie meta-program which can be efficiently verified by SMT solvers. We evaluate Icarus by using it to re-implement components of Firefox's JavaScript JIT. We show that Icarus can scale up to expressing complex JITs, quickly detects real-world JIT bugs and verifies fixed versions, and yields C++ code that is as fast as hand-written code. |
| 10:45-11:00 (15 mins) |
Break | --- | --- | --- | --- |
| 11:00-11:30 (30 mins) |
Léo Andrès | remote | OCamlPro | Cross-language bug-finding and solver-aided programming through Wasm | We'll show how we built a cross-language, multi-solver and multi-core symbolic engine that can be used for bug-finding or solver-aided programming thanks to Wasm. For instance we found a bug in the Rust stdlib ; and are able to generate music for string quartets respecting some classical harmony rules. We'll also present some recent work on symbolic annotation checking on C code by re-using ACSL and on Wasm by using Weasel, a new specification language for Wasm. |
| 11:30-12:00 (30 mins) |
Maxime Legoupil | remote | Aarhus Universitet | Iris-Wasm: a mechanisation, program logic and logical relation to formally reason about WebAssembly and its proposed extensions | WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher-order modular programming. We introduce Iris-Wasm (PLDI'23), a mechanised higher-order separation logic building on a specification of Wasm 1.0 mechanised in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby formally demonstrating that WebAssembly enforces strong isolation between modules. Iris-Wasm is also an optimal starting point to formally reason about extension to WebAssembly, such as MSWasm (Iris-MSWasm was presented at OOPSLA'24) and WasmFX (Iris-WasmFX is a work in progress). Formally describing and proving the desired properties of these extensions is a strong asset in validating them and encouraging their adoption. |
| 12:00-1:00 (1 hr) |
Lunch (provided) | --- | --- | --- | --- |
| 1:00-1:30 (30 mins) |
Edoardo Vacchi | remote | Dylibso | Introducing Chicory: a portable Wasm runtime for the JVM and beyond | We introduce Chicory, a pure Java Wasm runtime. We will discuss what makes it different from other runtimes, in particular we will compare it to wazero runtime for Go. We will also give a sneak peek on some ongoing work to port Chicory to Android. |
| 1:30-2:00 (30 mins) |
Arjun Ramesh | in-person | Carnegie Mellon University | Holistic Observability of Cyber-Physical Systems | Cyber-Physical Systems (CPS) involve intricate interactions between digital program execution and the physical dynamics of the system environment. CPS observability for debugging or profiling today often studies physical and digital aspects in isolation, thus relying on human experts for holistic system insights. Such approaches are impractical as increasingly complex sensing/intelligence are pushed into domains like automotives, VR, and factory automation. In this talk, we explore holistic CPS observability by integrating Wasm program execution and sensor data of system dynamics to understand CPS operation across the joint distribution of digital-physical state. |
| 2:00-2:30 (30 mins) |
Markus Scherer | in-person | TU Wien | Wappler and Beyond: Reachability and Noninterference Analysis for WebAssembly | In this talk I will present ongoing research on the static analysis of WebAssembly in our research group. First, I will introduce Wappler, our reachability solver presented at CSF'24, and cover which of Wasm's properties make it amenable to static analysis and which of its properties can cause problems. Afterward, I will talk about our current research that lifts reachability analyses like Wappler to noninterference. This hyperproperty allows us to reason about an attacker's ability to compromise integrity and confidentiality in a system and is inherently interesting due to Wasm's role as interface between different parts of a system. |
| 2:30-3:00 (30 mins) |
Break | --- | --- | --- | --- |
| 3:00-3:30 (30 mins) |
Eliot Moss | remote | University of Massachusetts Amherst | A Simple Transaction Extension for WebAssembly | On the way toward persistent programming support in Web Assembly, we have designed and are implementing a simple transactions extension. This offers standard ACID transactions without the durability (that would come with persistence). We add transactional versions of Wasm memory and heap objects along with suitable types for them. We add transaction-related permissions to references, which enable reducing the number of transaction related checks at run time. |
| 3:30-4:00 (30 mins) |
Amal Ahmed | in-person | Northeastern University | RichWasm Realizability: Facilitating Specification of ABIs for the WebAssembly Platform | RichWasm is a novel richly typed intermediate language designed 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. It makes use of capability types to ensure fine-grained memory ownership and sharing. In this talk, I'll describe work in progress on building a realizability model for RichWasm -- a semantic model of RichWasm types as sets os WebAssembly code and data that realize the behavior prescribed by those types. Such a model specifies an ABI for RichWasm, since it specifies the data layout, calling conventions, and constraints on ownership and sharing for RichWasm types. A powerful benefit of this model is that it immediately yields a specification of ABIs for high-level typed languages for which we have a type-preserving compiler to RichWasm. |
| 4:00-4:15 (15 mins) |
Break | --- | --- | --- | --- |
| 4:15-4:45 (30 mins) |
Dongjun Youn | remote | KAIST | West: Automatic Wasm Test Generation using SpecTec | This talk is about the work-in-progress project called West, an automatic Wasm test generation framework. West is built on top of SpecTec, a mechanized specification framework for Wasm. We were able to identify some of the previously unknown bugs from one of the well-known Wasm runtimes, Wasmtime. |
| 4:45-5:15 (30 mins) |
Doehyun Baek | remote | KAIST | RR-Reduce: Execution-Aware Program Reduction via Record-Replay | Program reduction is an important software engineering tool that aims to minimize a program's size while preserving a specific property of interest of the program. It is a key technique for debugging issues in compilers, runtime engines, and interpreters which are often well-tested on small programs but have latent bugs only exhibited when running large programs found in the wild. Previous work reduced input programs via syntactic and semantic code transformations. However, we observe that debugging a crash in a runtime engine often involves repeatedly executing the program-to-reduce, which provides valuable information not previously exploited for program reduction. This paper presents RR-Reduce, an execution-aware program reduction technique that leverages a record-and-replay mechanism to reduce programs. Our approach retains only a small subset of the input program's code and replaces the rest with replay logic that plays back recorded side-effects demanded by the original code. RR-Reduce performs three main steps: First, heuristically identify critical parts of the program that must be retained. Second, split the program into two subprograms-one containing the critical parts and another containing the remainder. Third, use record-and-replay to generate a new program that includes the critical parts and replay code necessary to execute the critical parts in a way that reproduces the property of interest. Our evaluation applies the approach to a set of WebAssembly binaries that trigger bugs in three runtime engines, showing that the approach is (1) effective - RR-Reduce produces a reduced program that is 5.72x smaller compared to prior work. (2) applicable - RR-Reduce is able to successfully reduce the given input program in 98.09% of cases, resulting into a program that has only 3.26% of the original program's size; (3) efficient - RR-Reduce takes 3.41x less time to produce a reduced program, where most of the time spent is independent of the size of the input program. |
| 5:15-5:30 (15 mins) |
Discussion | --- | --- | --- | --- |
Copyright (c) 2025, the WebAssembly Research Center at CMU.