Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…)
summary
Mechanisation produces MSWasmCert as a conservative, proof‑assistant formalisation of MSWasm and WebAssembly 1.0 modules, and builds Iris‑MSWasm: a separation logic plus a logical relation that proves robust capability safety. The formal model encodes handles: base,bound,offset,valid,id with the dynamic load/store checks and trap semantics, locates typos and underspecifications in the pen‑and‑paper design, and ships reproducible artifacts and evaluated proofs showing the claims hold on a machine‑checked semantics.
AI-written summary · about
chapters (10)
- 0:00Iris-MSWasm introduction
- 1:26WebAssembly for formal analysis
- 2:50WebAssembly memory limits
- 3:52Capabilities in Memory-Safe WebAssembly
- 5:38Formalizing MSWM with Iris
- 7:02Capability safety contract
- 7:23Simple Iris-MSWasm example
- 9:49Logical relations for unknown code
- 13:42Contributions and future work
- 15:07Q&A
related talks
18mIris-Wasm: reasoning formally about Wasm and Wasm extensions
16mIris-Wasm: Robust and Modular Verification of WebAssembly Programs
25mMSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
19mIris-WasmFX: Modular Reasoning for Wasm Stack Switching
26mMemory Safety Preservation for WebAssembly
51mLightning Talks
21mRichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
19mUpdating WasmCert-Isabelle to WebAssembly 2.0