论文标题
经过验证的幽灵沙箱的转折点
A Turning Point for Verified Spectre Sandboxing
论文作者
论文摘要
幽灵攻击使攻击者能够访问应用程序内存中的限制数据。学术界和行业退伍军人都已经开发了几种缓解措施来阻止幽灵攻击，但迄今为止，很少有人被正式审查。大多数是“最佳努力”策略。正式的保证对于保护诸如沙箱之类的隔离环境（防止幽灵攻击）尤其至关重要。在这样的环境中，缓解措施中的细微缺陷将使不信任的代码可以脱离沙箱并访问可信赖的内存区域。 在我们的工作中，我们开发了有原则的基础，以建立抵抗幽灵攻击的孤立环境。我们提出了一个正式的框架，用于推理沙箱执行和幽灵攻击。我们将声音缓解策略必须实现的属性形式化，我们展示了各种现有缓解措施如何满足（或不满足！）这些属性。
Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most are "best effort" strategies. Formal guarantees are particularly crucial for protecting isolated environments like sandboxing against Spectre attacks. In such environments, a subtle flaw in the mitigation would allow untrusted code to break out of the sandbox and access trusted memory regions. In our work, we develop principled foundations to build isolated environments resistant against Spectre attacks. We propose a formal framework for reasoning about sandbox execution and Spectre attacks. We formalize properties that sound mitigation strategies must fulfill and we show how various existing mitigations satisfy (or fail to satisfy!) these properties.
