一句话：提出零成本转换条件，改造 Lucet Wasm 运行时并构建静态验证器 VeriZero，在保证 SFI 安全的同时消除上下文切换开销。
软件故障隔离（SFI）用沙箱隔离不可信组件，但其上下文切换普遍采用重量级转换：保存、清空和恢复寄存器不仅易错，还带来显著性能开销。本文识别出一组零成本条件，刻画沙箱代码何时具有足够结构，可用简单函数调用实现安全的近零成本转换。作者修改 Lucet Wasm 编译器与运行时以采用零成本转换，使 Firefox 图像和字体渲染分别最高加速 29.7% 与 10%。为将 Lucet 编译器移出可信计算基，作者开发静态二进制验证器 VeriZero，秒级检查 Lucet 生成的二进制是否满足零成本条件，并用逻辑关系证明其可靠性；还构建 SegmentZero32，性能与 Native Client 相当。
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimize and verify SFI enforcement, context switching in SFI systems remains largely unexplored: almost all SFI systems use heavyweight transitions that are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set of zero-cost conditions that characterize when sandboxed code has sufficient structured to guarantee security via lightweight zero-cost transitions (simple function calls). We modify the Lucet Wasm compiler and its runtime to use zero-cost transitions, eliminating the undue performance tax on systems that rely on Lucet for sandboxing (e.g., we speed up image and font rendering in Firefox by up to 29.7% and 10% respectively). To remove the Lucet compiler and its correct implementation of the Wasm specification from the trusted computing base, we (1) develop a static binary verifier , VeriZero, which (in seconds) checks that binaries produced by Lucet satisfy our zero-cost conditions, and (2) prove the soundness of VeriZero by developing a logical relation that captures when a compiled Wasm function is semantically well-behaved with respect to our zero-cost conditions. Finally, we show that our model is useful beyond Wasm by describing a new, purpose-built SFI system, SegmentZero32, that uses x86 segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-cost conditions; our prototype performs on-par with the state-of-the-art Native Client SFI system.
@article{paperbot1543,
title = {Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI},
author = {Matthew Kolosick and Shravan Narayan and Evan Johnson and Conrad Watt and Michael LeMay and Deepak Garg and Ranjit Jhala and Deian Stefan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498688}
}