Decompiling for Constant-Time Analysis

Basic Information

• Paper ID: 2501.04183
• Title: Decompiling for Constant-Time Analysis
• Authors: Santiago Arranz-Olmos (MPI-SP), Gilles Barthe (MPI-SP & IMDEA), Lionel Blatter (MPI-SP), Youcef Bouzid (ENS Paris-Saclay), Sören van der Wall (TU Braunschweig), Zhiyuan Zhang (MPI-SP)
• Classification: cs.PL (Programming Languages)
• Publication Date: January 2025 (arXiv preprint)
• Paper Link: https://arxiv.org/abs/2501.04183

Abstract

Cryptographic libraries are primary targets for timing side-channel attacks. A practical defense strategy against such attacks is to adhere to constant-time (CT) principles. However, writing constant-time code is difficult, and even constant-time source code may be transformed by mainstream compilers into vulnerable binary code. This paper investigates how to verify whether binary code satisfies constant-time requirements. A common approach is to use decompilers as a frontend to transform binary code into source code or intermediate representations, then apply existing CT analysis tools. Unfortunately, this "decompile-then-analyze" approach has fundamental problems. Through instances such as the Clangover vulnerability, this paper demonstrates that five popular decompilers eliminate CT violations, rendering analysis results unreliable.

Research Background and Motivation

Problem Background

1. Timing Side-Channel Attack Threats: Cryptographic implementations are vulnerable to timing side-channel attacks, where attackers can infer secret information by observing program execution time.
2. Constant-Time Strategy: CT strategy requires that program execution time be independent of secret inputs, including avoiding secret-dependent memory accesses and branch jumps.
3. Compiler Security Vulnerabilities: Optimizations in mainstream compilers may transform secure source code into binary code with CT violations.

Core Problem

The existing "decompile-then-analyze" approach has fundamental flaws: decompilers may eliminate CT violations during transformation, causing analysis tools to incorrectly classify vulnerable binary code as safe.

Research Motivation

1. Practical Necessity: Binary code CT analysis is needed, but existing tools primarily target source code.
2. Method Deficiency: Current approaches using decompilers as frontends are unreliable.
3. Theoretical Gap: Lack of a theoretical framework for evaluating whether program transformations are suitable for CT analysis.

Core Contributions

1. Problem Identification and Proof: Demonstrates through instances such as Clangover that five mainstream decompilers eliminate CT violations, rendering analysis results unreliable.
2. CT Transparency Theory: Formalizes the concept of CT transparency—program transformations that neither eliminate nor introduce CT violations.
3. Proof Techniques Development: Proposes a general simulation-based method to prove CT transparency of program transformations.
4. Practical Tool Development: Develops the CT-RetDec tool based on a modified RetDec decompiler for reliable binary CT analysis.
5. Tool Defect Discovery: Proves that transformations used internally by existing CT analysis tools (CT-Verif and BinSec) are also non-transparent, containing security vulnerabilities.

Methodology Details

Task Definition

Input: Binary program Output: CT analysis result (safe/unsafe) Constraint: Analysis results must accurately reflect the actual CT properties of the binary program.

Theoretical Framework

CT Transparency Definition

For program transformation $\llbracket \cdot \rrbracket : L_s \to L_t$, three properties are defined:

1. Reflection: If $\llbracket P \rrbracket$ is φ-CT, then P is φ-CT
2. Preservation: If P is φ-CT, then $\llbracket P \rrbracket$ is φ-CT
3. Transparency: Simultaneously satisfies both reflection and preservation

Simulation Techniques

Two simulation methods are employed:

Lock-Step Simulation: Each step of the output program corresponds to one step of the input program

• Simulation relation: $s \sim t$
• Observation transformer: $T : O_s \to O_t$
• Key condition: T must be injective

Relaxed Simulation: Allows input and output programs to execute different numbers of steps

• Step function: $ns : PC \to \mathbb{N}_{>0}$
• Suffix function: $sf : PC \to O_s^*$
• PC injectivity: For each program point, the observation transformer must be injective

Technical Innovations

1. PC Injectivity Concept: Extends existing CT preservation techniques by requiring the observation transformer to be injective at each program point to ensure reflection.
2. Unified Framework: Analyzes multiple program transformations under a single theoretical framework.
3. Practical Orientation: Provides not only theoretical analysis but also practically usable tools.

Experimental Setup

Dataset

1. Decompiler Testing: Tests five decompilers using Clangover vulnerability and constructed minimal counterexamples.
2. Benchmark Suite: 160 binary programs containing 10 known timing side-channel vulnerabilities
   • Compilers: Clang 10/14/18/21
   • Optimization levels: -O0, -Os
   • Architectures: x86-32, x86-64

