一句话：为 MSWasm 建立机器化语义与 Iris 推理框架，证明其鲁棒能力安全。
WebAssembly 的模块系统只提供粗粒度封装，无法安全地细粒度共享线性内存。MSWasm 用句柄（保证时空安全的能力）扩展 WebAssembly 以支持灵活共享，但此前仅有纸面设计。本文对其进行形式验证：先定义 MSWasmCert，将 MSWasm 机器化为 WebAssembly 1.0 的完全定义且保守的扩展（含模块系统）；再提出 Iris-MSWasm，由推理已知代码的分离逻辑与推理未知对抗代码的逻辑关系组成，显式刻画 MSWasm 隐含契约中的鲁棒能力安全。作者将框架应用于关键句柄用例，证明调用未知函数的效果受鲁棒能力安全约束，为证明 MSWasm 程序复杂安全性质、评估其语言级保证提供基础。
WebAssembly offers coarse-grained encapsulation guarantees via its module system, but does not support fine-grained sharing of its linear memory. MSWasm is a recent proposal which extends WebAssembly with fine-grained memory sharing via handles, a type of capability that guarantees spatial and temporal safety, and thus enables an expressive yet safe style of programming with flexible sharing. In this paper, we formally validate the pen-and-paper design of MSWasm. To do so, we first define MSWasmCert, a mechanisation of MSWasm that makes it a fully-defined, conservative extension of WebAssembly 1.0, including the module system. We then develop Iris-MSWasm, a foundational reasoning framework for MSWasm composed of a separation logic to reason about known code, and a logical relation to reason about unknown, potentially adversarial code. Iris-MSWasm thereby makes explicit a key aspect of the implicit universal contract of MSWasm: robust capability safety. We apply Iris-MSWasm to reason about key use cases of handles, in which the effect of calling an unknown function is bounded by robust capability safety. Iris-MSWasm thus works as a framework to prove complex security properties of MSWasm programs, and provides a foundation to evaluate the language-level guarantees of MSWasm.
@article{LegoupilRGPB24,
title = {Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly},
author = {Maxime Legoupil and June Rousseau and Aïna Linn Georges and Jean Pichon-Pharabod and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689722}
}