{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T15:14:20Z","timestamp":1772032460365,"version":"3.50.1"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3689722","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"304-332","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-4093-2755","authenticated-orcid":false,"given":"Maxime","family":"Legoupil","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6778-6597","authenticated-orcid":false,"given":"June","family":"Rousseau","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5951-4642","authenticated-orcid":false,"given":"A\u00efna Linn","family":"Georges","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2311.07223"},{"key":"e_1_3_1_5_1","unstructured":"Matt Butcher. 2022. How to Think About WebAssembly (Amid the Hype). https:\/\/www.fermyon.com\/blog\/how-to-think-about-wasm"},{"key":"e_1_3_1_6_1","unstructured":"Lin Clark. 2019. Announcing the Bytecode Alliance: Building a secure by default composable future for WebAssembly. https:\/\/hacks.mozilla.org\/2019\/11\/announcing-the-bytecode-alliance\/"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/EUROSP.2016.22"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3337167.3337171"},{"key":"e_1_3_1_10_1","unstructured":"Fastly documentation. 2022. Compute@Edge. https:\/\/docs.fastly.com\/products\/compute-at-edge"},{"key":"e_1_3_1_11_1","volume-title":"Designing and Proving Robust Safety of Efficient Capability Machine Programs.","author":"Georges Aina Linn","year":"2023","unstructured":"Aina Linn Georges. 2023. Designing and Proving Robust Safety of Efficient Capability Machine Programs. Ph. D. Dissertation. Aarhus University."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_3_1_13_1","unstructured":"A\u00efna Linn Georges Armael Gueneau Thomas van Strydonck Amin Timany Alix Trieu Dominique Devriese and Lars Birkedal. 2022a. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. Technical Report. Aarhus University. https:\/\/cs.au.dk\/~birke\/papers\/cerise.pdf"},{"key":"e_1_3_1_14_1","article-title":"Cap\u2019 ou pas cap\u2019 ?: Preuve de programmes pour une machine \u00e0 capacit\u00e9s en pr\u00e9sence de code inconnu","author":"Georges A\u00efna Linn","year":"2021","unstructured":"A\u00efna Linn Georges, Arma\u00ebl Gu\u00e9neau, Thomas Van-Strydonck, Amin Timany, Dominique Trieu, Alix Devriese, and Lars Birkedal. 2021b. Cap\u2019 ou pas cap\u2019 ?: Preuve de programmes pour une machine \u00e0 capacit\u00e9s en pr\u00e9sence de code inconnu. In Journ\u00e9es Francophones des Langages Applicatifs 2021. https:\/\/cris.vub.be\/ws\/portalfiles\/portal\/55081793\/paper.pdf","journal-title":"Journ\u00e9es Francophones des Langages Applicatifs 2021"},{"key":"e_1_3_1_15_1","volume-title":"Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities","author":"Georges A\u00efna Linn","year":"2022","unstructured":"A\u00efna Linn Georges, Alix Trieu, and Lars Birkedal. 2022b. Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities. Technical Report. Aarhus University. https:\/\/cs.au.dk\/~ageorges\/publications_pdfs\/monotone-technical.pdf"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_1_17_1","unstructured":"Pat Hickey. 2020. How Fastly and the developer community are investing in the WebAssembly ecosystem. https:\/\/www.fastly.com\/blog\/how-fastly-and-developer-community-invest-in-webassembly-ecosystem"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2017 Paris France January 18-20 2017 Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Maxime Legoupil June Rousseau A\u00efna Linn Georges Jean Pichon-Pharabod and Lars Birkedal. 2024. Artifact and Appendix of \u2018Iris-MSWasm: elucidating and mechanising the security invariants of Memory- Safe WebAssembly\u2019. https:\/\/doi.org\/10.5281\/zenodo.13383121 10.5281\/zenodo.13383121","DOI":"10.5281\/zenodo.13383121"},{"key":"e_1_3_1_21_1","unstructured":"Daniel Lehmann Johannes Kinder and Michael Pradel. 2020. Everything Old is New Again: Binary Security of WebAssembly. In 29th USENIX Security Symposium USENIX Security 2020 August 12-14 2020 Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association 217\u2013234. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/lehmann"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"J. McCarthy and P.J. Hayes. 1981. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In Readings in Artificial Intelligence Bonnie Lynn Webber and Nils J. Nilsson (Eds.). Morgan Kaufmann 431\u2013450. https:\/\/doi.org\/10.1016\/B978-0-934613-03-3.50033-7 10.1016\/B978-0-934613-03-3.50033-7","DOI":"10.1016\/B978-0-934613-03-3.50033-7"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571208"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00055"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_27"},{"key":"e_1_3_1_28_1","unstructured":"Zoe Paraskevopoulou Michael Fitzgibbons Noble Mushtak Michelle Thalakottur Jose Sulaiman Manzur and Amal Ahmed. 2024. RichWasm: Bringing Safe Fine-Grained Shared-Memory Interoperability Down to WebAssembly. Technical Report. arXiv:2401.08287 https:\/\/arxiv.org\/pdf\/2401.08287.pdf"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_3_1_30_1","unstructured":"Andreas Rossberg. 2019. WebAssembly Core Specification W3C Recommendation. Technical Report. W3C. https:\/\/www.w3.org\/TR\/wasm-core-1\/"},{"key":"e_1_3_1_31_1","unstructured":"Andreas Rossberg. 2024. WebAssembly Specification Release 2.0\u2009+\u2009tail calls + function references + gc (Draft 2024-03-19). Technical Report. https:\/\/webassembly.github.io\/gc\/core\/syntax\/types.html"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_3_1_33_1","volume-title":"Formal Reasoning about Capability Machines","author":"Skorstengaard Lau","year":"2019","unstructured":"Lau Skorstengaard. 2019. Formal Reasoning about Capability Machines. Ph. D. Dissertation. Aarhus University."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_17"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363519"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_3_1_38_1","unstructured":"The Bytecode Alliance. 2023a. Component Model design and specification (GitHub repository). https:\/\/github.com\/WebAssembly\/component-model"},{"key":"e_1_3_1_39_1","unstructured":"The Bytecode Alliance. 2023b. The WebAssembly Component Model. https:\/\/component-model.bytecodealliance.org\/"},{"key":"e_1_3_1_40_1","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2022. A Logical Approach to Type Soundness. (2022). https:\/\/cs.au.dk\/~timany\/publications\/files\/2022-submitted-logical-type-soundness.pdf"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341688"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-987"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_4"},{"key":"e_1_3_1_44_1","volume-title":"The Cambridge CAP Computer and Its Operating System","author":"Wilkes M. V.","year":"1979","unstructured":"M. V. Wilkes and R. M. Needham. 1979. The Cambridge CAP Computer and Its Operating System. Elsevier. https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-cambridge-cap-computer-and-its-operating-system\/"},{"key":"e_1_3_1_45_1","unstructured":"Jonathan Woodruff Paul Metzger Robert N. M. Watson Brooks Davis Wes Filardo Jessica Clarke and John Baldwin. 2023. SOSP 2023 CHERI Exercises. https:\/\/www.cl.cam.ac.uk\/~pffm2\/sosp2023_cheri_tutorial\/cover\/README.html"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853201"},{"key":"e_1_3_1_47_1","unstructured":"Vadim Zaliva Kayvan Memarian Ricardo Almeida Jessica Clarke Brooks Davis Alex Richardson David Chisnall Brian Campbell Ian Stark Robert N. M. Watson and Peter Sewell. 2024. Formal Mechanised Semantics of CHERI C: Capabilities Provenance and Undefined Behaviour. http:\/\/www.cl.cam.ac.uk\/users\/pes20\/asplos24spring-paper110.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689722","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689722","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:03:44Z","timestamp":1770195824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689722"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":46,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689722"],"URL":"https:\/\/doi.org\/10.1145\/3689722","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}