Iris-Wasm: robust and modular verification of WebAssembly programs
File(s)
Published version
Author(s)
Type
Conference Paper
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.
Date Issued
2023-06-06
Date Acceptance
2023-03-31
Citation
Proceedings of the ACM on Programming Languages, 2023, 7, pp.1096-1120
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1096
End Page
1120
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
7
Copyright Statement
© 2023 Copyright held by the owner/author(s).
This work is licensed under a Creative Commons Attribution 4.0 International License.
This work is licensed under a Creative Commons Attribution 4.0 International License.
License URL
Identifier
https://dl.acm.org/doi/10.1145/3591265
Source
PLDI 2023
Publication Status
Published
Start Date
2023-06-17
Finish Date
2023-06-21
Coverage Spatial
Orlando
Date Publish Online
2023-06-06