2025-11-10T03:00:57.254697

Decompiling for Constant-Time Analysis

Arranz-Olmos, Barthe, Blatter et al.

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.

academic

Dekompilierung zur Analyse konstanter Ausführungszeit

Grundinformationen

Papier-ID: 2501.04183
Titel: Decompiling for Constant-Time Analysis
Autoren: 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)
Klassifizierung: cs.PL (Programmiersprachen)
Veröffentlichungsdatum: Januar 2025 (arXiv-Preprint)
Papierlink: https://arxiv.org/abs/2501.04183

Zusammenfassung

Kryptographische Bibliotheken sind primäre Ziele von Timing-Seitenkanalangriffen. Eine praktische Verteidigungsmethode gegen solche Angriffe ist die Einhaltung einer Strategie für konstante Ausführungszeit (CT). Das Schreiben von Code mit konstanter Ausführungszeit ist jedoch schwierig, und selbst CT-konformer Quellcode kann von modernen Compilern in anfällige Binärdateien transformiert werden. Dieses Papier untersucht, wie man überprüft, ob Binärcode die Anforderungen konstanter Ausführungszeit erfüllt. Ein häufiger Ansatz besteht darin, Dekompiler als Frontend zu verwenden, um Binärcode in Quellcode oder Zwischendarstellung umzuwandeln und dann bestehende CT-Analysewerkzeuge anzuwenden. Leider weist dieser „Dekompilierungs-Analyse"-Ansatz Probleme auf. Dieses Papier zeigt durch Beispiele wie die Clangover-Schwachstelle, dass fünf beliebte Dekompiler CT-Verstöße eliminieren, was zu unzuverlässigen Analyseergebnissen führt.

Forschungshintergrund und Motivation

Problemhintergrund

Bedrohung durch Timing-Seitenkanalangriffe: Kryptographische Implementierungen sind anfällig für Timing-Seitenkanalangriffe, bei denen Angreifer durch Beobachtung der Programmausführungszeit geheime Informationen ableiten können
Strategie für konstante Ausführungszeit: Die CT-Strategie erfordert, dass die Programmausführungszeit nicht von geheimen Eingaben abhängt, einschließlich der Vermeidung von geheimen Speicherzugriffen und bedingten Sprüngen
Compiler-Sicherheitslücken: Optimierungen moderner Compiler können sicheren Quellcode in Binärdateien mit CT-Verstößen transformieren

Kernproblem

Der bestehende „Dekompilierungs-Analyse"-Ansatz weist einen grundlegenden Fehler auf: Dekompiler können CT-Verstöße während der Transformation eliminieren, was dazu führt, dass Analysewerkzeuge fälschlicherweise annehmen, dass anfällige Binärdateien sicher sind.

Forschungsmotivation

Praktischer Bedarf: CT-Analyse von Binärcode ist erforderlich, aber bestehende Werkzeuge konzentrieren sich hauptsächlich auf Quellcode
Methodenmängel: Der aktuelle Ansatz mit Dekompilern als Frontend ist unzuverlässig
Theoretische Lücke: Es fehlt ein theoretischer Rahmen zur Bewertung, ob Programmtransformationen für CT-Analyse geeignet sind

Kernbeiträge

Problemidentifikation und -nachweis: Durch Beispiele wie Clangover wird nachgewiesen, dass fünf führende Dekompiler CT-Verstöße eliminieren, was zu unzuverlässigen Analyseergebnissen führt
CT-Transparenztheorie: Formale Definition des CT-Transparenzkonzepts, d.h. Programmtransformationen, die weder CT-Verstöße eliminieren noch einführen
Beweistechniken: Vorschlag einer simulationsbasierten allgemeinen Methode zum Nachweis der CT-Transparenz von Programmtransformationen
Praktisches Werkzeug: Entwicklung des CT-RetDec-Werkzeugs basierend auf einem modifizierten RetDec-Dekompiler für zuverlässige binäre CT-Analyse
Werkzeugmängel: Nachweis, dass interne Transformationen bestehender CT-Analysewerkzeuge (CT-Verif und BinSec) ebenfalls nicht transparent sind und Sicherheitslücken aufweisen

Methodische Details

