RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Zoe Paraskevopoulou, Michael Fitzgibbons, Michelle Thalakottur, Noble Mushtak, Jose Sulaiman Mazur, Amal Ahmed
TL;DR
RichWasm tackles safe, fine-grained cross-language sharing in WebAssembly by introducing a richly typed intermediate language that supports both garbage-collected and manually managed memory. Its core is a substructural type system with capabilities and size tracking, enabling static verification of memory ownership and sharing across modules, and it targets a lowering to Wasm for real-world deployment. The work provides compilers from ML and L^3 to RichWasm, proves type safety in Coq (progress and preservation), and demonstrates how unsafe inter-language interactions are blocked by type checks. It also presents a path from RichWasm to Wasm, outlining how existing hosts can run RichWasm programs while preserving inter-language safety. Together, these contributions advance safe FFI design and multi-language interoperability on the WebAssembly platform, with practical implications for compiling diverse languages to a common, type-checked runtime.
Abstract
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 paper, we present RichWasm, a novel richly typed intermediate language designed to serve as a compilation target for typed high-level languages with different memory-safety guarantees. RichWasm is based on WebAssembly and enables safe shared-memory interoperability by incorporating a variety of type features that support fine-grained memory ownership and sharing. 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. We demonstrate this by providing compilers from core ML and L3, a type-safe language with strong updates, to RichWasm. RichWasm is compiled to regular Wasm, allowing for use in existing environments. We formalize RichWasm in Coq and prove type safety.