Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly

Maxime Legoupil*, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal

*Corresponding author af dette arbejde

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avisTidsskriftartikelForskningpeer review

1 Citationer (Scopus)

Abstract

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 guarantees 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.

OriginalsprogEngelsk
Artikelnummer282
TidsskriftProceedings of the ACM on Programming Languages
Vol/bind8
NummerOOPSLA2
ISSN2475-1421
DOI
StatusUdgivet - okt. 2024

Fingeraftryk

Dyk ned i forskningsemnerne om 'Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly'. Sammen danner de et unikt fingeraftryk.

Citationsformater