Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

Xiaojia Rao; Aïna Linn Georges; Maxime Legoupil; Conrad Watt; Jean Pichon-Pharabod; Philippa Gardner; Lars Birkedal

doi:10.1145/3591265

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal

Institut for Datalogi

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

8 Citationer (Scopus)

Abstract

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.

Originalsprog	Engelsk
Artikelnummer	151
Tidsskrift	Proceedings of the ACM on Programming Languages
Vol/bind	7
ISSN	2475-1421
DOI	https://doi.org/10.1145/3591265
Status	Udgivet - jun. 2023

Adgang til dokumentet

10.1145/3591265Licens: CC BY

3591265Forlagets udgivne version, 349 KBLicens: CC BY

Citationsformater

@article{3e8d1eeba0e84c2c91acfa5349be0acc,

title = "Iris-Wasm: Robust and Modular Verification of WebAssembly Programs",

abstract = "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.",

keywords = "formal verification, higher-order logic, separation logic, WebAssembly",

author = "Xiaojia Rao and Georges, {A{\"i}na Linn} and Maxime Legoupil and Conrad Watt and Jean Pichon-Pharabod and Philippa Gardner and Lars Birkedal",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.",

year = "2023",

month = jun,

doi = "10.1145/3591265",

language = "English",

volume = "7",

journal = "Proceedings of the ACM on Programming Languages ",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

}

TY - JOUR

T1 - Iris-Wasm

T2 - Robust and Modular Verification of WebAssembly Programs

AU - Rao, Xiaojia

AU - Georges, Aïna Linn

AU - Legoupil, Maxime

AU - Watt, Conrad

AU - Pichon-Pharabod, Jean

AU - Gardner, Philippa

AU - Birkedal, Lars

PY - 2023/6

Y1 - 2023/6

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

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

KW - formal verification

KW - higher-order logic

KW - separation logic

KW - WebAssembly

U2 - 10.1145/3591265

DO - 10.1145/3591265

M3 - Journal article

AN - SCOPUS:85162034301

SN - 2475-1421

VL - 7

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

M1 - 151

ER -

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

Abstract

Adgang til dokumentet

Fingeraftryk

Citationsformater