Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
复制标题
Iris-Wasm：WebAssembly 程序的稳健和模块化验证
DOI：
10.1145/3591265
复制
发表时间：
2023
影响因子：
--
通讯作者：
Rao X
中科院分区：
文献类型：
--
作者：
Rao X
WebAssembly使在Web上以接近本机的性能运行C/C++应用程序成为可能。WebAssembly程序被表示为高阶ML类模块的集合，这些模块通过使用宿主语言的显式导入和导出系统组合在一起，从而实现高阶模块化编程的形式。我们提出了Iris-Wasm，这是一种机械化的高阶分离逻辑，建立在Coq和Iris框架中机械化的Wasm 1.0规范之上。使用Iris-Wasm，我们能够单独指定和验证各个模块，然后用一种简单的主机语言将它们模块化，该语言具有WebAssembly JavaScript接口的核心操作。在Iris-Wasm的基础上，我们开发了一种逻辑关系，可以强制执行强大的安全性：未知的对抗性代码只能通过显式导出的函数影响其他模块。总之，程序逻辑和逻辑关系允许我们正式验证WebAssembly程序的功能正确性，即使它们被未知代码调用和调用，从而证明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.
登录
查看更多内容
无需纳税的隔离：WebAssembly 和 SFI 的近乎零成本转换
影响因子：
--
作者：
Kolosick, Matthew;Narayan, Shravan;Johnson, Evan;Watt, Conrad;LeMay, Michael;Garg, Deepak;Jhala, Ranjit;Stefan, Deian
通讯作者：
Stefan, Deian
Cerise：存在不可信代码的能力机器上的程序验证
影响因子：
2.5
作者：
Aïna Linn Georges;Armaël Guéneau;Thomas Van Strydonck;Amin Timany;Alix Trieu;Dominique Devriese;L. Birkedal
通讯作者：
L. Birkedal
RockSalt：针对 x86 的更好、更快、更强的 SFI
DOI：
10.1145/2254064.2254111
发表时间：
2012
期刊：
Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Greg Morrisett;Gang Tan;Joseph Tassarotti;Jean;Edward Gan
通讯作者：
Edward Gan
一阶封装 WebAssembly 的程序逻辑
DOI：
10.4230/lipics.ecoop.2019.9
发表时间：
2018
期刊：
Programming Languages and Systems
影响因子：
--
作者：
Conrad Watt;P. Maksimovic;N. Krishnaswami;Philippa Gardner
通讯作者：
Philippa Gardner
Diaframe：Iris 中细粒度并发程序的自动验证
DOI：
10.1145/3519939.3523432
发表时间：
2022
期刊：
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Ike Mulder;Robbert Krebbers;H. Geuvers
通讯作者：
H. Geuvers