Constant-time programming is an established discipline to secure programs against timing attacks. Several real-world secure C libraries such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We propose an advanced static analysis, based on state-of-the-art techniques from abstract interpretation, to report time leakage during programming. To that purpose, we analyze source C programs and use full context-sensitive and arithmetic-aware alias analyses to track the tainted flows.
We give semantic evidences of the correctness of our approach on a core language. We also present a prototype implementation for C programs that is based on the CompCert compiler toolchain and its companion Verasco static analyzer. We present verification results on various real-world constant-time programs and report on a successful verification of a challenging SHA-256 implementation that was out of scope of previous tool-assisted approaches.
The accompanying Coq development is available here. It contains modified versions of Verasco and crypto implementations from different libraries.
It requires Coq 8.4pl6 in order to be compiled. The easiest way to install Coq is to use opam.
In order to compile, please use ./configure and follow the instructions. make ccheck will then start compiling the analyzer. Please be aware that this may take around one hour.
In order to test the analyzer, please head to the test/taint/ folder and then use make all.