Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
summary
Iris-Wasm mechanizes Wasm 1.0 in Coq on top of the Iris framework and claims modular, higher-order verification that composes across host boundaries. It builds a program logic, a host‑parametric interface, and a logical relation that enforces robust safety so unknown code can only affect exports. The authors prove module instantiation rules, verify a higher‑order stack module (specs for map and preservation of length), and ship evaluated artifacts demonstrating the toolchain works end‑to‑end.
AI-written summary · about
chapters (12)
- 0:00Iris-Wasm verification project
- 1:02WebAssembly runtime semantics
- 3:09Motivation for modular WASM verification
- 4:37Limitations of prior WASM verification
- 5:40Iris-Wasm framework features
- 6:22Separation logic core
- 8:07Host-WASM interoperation
- 9:53Modular WASM instantiation
- 10:57Safety verification of WASM
- 11:39Demonstration: stack model & higher-order functions
- 13:03Summary & acknowledgments
- 13:23Q&A
related talks
21mIris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…)
21mRichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
53mWebAssembly
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
50mWeb Assembly
43mMeet Your Future - WebAssembly
46mWebAssembly (Digging a bit deeper)
34mPlaying Safely in the...