Skip to Main content Skip to Navigation
Conference papers

Constant-Time Foundations for the New Spectre Era

Abstract : The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful. This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries.
Document type :
Conference papers
Complete list of metadata
Contributor : Tamara Rezk Connect in order to contact the contributor
Submitted on : Monday, February 15, 2021 - 11:29:25 AM
Last modification on : Friday, November 5, 2021 - 3:24:03 AM

Links full text


  • HAL Id : hal-03141383, version 1
  • ARXIV : 1910.01755



Sunjay Cauligi, Craig Disselkoen, Klaus Gleissenthall, Dean Tullsen, Deian Stefan, et al.. Constant-Time Foundations for the New Spectre Era. 2020 Programming Language Design and Implementation (PLDI'20), Jun 2020, London, United Kingdom. ⟨hal-03141383⟩



Les métriques sont temporairement indisponibles