Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
summary
Paper claims that adding static invariants lets sandboxed code use simple function calls instead of heavyweight wrappers, and implements this end-to-end. A modified Lucet runtime removes wrapper costs and speeds Firefox image and font rendering by up to 29.7% and 10%, a binary verifier VeriZero checks Lucet-produced assembly in seconds and is backed by a logical-relation proof, and a purpose-built prototype SegmentZero32 enforces the rules with about 22.5% end-to-end overhead.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:50Third party code is everywhere
- 1:01The danger of third party code
- 1:45Sandbox third party code!
- 2:52The problems of heavyweight wrappers
- 4:46What does it mean for the boundary to be sea
- 6:22Confidentiality: no reading secrets
- 6:53The heavyweight situation
- 8:00type safe function calls
- 8:39callee-save register restoration
- 9:08information flow control
- 9:45Zero-cost conditions: removing heavyweight wrappers
- 13:47Validating VeriZero Theory
- 15:03the overhead of heavyweight wrappers
- 16:03the end-to-end costs of zero-cost Wasm
- 16:57the overhead of purpose built zero-cost SFI
- 17:51Zero-cost transitions: isolation without taxatio
related talks
32mIsolation without Containers
20mIsolation without Containers
47mSecure Sandboxing in a Post-Spectre World
29mIsolation without Containers
37mLucet: Safe WebAssembly Outside the Browser
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
42mAdventures in Making Wasm Fast and More Secure
54mLucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing