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.
In this paper, 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. Then, we leverage our foundations and additional empirical methods to build CT-RetDec, a CT analysis tool based on a modified version of the popular LLVM-based decompiler RetDec. We evaluate CT-RetDec on a benchmark set of real-world vulnerabilities in binaries, and show that the modifications had significant impact on how well CT-RetDec performs.
As a contribution of independent interest, we found that popular tools for binary-level CT analysis, which do not employ a decompiler explicitly, still rely on similar program transformations before analysis. We show that two such tools employ transformations that are not CT transparent, and, consequently, that the tools incorrectly accept non-CT programs. While our examples are very specific and do not invalidate the general approach of these tools for real-world code, we advocate that CT tool developers counter such potential issues by documenting and proving the transparency of the transformations used in their tools.
