Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI
复制标题
无需纳税的隔离：WebAssembly 和 SFI 的近乎零成本转换
DOI：
10.1145/3498688
复制
发表时间：
2022
影响因子：
--
通讯作者：
Stefan, Deian
中科院分区：
文献类型：
--
作者：
Kolosick, Matthew;Narayan, Shravan;Johnson, Evan;Watt, Conrad;LeMay, Michael;Garg, Deepak;Jhala, Ranjit;Stefan, Deian
软件沙箱或基于软件的故障隔离（SFI）是一种轻量级的方法，用于从不受信任的组件中构建安全系统。例如，Mozilla使用SFI通过对第三方库进行沙箱化来强化Firefox浏览器，Fastly和Cloudflare等公司使用SFI在其边缘云上安全地共同定位不受信任的租户。虽然已经做出了重大努力来优化和验证SFI实施，但SFI系统中的上下文切换在很大程度上仍未被探索：几乎所有的SFI系统都使用重量级转换，这些转换不仅容易出错，而且在上下文切换时从保存，清除和恢复寄存器中产生显着的性能开销。我们确定了一组零成本条件，这些条件表征了沙箱代码何时具有足够的结构，以通过轻量级零成本转换（简单的函数调用）来保证安全性。我们修改了Lucet Wasm编译器及其运行时，以使用零成本转换，消除了依赖Lucet进行沙盒的系统上不适当的性能负担（例如，在Firefox中，我们将图像和字体渲染速度分别提高了29.7%和10%）。为了将Lucet编译器及其对Wasm规范的正确实现从可信计算基础中移除，我们（1）开发了静态二进制验证器VeriZero，（以秒为单位）检查Lucet生成的二进制文件是否满足我们的零成本条件，以及（2）通过开发一个逻辑关系来证明VeriZero的可靠性，该逻辑关系可以捕获编译后的Wasm函数何时相对于我们的零在语义上表现良好-成本条件。最后，我们通过描述一个新的专用SFI系统SegmentZero 32来证明我们的模型在Wasm之外是有用的，该系统使用x86分段和LLVM，大部分是现成的通行证来执行我们的零成本条件;我们的原型与最先进的Native Client SFI系统不相上下。
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 useheavyweight transitionsthat are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set ofzero-cost conditionsthat characterize when sandboxed code has sufficient structured to guarantee security via lightweightzero-costtransitions (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 astatic 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.
登录
查看更多内容
编译沙箱：经过正式验证的软件故障隔离
影响因子：
--
作者：
Frédéric Besson;Sandrine Blazy;Alexandre Dang;T. Jensen;Pierre Wilke
通讯作者：
Pierre Wilke
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
设备驱动程序的故障隔离
DOI：
10.1109/dsn.2009.5270357
发表时间：
2009
期刊：
2009 IEEE/IFIP International Conference on Dependable Systems & Networks
影响因子：
--
作者：
J. Herder;H. Bos;Ben Gras;P. Homburg;A. Tanenbaum
通讯作者：
A. Tanenbaum
DOI：
--
发表时间：
2010
期刊：
--
影响因子：
--
作者：
A. Mettler;D. Wagner;T. Close
通讯作者：
A. Mettler;D. Wagner;T. Close
便携式软件故障隔离
DOI：
10.1109/csf.2014.10
发表时间：
2014
期刊：
2014 IEEE 27th Computer Security Foundations Symposium
影响因子：
--
作者：
Joshua A. Kroll;Gordon Stewart;A. Appel
通讯作者：
A. Appel