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.
翻译:近年来出现了惊人的复杂程度的硬件(HW)安全问题,特别是中转性执行攻击对现代计算系统的安全构成真正的威胁。尽管最近取得了一些进展,但了解微分构设计决定对过程安全产生的复杂影响仍然是一项巨大挑战,并在过去导致了一系列更新周期。过去更新周期的数量。这些文件谈到对HW签定核查采取新办法的必要性,这保证了登记册实际转移级别(TRL)处理者的安全。为此,我们引入了暂时性执行攻击安全的正式定义,该定义是HW财产。我们根据UPEC执行特殊方案检查(UPEC)提出一种正式的证明方法,可以用来系统检测在RTL设计中进行临时执行攻击的所有弱点。UPEC没有利用关于已知攻击的任何事先知识,因此也能够根据新的、非常不为人所知的渠道类型探测脆弱性。我们与UPEC试验中发现的两种新的攻击情景证明了这一点。 UPEC规模的大规模执行执行执行执行行动,其范围是广泛的HW设计,包括机检过程的技术性执行(ROM ) 和机检程序(RO-R) 外执行过程(Rotorial-tracal-tracers)。