用于安全漏洞推理的推测执行的抽象语义
An abstract semantics of speculative execution for reasoning about security vulnerabilities
摘要：
由于诸如乱序执行等现代微体系结构特征的复杂性，关于软件的正确性和安全性的推理变得越来越困难。一类名为Spectre的安全漏洞利用了投机性的副作用，乱序执行于2018年公布，此后引起了广泛关注。在本文中，我们正式的投机执行及其副作用的意图，让投机的推理抽象在程序级别，限制暴露于特定的处理器或低级别的语义。为此，我们编码和暴露的投机执行明确的程序设计语言，而不是仅仅在操作语义，因此，投机执行的影响被捕获的重新定义的含义的条件语句，并引入新的语言结构，模型瞬态执行的替代分支。我们在系统的全局状态中添加了一个抽象缓存，并推导出一些通用的细化规则，这些规则暴露了由于推测性负载而产生的缓存副作用。这个扩展的基础是一个基于指令级并行的语义模型。这些规则被编码在一个模拟工具中，我们用它来分析Spectre攻击的抽象规范和易受攻击的代码片段。
英文摘要：
Reasoning about correctness and security of software is increasingly difficult due to the complexity of modern microarchitectural features such as out-of-order execution. A class of security vulnerabilities termed Spectre that exploits side effects of speculative, out-of-order execution was announced in 2018 and has since drawn much attention. In this paper we formalise speculative execution and its side effects with the intention of allowing speculation to be reasoned about abstractly at the program level, limiting the exposure to processor-specific or low-level semantics. To this end we encode and expose speculative execution explicitly in the programming language, rather than solely in the operational semantics; as a result the effects of speculative execution are captured by redefining the meaning of a conditional statement, and introducing novel language constructs that model transient execution of an alternative branch. We add an abstract cache to the global state of the system, and derive some general refinement rules that expose cache side effects due to speculative loads. Underlying this extension is a semantic model that is based on instruction-level parallelism. The rules are encoded in a simulation tool, which we use to analyse an abstract specification of a Spectre attack and vulnerable code fragments.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
