Indexed Types for a Statically Safe WebAssembly - POPL 2024

Explore a groundbreaking approach to enhancing WebAssembly's safety and performance in this 18-minute conference talk from POPL 2024. Dive into Wasm-prechk, a WebAssembly superset that leverages indexed types to express and verify constraints on program values, enabling the safe removal of dynamic safety checks. Learn how this innovation, implemented as an extension of the Wasmtime compiler and runtime, achieves an average 1.71x speed improvement in the PolyBenchC benchmark suite with minimal overhead. Examine the proofs of type and memory safety, backwards compatibility, and type erasure to WebAssembly. Gain insights into the design and implementation trade-offs, and understand the potential impact on optimizing WebAssembly programs for enhanced efficiency and security.