The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique for preventing the leakage of secret information through timing. It is based on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether or not an instruction satisfies this data-independent timing criterion varies between individual processor microarchitectures. In this paper, we propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. The proposed methodology is based on an inductive property that enables scalability even to complex out-of-order cores. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. In addition, the paper discusses several techniques that can be used to make the verification process easier and faster. We demonstrate the feasibility of the proposed methodology through case studies on several open-source designs. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core. In addition to several hardware accelerators and in-order processors, our experiments also include RISC-V BOOM, a complex out-of-order processor, highlighting the scalability of the approach.

翻译：近年来，防止安全关键应用中的微架构时间侧信道的重要性急剧上升。常数时间编程已成为防止通过时间泄漏秘密信息的最佳实践技术。它基于以下假设：某些基本机器指令的执行时间与其各自的输入数据无关。然而，指令是否满足这种数据无关时间标准因个别处理器微架构而异。在本文中，我们提出了一种新颖的方法，使用标准属性检查技术来形式化验证硬件中的数据无关行为。所提出的方法基于一种归纳属性，即使对于复杂的乱序处理器内核也能实现可扩展性。我们证明，证明该归纳属性足以在微架构级别穷举验证数据无关性。此外，本文讨论了几种可用于使验证过程更简单、更快速的技术。我们通过对多个开源设计进行案例研究来证明所提出方法的可行性。一个案例研究在经过了广泛验证且高度安全的IBEX RISC-V内核中发现了一个数据依赖的时间违规。除了多种硬件加速器和有序处理器外，我们的实验还包括RISC-V BOOM（一种复杂的乱序处理器），突显了该方法的高度可扩展性。