What is Fairy Dust? Universal Contracts for WebAssembly
summary
Proposes making WebAssembly’s informal “fairy dust” into explicit universal contracts by identifying, formalizing and proving language guarantees such as type soundness and robust safety. Demonstrates a case study for module-level local state encapsulation, formalized in a theorem prover and reasoned about with Iris/separation-logic style ownership, showing reentrancy and stack-switching complicate bracketing and can break naive expectations. Calls for standardizing these proved properties and requiring proposals to preserve or justify changes to them.
AI-written summary · about
chapters (9)
- 0:00WebAssembly safety basics
- 1:06Defining WebAssembly safety
- 3:56Control flow integrity
- 5:41External sandboxing
- 8:29Module boundaries
- 10:55Universal contracts
- 14:09Local state encapsulation
- 21:37Call for community action
- 22:42Q&A
related talks
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
07mBuilding New Software Foundations With the WebAssembly Comp...
16mIris-Wasm: Robust and Modular Verification of WebAssembly Programs
29mVerification of WebAssembly Features
19mIris-WasmFX: Modular Reasoning for Wasm Stack Switching
51mLightning Talks
01h 06mAs low-level as possible, but no lower
43mMeet Your Future - WebAssembly