  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.
