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 and by exhibiting a new, confirmed class of Spectre attacks based on alias prediction. Second, by implementing a static analysis tool, Blindfold, which detects violations of our extended constant-time property in real world cryptographic libraries.
Wed 15 JunDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 14:50 | |||
13:30 20mTalk | (OOPSLA 2021) Reconciling Optimization with Secure Compilation SIGPLAN Track Son Tuan Vu Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert Cohen Google, Arnaud de Grandmaison , Christophe Guillon STMicroelectronics, Karine Heydemann Sorbonne University; CNRS; LIP6 Link to publication DOI Authorizer link Pre-print | ||
13:50 20mTalk | (PLDI 2020) Constant-Time Foundations for the New Spectre Era SIGPLAN Track Sunjay Cauligi University of California at San Diego, USA, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, Tamara Rezk INRIA, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain | ||
14:10 20mTalk | (PLDI 2020) SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework SIGPLAN Track Sotiris Apostolakis Google, Ziyang Xu Princeton University, Zujun Tan Princeton University, USA, Greg Chan Princeton University, USA, Simone Campanoni Northwestern University, USA, David I. August Princeton University | ||
14:30 20mTalk | (POPL 2021) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade SIGPLAN Track Marco Vassena Utrecht University, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego; Amazon Web Services, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego | ||