处理器RTL设计中瞬态执行边通道的穷举检测方法
An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors
摘要：
近年来，硬件（HW）安全问题以惊人的速度出现。特别是瞬态执行攻击，对现代计算系统的安全性构成了真正的威胁。尽管最近取得了进展，理解微架构设计决策对处理器安全性的复杂影响仍然是一个巨大的挑战，并在过去引起了一些更新周期。过去的更新周期数。本文讨论了需要一种新的方法来硬件签核验证，保证安全的处理器在寄存器传输级（RTL）。为此，我们引入了一个正式的定义，安全性方面的瞬态执行攻击，制定为HW属性。我们提出了一个形式化的证明方法，唯一程序执行检查（UPEC）的基础上，可用于系统地检测所有的RTL设计中的瞬态执行攻击的漏洞。UPEC不利用已知攻击的任何先验知识，因此也可以基于新的、迄今为止未知的信道类型来检测漏洞。这是证明了两个新的攻击场景中发现的实验与UPEC。UPEC可扩展到各种硬件设计，包括有序处理器（RocketChip），具有乱序写回的流水线（Ariane）和具有深度乱序推测执行的处理器（BOOM）。据我们所知，UPEC是第一个RTL验证技术，详尽地涵盖了现实复杂性的处理器中的瞬态执行侧通道。
英文摘要：
Hardware (HW) security issues have been emerging at an alarming rate in recent years. Transient execution attacks, in particular, pose a genuine threat to the security of modern computing systems. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on processor security remains a great challenge and has caused a number of update cycles in the past. number of update cycles in the past. This papers addresses the need for a new approach to HW sign-off verification which guarantees the security of processors at the Register Transfer Level (RTL). To this end, we introduce a formal definition of security with respect to transient execution attacks, formulated as a HW property. We present a formal proof methodology based on Unique Program Execution Checking (UPEC) which can be used to systematically detect all vulnerabilities to transient execution attacks in RTL designs. UPEC does not exploit any a priori knowledge on known attacks and can therefore detect also vulnerabilities based on new, so far unknown, types of channels. This is demonstrated by two new attack scenarios discovered in our experiments with UPEC. UPEC scales to a wide range of HW designs, including in-order processors (RocketChip), pipelines with out-of-order writeback (Ariane), and processors with deep out-of-order speculative execution (BOOM). To the best of our knowledge, UPEC is the first RTL verification technique that exhaustively covers transient execution side channels in processors of realistic complexity.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