Aufgabendefinition

Eingabe: Binärprogramm Ausgabe: CT-Analyseergebnis (sicher/unsicher) Einschränkung: Das Analyseergebnis muss die tatsächlichen CT-Eigenschaften des Binärprogramms genau widerspiegeln

Theoretischer Rahmen

CT-Transparenzdefinition

Für eine Programmtransformation $\llbracket \cdot \rrbracket : L_s \to L_t$ werden drei Eigenschaften definiert:

Reflexivität (Reflection): Wenn $\llbracket P \rrbracket$ φ-CT ist, dann ist P φ-CT
Bewahrung (Preservation): Wenn P φ-CT ist, dann ist $\llbracket P \rrbracket$ φ-CT
Transparenz (Transparency): Erfüllt gleichzeitig Reflexivität und Bewahrung

Simulationstechniken

Zwei Methoden werden verwendet: Lockstep-Simulation und gelockerte Simulation:

Lockstep-Simulation: Jeder Schritt des Ausgabeprogramms entspricht einem Schritt des Eingabeprogramms

Simulationsrelation: $s \sim t$
Beobachtungstransformer: $T : O_s \to O_t$
Schlüsselbedingung: T muss injektiv sein

Gelockerte Simulation: Erlaubt unterschiedliche Ausführungsschritte für Ein- und Ausgabeprogramme

Schrittfunktion: $ns : PC \to \mathbb{N}_{>0}$
Suffixfunktion: $sf : PC \to O_s^*$
PC-Injektivität: Für jeden Programmpunkt muss der Beobachtungstransformer injektiv sein

Technische Innovationen

PC-Injektivitätskonzept: Erweitert bestehende CT-Bewahrungstechniken durch Forderung nach Injektivität des Beobachtungstransformers an jedem Programmpunkt
Einheitlicher Rahmen: Vereinigt mehrere Programmtransformationen unter einem theoretischen Rahmen
Praktische Ausrichtung: Bietet nicht nur theoretische Analyse, sondern entwickelt auch praktisch einsetzbare Werkzeuge

Experimentelle Einrichtung

Datensätze

Dekompiler-Tests: Verwendung der Clangover-Schwachstelle und konstruierter minimaler Gegenbeispiele zum Testen von 5 Dekompilern
Benchmark-Suite: 160 Binärprogramme mit 10 bekannten Timing-Seitenkanalvulnerabilitäten
- Compiler: Clang 10/14/18/21
- Optimierungsstufen: -O0, -Os
- Architekturen: x86-32, x86-64

Bewertungsmetriken

Genauigkeit: Korrekte Identifikation von CT-Verstößen
Vollständigkeit: Keine echten Schwachstellen übersehen
Falsch-Positiv-Rate: Sichere Codes nicht als unsicher kennzeichnen

Vergleichsmethoden

Original RetDec + CT-LLVM
CT-RetDec (modifizierte Version)
Manuelle Analyse als Grundwahrheit

Implementierungsdetails

Deaktivierung von 10 nicht-transparenten Optimierungs-Passes in RetDec
Beibehaltung von 52 Passes, von denen 7 theoretisch transparent nachgewiesen sind
Verwendung von CT-LLVM für die endgültige CT-Analyse

Experimentelle Ergebnisse

Hauptergebnisse

Dekompiler-Transparenztests

Alle 5 getesteten Dekompiler eliminieren bestimmte CT-Verstöße:

Dekompiler	Clangover	Branch Coalescing	Empty Branch	Dead Load	Dead Store
Angr	✗	✗	-	✗	-
BinaryNinja	-	✗	✗	✗	✗
Ghidra	-	-	✗	✗	-
Hex-Rays	-	✗	✗	✗	-
RetDec	✗	✗	✗	✗	✗

CT-RetDec-Leistungsbewertung

Auf 160 Benchmark-Programmen:

Genauigkeit: 100% (keine Falsch-Positive, keine Falsch-Negative)
Original RetDec: Übersieht die meisten CT-Verstöße
Verbesserungseffekt: Signifikante Verbesserung der Zuverlässigkeit der CT-Analyse

Programmtransformationsanalyse

Analyse der Transparenz von 10 häufigen Programmtransformationen:

