Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees. This paper systematizes the community's current knowledge about software verification and mitigation for Spectre. We study state-of-the-art software defenses, both with and without associated formal models, and use a cohesive framework to compare the security properties each defense provides. We explore a wide variety of tradeoffs in the complexity of formal frameworks, the performance of defense tools, and the resulting security guarantees. As a result of our analysis, we suggest practical choices for developers of analysis and mitigation tools, and we identify several open problems in this area to guide future work on grounded software defenses.
翻译:光谱脆弱性违反了我们对建筑抽象学的基本假设,使攻击者可以窃取敏感数据,尽管此前是最先进的反措施。为了防御光谱,核查工具的开发者和基于编译者的缓解措施被迫解释微观建筑细节,例如投机性执行。为了以原则方式帮助开发者应对这些攻击,研究界为投机性执行寻求正式基础,以此重建可证实的安全保障。本文将社区目前关于软件核查和减轻监视器影响的知识系统化。我们研究的是最新的软件防御,无论是否相关的正式模型,并使用一个统一框架来比较每一项防御所提供的安全特性。我们探索了形式框架的复杂性、国防工具的性能以及由此产生的安全保障。我们的分析的结果是,我们为分析和缓解工具的开发者提出了切实可行的选择,我们找出了这方面的一些公开问题,以指导今后关于基础软件防御的工作。