Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter et al.
The CT programming discipline is commonly used to protect cryptographic libraries against side-channel attacks. However, it is hard to write CT code; moreover, compilers can introduce CT violations. Therefore, it is important to ensure that assembly code is CT. One approach is to show that source programs are CT, and that CT is preserved by compilation. In this paper, we explore the methodological soundness and scalability of the Decompile-then-Analyze (DtA) approach, a less conventional alternative that has been suggested in the broader setting of static analysis. Informally, the DtA approach uses decompilers a front-end for static analysis tools. As a motivation for our study, we show that current decompilers eliminate CT vulnerabilities before CT analysis, leading to non-CT programs being accepted as CT. Independently, we provide *constructed* examples of non-CT, exploitable, programs that are accepted by two popular CT analysis tools; in both cases the culprit are program transformations that are used internally prior to CT analysis and eliminate CT violations. While our examples do not invalidate the general approach of these tools, they emphasize the need for studying the DtA approach. On the methodological side, we define the notion of *CT transparency*. Informally, a program transformation is CT transparent if does not eliminate nor introduce CT violations. We also provide general methods for proving that a transformation is CT transparent, and show that several transformations of interest are transparent. We also sketch an extension of CT transparency to speculative CT, which is used by cryptographic software as a protection against Spectre attacks. On the practical side, we build a CT-transparent version of the popular LLVM-based decompiler RETDEC, and combine it with CT-LLVM, an existing CT verification...