Decompiling for Constant-Time Analysis

TL;DR

This work addresses the challenge of verifying constant-time security for binary programs via decompiled representations. It introduces CT transparency and ${\mathcal{PC}}$-injectivity to formalize when decompiler and subsequent analyses preserve CT properties, and proves CT transparency for several transformations while providing counterexamples for non-transparent ones. The authors build CT-RetDec, a CT analysis pipeline combining a modified RetDec with CT-LLVM, and demonstrate its effectiveness on a benchmark of compiler-induced CT vulnerabilities, including the Clangover case, while showing that non-transparent converters in CT-Verif and BinSec can yield unsound results. The findings emphasize the need for transparent transformations in CT analysis tools and offer practical guidance for implementing and evaluating CT transparency in decompilation pipelines. Overall, the work highlights a foundational security gap in current CT analysis workflows and provides a concrete method and tools to address it, with implications for secure compilation and vulnerability assessment in cryptographic software.

Abstract

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 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, rendering them not applicable with the approach. In this paper, we develop foundations to asses whether a decompiler is fit for the Decompile-then-Analyze approach. We propose CT transparency, which states that a transformation neither eliminates nor introduces CT violations, and a general method for proving that a program transformation is CT transparent. Then, we build CT-RetDec, a CT analysis tool based on a modified version of the LLVM-based decompiler RetDec. We evaluate CT-RetDec on a benchmark of real-world vulnerabilities in binaries, and show that the modifications had significant impact on CT-RetDec's performance. As a contribution of independent interest, we found that popular tools for binary-level CT analysis rely on decompiler-like transformations before analysis. We show that two such tools employ transformations that are not CT transparent, and, consequently, that they incorrectly accept non-CT programs. While our examples are very specific and do not invalidate the general approach of these tools, we advocate that tool developers counter such potential issues by proving the transparency of such transformations.

Figures (12)

• Figure 1: Decompiling Clangover removes the CT vulnerability.
• Figure 2: Multi-step execution semantics.
• Figure 3: Single-step execution semantics.
• Figure 4: Relaxed simulation instantiations of ${T}$, ${\mathsf{ns}}$, and ${\mathsf{sf}}$ for Dead Branch Elimination.
• Figure 5: Relaxed simulation instantiations of ${T}{}$, ${\mathsf{ns}}$, and ${\mathsf{sf}}$ for Dead Assignment Elimination.

Theorems & Definitions (18)

• Definition 1: Program Behavior
• Definition 2: ${{\mathphi}\text{-CT}}$
• Definition 3: Reflection, Preservation, and Transparency
• Definition 4: Lock-Step Simulation Diagram
• Theorem 1: Soundness of Lock-Step Simulations
• Definition 5: Simulation Diagram
• Definition 6: ${\mathcal{PC}}$-Injectivity
• Theorem 2: Soundness of Simulations
• Proposition 1
• Theorem 3