Full-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the Sandbox
summary
A real bug in Cranelift causes a JIT-produced load to become sign‑extended instead of zero‑extended, letting a wasm instance access another instance’s memory and producing a CVE; fixes combine three concrete techniques: Cranelift miscompilation (zero vs sign extend) is caught by SMT-backed Isle verification of lowering rules, machine-code checks use an updated Verm-style abstract interpreter (now handling multiple static memories at ~1% compile overhead), and longer-term work uses proof-carrying code and interpreter→JIT partial evaluation to provide cheap, checkable guarantees.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:05What is WebAssembly
- 3:59WebAssembly breach incident
- 10:16Trust compiler isolation
- 12:00Compiler correctness techniques
- 14:27Verifying Cranelift lowering
- 21:27End-to-end verification bugs
- 22:52Verm SFI safety
- 28:29Practical verifier requirements
- 29:14Proof carrying code
- 33:03Correctness inside sandbox
- 35:30Single-source interpreter
- 36:12Q&A
related talks
28mSecurity and Correctness in Wasmtime
26mSyscall Me by Your Name: Sandboxing Wasm Programs
17mWaltzz: WebAssembly Runtime Fuzzing with Stack-Invariant Transformation
36mSandboxing Your Sandbox: Leveraging Hypervisors for WebAssembly Security
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
50mSmashing the Stack: Let’s Make It Less Fun And Unprofitable!
35mModern Sandboxing: Using Web Assembly in Java
37mBridging the Architecture Divide: How Hardware Limits Wasm, and How We Can Do Better