Transparente Transformationen (7):

Ausdrucksersetzung (Konstantenfaltung, Inlining usw.)
Elimination toter Branches
Elimination toter Zuweisungen
Anti-Overflow-Optimierung
Strukturierte Analyse
Schleifenrotation

Nicht-transparente Transformationen (3):

Branch-Zusammenführung
If-Konvertierung
Speicherzugriffselimination

Werkzeugmängel-Entdeckung

Entdeckung von Sicherheitslücken in CT-Verif und BinSec:

CT-Verif: Der SMACK-Transformer eliminiert Dead Loads, was zur Akzeptanz von nicht-CT-Programmen führt
BinSec: Der DBA-Lifting-Prozess führt leere Branches zusammen und eliminiert CT-Verstöße

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

Universalität des Problems: Führende Dekompiler weisen weit verbreitete CT-Transparenzprobleme auf
Theoretische Notwendigkeit: Ein formaler theoretischer Rahmen ist erforderlich, um die Transparenz von Programmtransformationen zu bewerten und zu gewährleisten
Praktische Machbarkeit: Durch theoretische Anleitung können zuverlässige binäre CT-Analysewerkzeuge konstruiert werden
Werkzeugmängel: Bestehende CT-Analysewerkzeuge weisen selbst Transparenzprobleme auf

Einschränkungen

Abdeckungsbereich: Nur grundlegende CT-Strategien analysiert, keine Entschlüsselung oder verfeinerte Leak-Modelle berücksichtigt
Transformationstypen: Theoretische Analyse deckt nur 10 häufige Transformationen ab, RetDec enthält 62 Passes
Implementierungsmängel: Selbst theoretisch transparente Transformationen können Implementierungsfehler aufweisen

Zukünftige Richtungen

Theoretische Erweiterung: Unterstützung komplexerer Sicherheitseigenschaften und Leak-Modelle
Automatisierte Verifikation: Entwicklung von Werkzeugen zur automatisierten Verifikation der Transformationstransparenz
Compiler-Verbesserung: Integration von Transparenzanforderungen in das Compiler-Design

Tiefgreifende Bewertung

Stärken

Problemrelevanz: Löst kritische Probleme in der praktischen Sicherheitsanalyse
Theoretischer Beitrag: Bietet einen umfassenden theoretischen Rahmen für CT-Transparenz
Ausreichende empirische Evidenz: Verifiziert die Theorie durch mehrere Beispiele und Benchmark-Tests
Praktischer Wert: Entwickelt einsetzbare Werkzeuge und entdeckt Mängel bestehender Werkzeuge
Formale Strenge: Bietet mechanisierte Coq-Beweise

Schwächen

Theoretische Abdeckung: Analysiert nur einen Teil der Programmtransformationstypen
Experimentelle Skalierung: Benchmark-Tests enthalten zwar echte Schwachstellen, sind aber relativ begrenzt
Werkzeugvollständigkeit: CT-RetDec basiert immer noch auf empirischen Methoden zum Deaktivieren bestimmter Passes

Einfluss

Akademischer Wert: Bietet einen neuen theoretischen Rahmen für die Sicherheitsanalyse von Programmtransformationen
Praktische Bedeutung: Beeinflusst direkt die Praxis der Sicherheitsanalyse kryptographischer Software
Werkzeugeinfluss: Die entdeckten Werkzeugmängel werden die Verbesserung verwandter Werkzeuge fördern

Anwendungsszenarien

Kryptographische Softwareanalyse: Geeignet für Szenarien, die CT-Analyse binärer kryptographischer Implementierungen erfordern
Compiler-Entwicklung: Bietet theoretische Grundlagen für die Sicherheitsverifikation von Compiler-Optimierungen
Sicherheitswerkzeugentwicklung: Bietet Anleitung für die Entwicklung zuverlässiger binärer Sicherheitsanalysewerkzeuge

Literaturverzeichnis

Das Papier zitiert 61 verwandte Arbeiten, die wichtige Arbeiten in mehreren Bereichen wie Seitenkanalanalyse, sichere Kompilierung und Dekompilierungstechniken abdecken und eine solide theoretische Grundlage für die Forschung bieten.