When obfuscations preserve 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. Cryptographic libraries often resort to the so-called cryptographic constant-time property to guarantee that no attackers can learn any secret values by monitoring and analyzing program execution time. Here, we propose a sufficient condition to check if a given obfuscation preserves the constant-time property. Checking this condition amounts to a simple and efficient static analysis that can be easily implemented. We consider several obfuscating transformations implemented in popular obfuscating compilers (e.g. the Tigress C compiler and O-MVLL). By relying on our condition we prove that some of them preserve constant-time, while others do not. For the last case we propose a translation validation procedure that applies our condition to the given program and verify whether instead the constant-time property is kept.