Indexed Types for a Statically Safe WebAssembly

Reference. Indexed Types for a Statically Safe WebAssembly

Adam T. Geller, Justine Frank, William J. Bowman · POPL · 2024 · refinement-types · PDF · DOI · pldb

We present Wasm-precheck, a superset of WebAssembly (Wasm) that uses indexed types to express and check simple constraints over program values. This additional static reasoning enables safely removing dynamic safety checks from Wasm, such as memory bounds checks. We implement Wasm-precheck as an extension of the Wasmtime compiler and runtime, evaluate the run-time and compile-time performance of Wasm-precheck vs Wasm configurations with explicit dynamic checks, and find an average run-time performance gain of 1.71 x faster in the widely used PolyBenchC benchmark suite, for a small overhead in binary size ( 7.18 % larger) and type-checking time (1.4% slower). We also prove type and memory safety of Wasm-precheck, prove Wasm safely embeds into Wasm-precheck ensuring backwards compatibility, prove Wasm-precheck type-erases to Wasm, and discuss design and implementation trade-offs.

Cite

Cite as @geller-2024-indexed (helia, typst) · \cite{geller-2024-indexed} (LaTeX)

BibTeX

bibtex · 1 line

@article{geller-2024-indexed, title={Indexed Types for a Statically Safe WebAssembly}, volume={8}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3632922}, DOI={10.1145/3632922}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Geller, Adam T. and Frank, Justine and Bowman, William J.}, year={2024}, month=Jan, pages={2395–2424} }

hayagriva YAML (typst)

yaml · 19 lines

geller-2024-indexed:
  type: article
  title: Indexed Types for a Statically Safe WebAssembly
  author:
  - Geller, Adam T.
  - Frank, Justine
  - Bowman, William J.
  date: 2024-01
  page-range: 2395-2424
  url: http://dx.doi.org/10.1145/3632922
  serial-number:
    doi: 10.1145/3632922
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 8

Download: geller-2024-indexed.bib · geller-2024-indexed.yml

Cites 28 works (0 here)

External (28)

Artifacts and Reproduction Package for Article `Indexed Types for a Statically Safe WebAssembly' (2024)
VectorVisor: A Binary Translation Scheme for Throughput-Oriented GPU Acceleration (2023)
WebAssembly Core Specification (2022)
Safer at any speed: automatic context-aware safety enhancement for Rust (2021)
Refinement Types: A Tutorial (2020)
The Cost of Software-Based Memory Management Without Virtual Memory (2020)
Not So Fast: Analyzing the Performance of WebAssembly vs. Native Code (2019)
Wasmtime: A fast and secure runtime for WebAssembly (2019)
Bringing the web up to speed with WebAssembly (2017)
Refinement Types for Ruby (2017)
Refinement types for TypeScript (2016)
PolyBench/C: The Polyhedral benchmark suite, v4.2.1 (2016)
LiquidHaskell: experience with refinement types in the real world (2014)
Refinement types for Haskell (2014)
STABILIZER: statistically sound performance evaluation (2013)
Dependent types for JavaScript (2012)
CSolve: Verifying C with Liquid Types (2012)
Low-level liquid types (2010)
Type-based data structure verification (2009)
Semantics engineering with PLT Redex (2009)
Z3: An Efficient SMT Solver (2008)
Houdini, an Annotation Assistant for ESC/Java (2001)
The octagon abstract domain (2001)
A dependently typed assembly language (2001)
From system F to typed assembly language (1999)
Proof-carrying code (1997)
Indexed types (1997)
TIL: a type-directed optimizing compiler for ML (1996)