Iris-Wasm: reasoning formally about Wasm and Wasm extensions
summary
Iris-Wasm is a Coq mechanisation of WebAssembly 1.0 built on the Iris framework that gives a higher-order, modular separation logic and a machine-checked logical relation; it proves that well-typed modules satisfy robust safety so adversarial imports can only affect what modules explicitly export. The development verifies modular composition and type soundness, and it already scales to extensions like MSWasm, RichWasm and stack-switching where capability safety and effect-handler reasoning are mechanised and proved.
AI-written summary · about
chapters (12)
- 0:00Iris-Wasm intro and formal reasoning
- 1:04Formal reasoning with proof assistants
- 3:13WebAssembly for formal verification
- 4:36Iris-Wasm framework core
- 6:22Resource-based reasoning in Iris-Wasm
- 8:28Safety and local state encapsulation
- 9:53Extending Iris-Wasm to new variants
- 11:59Iris-MSw: Memory-safe Wasm with caps
- 13:44Iris-WAM: Stack switching and effects
- 14:46Iris-RichWasm: Richer Wasm types
- 15:29Future directions with SpectaC
- 16:53Q&A: Concurrency in Iris-Wasm
related talks
19mIris-WasmFX: Modular Reasoning for Wasm Stack Switching
21mIris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…)
21mRichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
43mRichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssem...
51mLightning Talks
01h 08mOn WebAssembly
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
29mVerification of WebAssembly Features