Verifying Constant-Time Implementations

Опубликовано 1 августа 2016, 18:35

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.