一句话：提出 Iris-Wasm，在 Coq/Iris 中为 Wasm 1.0 建立高阶分离逻辑，支持模块化验证与鲁棒安全。
WebAssembly 程序由类 ML 的高阶模块经显式导入/导出组合而成，其模块化与宿主语言交互使功能正确性验证困难，尤其在面对未知对抗代码时。本文提出 Iris-Wasm：基于 Coq 中机器化的 Wasm 1.0 规范与 Iris 框架，构建高阶分离逻辑，支持分别指定和验证单个模块，并在含 WebAssembly JavaScript Interface 核心操作的宿主语言中模块化组合。作者进一步建立逻辑关系以刻画鲁棒安全：未知对抗代码只能通过模块显式导出的函数影响其他模块。该逻辑与逻辑关系可形式化验证在调用或被未知代码调用情况下的 Wasm 程序功能正确性，表明 WebAssembly 确实提供强模块隔离。
WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher- order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.
@article{paperbot1981,
title = {Iris-Wasm: Robust and Modular Verification of WebAssembly Programs},
author = {Xiaojia Rao and Aïna Linn Georges and Maxime Legoupil and Conrad Watt and Jean Pichon-Pharabod and Philippa Gardner and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591265}
}