Cryptographic libraries are a main target of timing side-channel attacks. A practical means to protect against these attacks is to adhere to the constant-time (CT) policy. However, it is hard to write constant-time code, and even constant-time code can be turned vulnerable by mainstream compilers. So how can we verify that binary code is constant-time? The obvious answer is to use binary-level CT tools. To do so, a common approach is to use decompilers or lifters as a front-end for CT analysis tools operating on source code or IR@. Unfortunately, this Decompile-then-Analyze approach is problematic with current decompilers. To illustrate this fact, we use the recent Clangover vulnerability and other constructed examples to show that five popular decompilers eliminate CT violations, making them unsound to be used as front-ends to the approach.

We formalize and develop foundations to asses whether a decompiler is fit for the Decompile-then-Analyze approach. We propose the property of CT transparency, which states that a transformation neither eliminates nor introduces CT violations. We also present a general method for proving that a program transformation is CT transparent.