University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Verifying Constant-Time Implementations

Verifying Constant-Time Implementations

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity