  This paper tackles the problem of designing efficient binary-level
verification for a subset of information flow properties encompassing
constant-time and secret-erasure. These properties are crucial for
cryptographic implementations, but are generally not preserved by compilers.
Our proposal builds on relational symbolic execution enhanced with new
optimizations dedicated to information flow and binary-level analysis, yielding
a dramatic improvement over prior work based on symbolic execution. We
implement a prototype, Binsec/Rel, for bug-finding and bounded-verification of
constant-time and secret-erasure, and perform extensive experiments on a set of
338 cryptographic implementations, demonstrating the benefits of our approach.
Using Binsec/Rel, we also automate two prior manual studies on preservation of
constant-time and secret-erasure by compilers for a total of 4148 and 1156
binaries respectively. Interestingly, our analysis highlights incorrect usages
of volatile data pointer for secret erasure and shows that scrubbing mechanisms
based on volatile function pointers can introduce additional register spilling
which might break secret-erasure. We also discovered that gcc -O0 and backend
passes of clang introduce violations of constant-time in implementations that
were previously deemed secure by a state-of-the-art constant-time verification
tool operating at LLVM level, showing the importance of reasoning at
binary-level.
