Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
summary
Mechanisation in Rocq produces WasmFXCert and a syntactic type-safety proof for Wasm with explicit stack continuations, proving the extension sound. Iris-WasmFX is a program logic built in Iris that verifies real libraries: a coroutine library and a generator implementation are mechanically checked. The work models the actual WasmFX primitives new, resume, suspend, uses Iris-WasmFX and WasmFXCert, and ships reusable artifacts and proofs demonstrating modular, protocol-based reasoning.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:34WebAssembly formal reasoning
- 2:20Iris separation logic
- 3:46Reasoning about Wasm variants
- 5:30WASM effects intro
- 7:39WASM effects instructions
- 11:55Modular reasoning protocol
- 14:25Suspend/resume rules
- 16:54Contributions
- 17:37Q&A
related talks
18mIris-Wasm: reasoning formally about Wasm and Wasm extensions
21mIris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…)
47mStack Switching in WebAssembly with Effect Handlers
18mContinuing WebAssembly with Effect Handlers
51mLightning Talks
29mVerification of WebAssembly Features
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
43mRichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssem...