WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
summary
A prototype compiler verifies sandboxing properties for WebAssembly by lowering Wasm into an unstructured CFG family early, doing optimizations there, and emitting x86_64 with sandboxing checks; verification work uses F with SMT and a machine model inspired by HACL/x64. Indirect-call tables and globals live outside the sandbox* so a single checked lookup plus bounds checks gives control‑flow integrity; many memory checks are conservatively injected now but a verified data‑flow/abstract‑interpretation pass already proves and removes a large subset. The design is partially proven, works end‑to‑end to .s output, and aims to finish full proofs.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:22What Why is WebAssembly?
- 2:52Software Sandboxing Beyond the Web
- 4:18Software Sandboxing & SFI
- 4:46WASM: Attractive Narrow Waist
- 5:41Formal Definition of Sandboxing
- 7:47Choice of Semantics
- 8:40Surprisingly, Unstructured Structured
- 11:43Structure of the Sandboxes
- 13:01Handling Function Calls
- 13:33Control-Flow Integrity (CFI)
- 14:24Current Implementation (in Progress)
- 15:30Structure of the Compiler
- 17:46WASM as an IL for Provably-Safe Software Sandboxing
related talks
35mModern Sandboxing: Using Web Assembly in Java
42mAdventures in Making Wasm Fast and More Secure
36mSandboxing Your Sandbox: Leveraging Hypervisors for WebAssembly Security
32mIsolation without Containers
48mDon't Trust Anything! Real-world Uses For WebAssembly
01h 08mOn WebAssembly
26mSyscall Me by Your Name: Sandboxing Wasm Programs
53mWebAssembly