{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:13Z","timestamp":1780994713213,"version":"3.54.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"villum investigator grant","award":["25804"],"award-info":[{"award-number":["25804"]}]},{"name":"EPSRC fellowship","award":["EP\/R034567\/1"],"award-info":[{"award-number":["EP\/R034567\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>WebAssembly makes it possible to run C\/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher- order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.<\/jats:p>","DOI":"10.1145\/3591265","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1096-1120","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Iris-Wasm: Robust and Modular Verification of WebAssembly Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4391-1214","authenticated-orcid":false,"given":"Xiaojia","family":"Rao","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5951-4642","authenticated-orcid":false,"given":"A\u00efna Linn","family":"Georges","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4093-2755","authenticated-orcid":false,"given":"Maxime","family":"Legoupil","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0596-877X","authenticated-orcid":false,"given":"Conrad","family":"Watt","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4187-0585","authenticated-orcid":false,"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Lecture Notes on Iris: Higher-Order Concurrent Separation Logic","author":"Birkedal Lars","unstructured":"Lars Birkedal and Ale\u0161 Bizjak . 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic . Aarhus University . Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. Aarhus University."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3337167.3337171"},{"key":"e_1_2_1_3_1","unstructured":"Daniel Ehrenberg. 2019. WebAssembly JavaScript Interface W3C Recommendation. W3C. https:\/\/www.w3.org\/TR\/wasm-js-api-1\/ \t\t\t\t  Daniel Ehrenberg. 2019. WebAssembly JavaScript Interface W3C Recommendation. W3C. https:\/\/www.w3.org\/TR\/wasm-js-api-1\/"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086399"},{"key":"e_1_2_1_5_1","unstructured":"Michael Fitzgibbons. 2022. CapableWasm: Bringing Better Interop Down to WebAssembly. https:\/\/www.youtube.com\/watch?v=E44lTaa2qHk POPL\u201922 student research competition presentation \t\t\t\t  Michael Fitzgibbons. 2022. CapableWasm: Bringing Better Interop Down to WebAssembly. https:\/\/www.youtube.com\/watch?v=E44lTaa2qHk POPL\u201922 student research competition presentation"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_2_1_7_1","volume-title":"Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code","author":"Georges A\u00efna Linn","year":"2022","unstructured":"A\u00efna Linn Georges , Arma\u00ebl Gu\u00e9neau , Thomas van Strydonck , Amin Timany , Alix Trieu , Dominique Devriese , and Lars Birkedal . 2022 . Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code . Aarhus University . https:\/\/cs.au.dk\/~birke\/papers\/cerise.pdf A\u00efna Linn Georges, Arma\u00ebl Gu\u00e9neau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. 2022. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. Aarhus University. https:\/\/cs.au.dk\/~birke\/papers\/cerise.pdf"},{"key":"e_1_2_1_8_1","volume-title":"Cap","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 . 2021. 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 A\u00efna Linn Georges, Arma\u00ebl Gu\u00e9neau, Thomas Van-Strydonck, Amin Timany, Dominique Trieu, Alix Devriese, and Lars Birkedal. 2021. 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"},{"key":"e_1_2_1_9_1","volume-title":"Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities","author":"Georges A\u00efna Linn","unstructured":"A\u00efna Linn Georges , Alix Trieu , and Lars Birkedal . 2022. Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities . Aarhus University . https:\/\/cs.au.dk\/~ageorges\/publications_pdfs\/monotone-technical.pdf A\u00efna Linn Georges, Alix Trieu, and Lars Birkedal. 2022. Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities. Aarhus University. https:\/\/cs.au.dk\/~ageorges\/publications_pdfs\/monotone-technical.pdf"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_11_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA , November 2-4, 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_13_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 \t\t\t\t  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_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498688"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_21_1","volume-title":"29th USENIX Security Symposium, USENIX Security 2020","author":"Lehmann Daniel","year":"2020","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 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_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571208"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_2_1_25_1","first-page":"978 17","volume-title":"Proceedings of the 29th USENIX Conference on Security Symposium. USENIX Association, USA. Article 40","author":"Narayan Shravan","year":"2020","unstructured":"Shravan Narayan , Craig Disselkoen , Tal Garfinkel , Nathan Froyd , Eric Rahm , Sorin Lerner , Hovav Shacham , and Deian Stefan . 2020 . Retrofitting Fine Grain Isolation in the Firefox Renderer . In Proceedings of the 29th USENIX Conference on Security Symposium. USENIX Association, USA. Article 40 , 18 pages. isbn: 978 - 971 -939133- 17 - 15 Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020. Retrofitting Fine Grain Isolation in the Firefox Renderer. In Proceedings of the 29th USENIX Conference on Security Symposium. USENIX Association, USA. Article 40, 18 pages. isbn:978-1-939133-17-5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111066"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7808708"},{"key":"e_1_2_1_28_1","unstructured":"Andreas Rossberg. 2019. WebAssembly Core Specification W3C Recommendation. W3C. https:\/\/www.w3.org\/TR\/wasm-core-1\/ \t\t\t\t  Andreas Rossberg. 2019. WebAssembly Core Specification W3C Recommendation. W3C. https:\/\/www.w3.org\/TR\/wasm-core-1\/"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.9"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_4"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_25"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016875"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591265","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":35,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591265"],"URL":"https:\/\/doi.org\/10.1145\/3591265","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}