Constant-time foundations for the new spectre era

Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthal, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe

Research output: Chapter in Book / Report / Conference proceedingChapterAcademicpeer-review


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.
Original languageEnglish
Title of host publicationPLDI 2020
Subtitle of host publicationProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
Number of pages14
ISBN (Electronic)9781450376136
Publication statusPublished - Jun 2020


Dive into the research topics of 'Constant-time foundations for the new spectre era'. Together they form a unique fingerprint.

Cite this