Enabling Safe Shared-Memory Interoperability in WebAssembly
WebAssembly (Wasm) is a portable compilation target that enables almost-native execution speed for a variety of languages. Though Wasm provides a safe, sandboxed environment for programs to run in, Wasm lacks the necessary 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, then it essentially ends up sharing all of its memory, potentially allowing adversarial code to access and modify arbitrary parts of its memory. Unfortunately, the Wasm Interface Types proposal to enable safe interoperability focuses on “shared-nothing” interoperability, in which values are copied across language boundaries when necessary, while the current proposal to add garbage collection to Wasm lists language interoperability as a non-goal.
In this talk, we will present CapableWasm (CapWasm), a higher-level version of Wasm with an enriched capability-based type system to support fine-grained safe shared-memory interoperability. CapWasm builds on L^3 ’s linear capabilities, which support safe strong updates, and adds analogous shared capabilities for garbage-collected locations, allowing a module to provide fine-grained access to a location to another module, regardless of memory-management strategy. CapWasm 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. CapWasm is compiled to regular Wasm, allowing for use in existing environments. We have formalized CapWasm in Coq and are currently proving its safety via progress (proved) and preservation (in progress).
Sun 11 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
16:00 - 17:30
|Dependent Temporal Type-and-Effect System with Delimited Continuations|
|Enabling Safe Shared-Memory Interoperability in WebAssemblyVirtual|
|Verifying non-terminating programs with IO in F*|
Cezar-Constantin Andrici MPI-SP, Theo Winterhalter MPI-SP, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of TechnologyPre-print File Attached