When Obfuscations Preserve Cryptographic Constant-Time

Obfuscating compilers are designed to protect a program by obscuring its meaning and impeding the reconstruction of its original source code. Usually, the main concern with such compilers is their correctness and their robustness against reverse engineering. On the contrary, little attention is paid to ensure that obfuscation introduces no attacks in the transformed program that where not present in the original one. We are interested in checking whether a given obfuscation technique preserves the cryptographic constant-time property. Cryptographic libraries often resort to this property to guarantee that no attackers can learn any secret values by monitoring and analysing program execution time. Here, we propose a sufficient condition to prove if a given obfuscation preserves cryptographic constant-time. For transformations such that the condition does not hold for all possible programs, or the proof is too hard, we propose a translation validation procedure that applies our condition case by case.