一句话：提出 Wasm-precheck，用索引类型静态检查程序值约束，从而安全移除 Wasm 的动态安全检查。
WebAssembly（Wasm）依赖动态安全检查（如内存边界检查）来保证安全，但带来运行时开销。本文提出 Wasm-precheck：Wasm 的一个超集，用索引类型（indexed types）表达并检查程序值的简单约束，使得编译器可以静态地、安全地删除这些动态检查。作者将 Wasm-precheck 实现为 Wasmtime 编译器与运行时的扩展，并与带显式动态检查的 Wasm 配置进行运行时与编译时性能对比：在广泛使用的 PolyBenchC 基准上平均运行时性能提升 1.71 倍，代价是二进制体积增加 7.18%、类型检查时间慢 1.4%。作者还证明了 Wasm-precheck 的类型安全与内存安全，证明 Wasm 可安全嵌入 Wasm-precheck（保证向后兼容），证明 Wasm-precheck 可类型擦除到 Wasm，并讨论了设计与实现上的权衡。
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.
@article{paperbot2624,
title = {Indexed Types for a Statically Safe WebAssembly},
author = {Adam T. Geller and Justine Frank and William J. Bowman},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632922}
}