BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying Constant-Time Implementations - Francois Dupressoir
DTSTART:20160721T130000Z
DTEND:20160721T140000Z
UID:TALK66868@talks.cam.ac.uk
CONTACT:44515
DESCRIPTION:The constant-time programming discipline is an effective count
 ermeasure against timing and cache-timing attacks\, which can lead to comp
 lete breaks of otherwise secure systems. However\, adhering to it is hard\
 , especially under additional efficienty and legacy constraints. This make
 s automated verification of constant-time code an essential component for 
 building secure software.\n\nWe propose a novel approach\, based on the co
 nstruction of a selective product program\, for verifying constant-time se
 curity of real-world code\, including implementations that locally and int
 entionally violate strict constant-time when such violations are benign wi
 th respect to the desired security property. To illustrate the practicalit
 y of our approach\, we implement our approach in a fully automated prototy
 pe\, ct-verif\, that leverages the Smack and Boogie tools and verifies con
 stant-time properties of optimized LLVM code\, thereby removing the main p
 art of the compiler from the TCB for side-channel security. We present ver
 ification results obtained over a wide range of constant-time components\,
  from cryptographic (NaCl\, FourQLib\, OpenSSL\, ...) and non-cryptographi
 c (libfixedtimefixedpoint\, ...) off-the-shelf libraries.\n\nThis talk is 
 based on joint work with J. B. Almeida\, M. Barbosa\, G. Barthe and M. Emm
 i\, to appear at USENIX Security 2016.\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR