一句话：为 Wasm 引入语言级内存安全抽象，形式化证明良类型程序内存安全，并实现支持多种强制机制的编译器。
编译到 WebAssembly 的程序多由 C/C++ 等不安全语言编写，缓冲区溢出和 use-after-free 等漏洞在 Wasm 中同样可被利用。MSWasm 为 Wasm 引入语言级内存安全抽象。本文给出 MSWasm 的精确形式语义，提出基于“着色内存位置与指针”的语言无关内存安全性质，证明良类型程序具有鲁棒内存安全；并形式化 C-to-MSWasm 编译器，证明其总产生内存安全程序且保持安全程序语义。基于这些结果，作者实现两个 MSWasm 到原生代码的编译器和一个扩展 Clang 的 C-to-MSWasm 编译器，支持多种强制机制。在 PolyBenchC 上，软件强制执行内存安全开销为 22%（仅空间安全）到 198%（完整内存安全），用硬件内存能力实现空间安全和指针完整性时为 51.7%。
Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm—and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory- Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to precisely address this problem. In this paper, we build on the original MSWasm position paper to realize this vision. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler—and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Two compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). Our MSWasm compilers support different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs. Our evaluation shows that on the PolyBenchC suite, the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 51.7% when using hardware memory capabilities for spatial safety and pointer integrity. More importantly, MSWasm’s design makes it easy to swap between enforcement mechanisms; as fast (especially hardware-based) enforcement techniques become available, MSWasm will be able to take advantage of these advances almost for free.
@article{paperbot2107,
title = {MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code},
author = {Alexandra E. Michael and Anitha Gollamudi and Jay Bosamiya and Evan Johnson and Aidan Denlinger and Craig Disselkoen and Conrad Watt and Bryan Parno and Marco Patrignani and Marco Vassena and Deian Stefan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571208}
}