ProSpeCT: Provably Secure Speculation for the Constant-Time Policy (Extended version)

Abstract

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.

arXiv commentTechnical report for our paper accepted at the 32nd USENIX Security Symposium (2023), 56 pages

References in corpus (7)

• ret2spec: Speculative Execution Using Return Stack Buffers
• A Systematic Evaluation of Transient Execution Attacks and Defenses
• Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level
• SafeSpec: Banishing the Spectre of a Meltdown with Leakage-Free Speculation
• KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution
• SpectreRewind: Leaking Secrets to Past Instructions
• SpecuSym: Speculative Symbolic Execution for Cache Timing Leak Detection