Verifying Constant-Time Implementations

Add to your list(s) Download to your calendar using vCal

• Francois Dupressoir
• Thursday 21 July 2016, 14:00-15:00
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact lecturescam.

Please note, this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

The constant-time programming discipline is an effective countermeasure against timing and cache-timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to it is hard, especially under additional efficienty and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software.

We propose a novel approach, based on the construction of a selective product program, for verifying constant-time security of real-world code, including implementations that locally and intentionally violate strict constant-time when such violations are benign with respect to the desired security property. To illustrate the practicality of our approach, we implement our approach in a fully automated prototype, ct-verif, that leverages the Smack and Boogie tools and verifies constant-time properties of optimized LLVM code, thereby removing the main part of the compiler from the TCB for side-channel security. We present verification results obtained over a wide range of constant-time components, from cryptographic (NaCl, FourQLib, OpenSSL, ...) and non-cryptographic (libfixedtimefixedpoint, ...) off-the-shelf libraries.

This talk is based on joint work with J. B. Almeida, M. Barbosa, G. Barthe and M. Emmi, to appear at USENIX Security 2016.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.