Evaluation Metrics

• Accuracy: Correct identification of CT violations
• Completeness: No missed real vulnerabilities
• False Positive Rate: No misclassification of safe code as unsafe

Comparison Methods

• Original RetDec + CT-LLVM
• CT-RetDec (modified version)
• Manual analysis as ground truth

Implementation Details

• Disabled 10 non-transparent optimization passes in RetDec
• Retained 52 passes, 7 of which are theoretically proven transparent
• Used CT-LLVM for final CT analysis

Experimental Results

Main Results

Decompiler Transparency Testing

All five tested decompilers eliminate certain CT violations:

CT-RetDec Performance Evaluation

On 160 benchmark programs:

• Accuracy: 100% (no false positives, no false negatives)
• Original RetDec: Misses most CT violations
• Improvement Effect: Significantly enhances CT analysis reliability

Program Transformation Analysis

Analyzes transparency of 10 common program transformations:

Transparent Transformations (7 types):

• Expression substitution (constant folding, inlining, etc.)
• Dead branch elimination
• Dead assignment elimination
• Anti-overflow optimization
• Structural analysis
• Loop rotation

Non-Transparent Transformations (3 types):

• Branch coalescing
• If-conversion
• Memory access elimination

Tool Vulnerability Discovery

Discovers security vulnerabilities in CT-Verif and BinSec tools:

• CT-Verif: SMACK transformer eliminates dead loads, causing acceptance of non-CT programs
• BinSec: DBA lifting process merges empty branches, eliminating CT violations

Related Work

Side-Channel Analysis

Existing CT analysis tools are primarily based on:

• Product program construction (CT-Verif)
• Type systems (Jasmin)
• SMT solvers (Vale)
• Abstract interpretation (Blazy et al.)
• Symbolic execution (BinSec)

Secure Compilation

Related research focuses on how compilers preserve security properties:

• CT simulation techniques (Barthe et al.)
• Leakage transformer methods
• CT preservation proofs in Jasmin and CompCert compilers

Decompilation Correctness

Existing work primarily addresses functional correctness, with limited consideration of security property preservation.

Conclusions and Discussion

Main Conclusions

1. Problem Prevalence: Mainstream decompilers universally exhibit CT transparency issues.
2. Theoretical Necessity: Formal theory is needed to evaluate and ensure transparency of program transformations.
3. Practical Feasibility: Reliable binary CT analysis tools can be constructed through theory-guided approaches.
4. Tool Defects: Existing CT analysis tools themselves contain transparency issues.

Limitations

1. Coverage Scope: Only analyzes basic CT strategies; does not address decryption and refined leakage models.
2. Transformation Types: Theoretical analysis covers only 10 common transformations; RetDec contains 62 passes.
3. Implementation Defects: Even theoretically transparent transformations may contain bugs in implementation.

Future Directions

1. Theory Extension: Support more complex security properties and leakage models.
2. Automated Verification: Develop tools for automatically verifying transformation transparency.
3. Compiler Improvement: Integrate transparency requirements into compiler design.

In-Depth Evaluation

Strengths

1. Problem Importance: Addresses critical issues in practical security analysis.
2. Theoretical Contribution: Proposes a complete CT transparency theoretical framework.
3. Sufficient Empirical Evidence: Validates theory through multiple instances and benchmark tests.
4. Practical Value: Develops usable tools and discovers vulnerabilities in existing tools.
5. Formal Rigor: Provides Coq mechanized proofs.

Weaknesses

1. Theory Coverage: Analyzes only partial program transformation types.
2. Experiment Scale: Benchmark suite contains real vulnerabilities but is relatively limited in scale.
3. Tool Maturity: CT-RetDec still relies on empirical methods to disable certain passes.

Impact

1. Academic Value: Provides new theoretical framework for security analysis of program transformations.
2. Practical Significance: Directly influences security analysis practices for cryptographic software.
3. Tool Impact: Discovered tool vulnerabilities will promote improvements in related tools.

Applicable Scenarios

1. Cryptographic Software Analysis: Suitable for scenarios requiring CT analysis of binary cryptographic implementations.
2. Compiler Development: Provides theoretical foundation for compiler optimization security verification.
3. Security Tool Development: Guides development of reliable binary security analysis tools.

References

The paper cites 61 related references covering multiple domains including side-channel analysis, secure compilation, and decompilation techniques, providing a solid theoretical foundation for the research.