Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly
This program is tentative and subject to change.
WebAssembly offers coarse-grained encapsulation guarantees via its module system, but does not support fine-grained sharing of its linear memory. MSWasm is a recent proposal which extends WebAssembly with fine-grained memory sharing via handles, a type of capability that guarantee spatial and temporal safety, and thus enables an expressive yet safe style of programming with flexible sharing. In this paper, we formally validate the pen-and-paper design of MSWasm. To do so, we first define MSWasmCert, a mechanisation of MSWasm that makes it a fully-defined, conservative extension of WebAssembly 1.0, including the module system. We then develop Iris-MSWasm, a foundational reasoning framework for MSWasm composed of a separation logic to reason about known code, and a logical relation to reason about unknown, potentially adversarial code. Iris-MSWasm thereby makes explicit a key aspect of the implicit universal contract of MSWasm: robust capability safety. We apply Iris-MSWasm to reason about key use cases of handles, in which the effect of calling an unknown function is bounded by robust capability safety. Iris-MSWasm thus works as a framework to prove complex security properties of MSWasm programs, and provides a foundation to evaluate the language-level guarantees of MSWasm.
This program is tentative and subject to change.
Fri 25 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:20 | |||
11:00 20mTalk | A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code OOPSLA 2024 Julien Simonnet CEA LIST, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Mihaela Sighireanu University Paris-Saclay, ENS Paris-Saclay, CNRS, LMF | ||
11:20 20mTalk | Modeling Dynamic (De)Allocations of Local Memory for Translation Validation OOPSLA 2024 | ||
11:40 20mTalk | Mark--Scavenge: Waiting for Trash to Take Itself Out OOPSLA 2024 Jonas Norlinder Uppsala University, Erik Österlund Oracle, David Black-Schaffer Uppsala University, Tobias Wrigstad Uppsala University | ||
12:00 20mTalk | Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly OOPSLA 2024 Maxime Legoupil Aarhus University, June Rousseau Aarhus University, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Jean Pichon-Pharabod Aarhus University, Lars Birkedal Aarhus University |