ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Sun 11 Sep 2022 16:30 - 17:00 at M1 - HOPE Session 4

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 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

16:00 - 17:30
HOPE Session 4HOPE at M1
16:00
30m
Talk
Dependent Temporal Type-and-Effect System with Delimited Continuations
HOPE
Taro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP
16:30
30m
Talk
Enabling Safe Shared-Memory Interoperability in WebAssemblyVirtual
HOPE
Michael Fitzgibbons Northeastern University (USA), Zoe Paraskevopoulou Northeastern University, Noble Mushtak Northeastern University, Amal Ahmed Northeastern University, USA
17:00
30m
Talk
Verifying non-terminating programs with IO in F*
HOPE
Cezar-Constantin Andrici MPI-SP, Théo Winterhalter MPI-SP, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of Technology
Pre-print File Attached