We propose ProSpeCT, a generic formal processor model providing provably secure speculation for the constant-time policy. For constant-time programs under a non-speculative semantics, ProSpeCT guarantees that speculative and out-of-order execution cause no microarchitectural leaks. This guarantee is achieved by tracking secrets in the processor pipeline and ensuring that they do not influence the microarchitectural state during speculative execution. Our formalization covers a broad class of speculation mechanisms, generalizing prior work. As a result, our security proof covers all known Spectre attacks, including load value injection (LVI) attacks. In addition to the formal model, we provide a prototype hardware implementation of ProSpeCT on a RISC-V processor and show evidence of its low impact on hardware cost, performance, and required software changes. In particular, the experimental evaluation confirms our expectation that for a compliant constant-time binary, enabling ProSpeCT incurs no performance overhead.

翻译：我们提出ProSpeCT，一种通用的形式化处理器模型，可为常量时间策略提供可证明安全的推测执行。对于在非推测语义下的常量时间程序，ProSpeCT保证推测执行和乱序执行不会引发微架构泄漏。该保证通过在处理器流水线中追踪秘密信息，并确保其在推测执行期间不会影响微架构状态来实现。我们的形式化框架覆盖了广泛的推测机制，拓展了先前工作。因此，我们的安全性证明涵盖了所有已知的Spectre攻击，包括负载值注入攻击。除形式化模型外，我们还在RISC-V处理器上提供了ProSpeCT的原型硬件实现，并证明其对硬件成本、性能及所需软件变更的影响较低。特别地，实验评估证实了我们的预期：对于符合规范的常量时间二进制程序，启用ProSpeCT不会产生性能开销。