WaVe: a verifiably secure WebAssembly sandboxing runtime
WaVe: a verifiably secure WebAssembly sandboxing runtime
复制标题
DOI：
10.1109/sp46215.2023.10179357
复制
发表时间：
2023-05
期刊：
影响因子：
--
通讯作者：
Evan Johnson;Evan Laufer;Zijie Zhao;D. Gohman;Shravan Narayan;S. Savage;D. Stefan;Fraser Brown-Fraser-Brow
中科院分区：
文献类型：
--
作者：
Evan Johnson;Evan Laufer;Zijie Zhao;D. Gohman;Shravan Narayan;S. Savage;D. Stefan;Fraser Brown-Fraser-Brow
软件沙箱的承诺是灵活的，快速的和便携式的隔离；在不需要操作系统参与的情况下，捕获了基于硬件的内存保护。控制流程和控制流量确实是一个内存段，现代编译的WASM实现已经验证了这些检查本身可以验证这些检查，从而将编译器从可信赖的计算基础上删除。严格在WASM沙箱中执行。仍然允许此类程序与外界进行交互（即，与文件系统，网络等相互作用）。与WAVE的交互（包括OS副作用）不仅可以保持WASM的存储安全性保证，而且还保持了主机OS的存储和网络资源的访问隔离。提供现有工业（但不安全）的WASM运行时的性能竞争。
The promise of software sandboxing is flexible, fast and portable isolation; capturing the benefits of hardwarebased memory protection without requiring operating system involvement. This promise is reified in WebAssembly (Wasm), a popular portable bytecode whose compilers automatically insert runtime checks to ensure that data and control flow are constrained to a single memory segment. Indeed, modern compiled Wasm implementations have advanced to the point where these checks can themselves be verified, removing the compiler from the trusted computing base. However, the resulting integrity properties are only valid for code executing strictly inside the Wasm sandbox. Any interactions with the runtime system, which manages sandboxes and exposes the WebAssembly System Interface (WASI) used to access operating system resources, operate outside this contract. The resulting conundrum is how to maintain Wasm’s strong isolation properties while still allowing such programs to interact with the outside world (i.e., with the file system, the network, etc.). Our paper presents a solution to this problem, via WaVe, a verified secure runtime system that implements WASI. We mechanically verify that interactions with WaVe (including OS side effects) not only maintain Wasm’s memory safety guarantees, but also maintain access isolation for the host OS’s storage and network resources. Finally, in spite of completely removing the runtime from the trusted computing base, we show that WaVe offers performance competitive with existing industrial (yet unsafe) Wasm runtimes.