无税隔离：SFI 的近零成本转换
密码学与安全
2021-11-19 v3
摘要
软件沙箱化或基于软件的故障隔离（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 系统 SegmentZero32 表明我们的模型在 Wasm 之外也有用，该系统使用 x86 分段和 LLVM（大多为现成 pass）来实施我们的零成本条件；我们的原型性能与最先进的 Native Client SFI 系统相当。
引用
@article{arxiv.2105.00033,
title = {Isolation Without Taxation: Near Zero Cost Transitions for 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= {arXiv preprint arXiv:2105.00033},
year = {2021}
}