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.
Fri 19 Jun Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change
|13:00 - 13:20|
Sunjay CauligiUniversity of California at San Diego, USA, Craig DisselkoenUniversity of California at San Diego, USA, Klaus v. GleissenthallUniversity of California at San Diego, USA, Dean TullsenUniversity of California at San Diego, USA, Deian StefanUniversity of California at San Diego, USA, Tamara RezkInria, France, Gilles BartheMPI for Security and Privacy, Germany / IMDEA Software Institute, Spain
|13:20 - 13:40|
José Fragoso SantosINESC-ID/Instituto Superior Técnico, Portugal , Petar MaksimovićImperial College London, UK, Sacha-Élie AyounImperial College London, UK, Philippa GardnerImperial College London, UKDOI
|13:40 - 14:00|
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Yu-Fang ChenAcademia Sinica, Taiwan, Bui Phi DiepUppsala University, Sweden, Julian DolbyIBM Research, USA, Petr JankůBrno University of Technology, Czechia, Hsin-Hung LinAcademia Sinica, Taiwan, Lukáš HolíkBrno University of Technology, Czechia, Wei-Cheng WuUniversity of Southern California, USA