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不会产生性能开销。