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

定時間分析のための逆コンパイル

基本情報

論文ID: 2501.04183
タイトル: Decompiling for Constant-Time Analysis
著者: 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)
分類: cs.PL (プログラミング言語)
発表時期: 2025年1月 (arXiv プレプリント)
論文リンク: https://arxiv.org/abs/2501.04183

概要

暗号化ライブラリはタイミング側チャネル攻撃の主要な標的である。このような攻撃に対する防御の実用的な方法は、定時間(CT)戦略に従うことである。しかし、定時間コードの作成は困難であり、定時間のソースコードであっても、主流のコンパイラによって脆弱性のあるバイナリコードに変換される可能性がある。本論文は、バイナリコードが定時間要件を満たしているかどうかを検証する方法を研究する。一般的なアプローチは、逆コンパイラをフロントエンドとして使用し、バイナリコードをソースコードまたは中間表現に変換してから、既存のCT分析ツールを適用することである。残念ながら、この「逆コンパイル-分析」方法には問題がある。本論文はClangover脆弱性などの事例を通じて、5つの一般的な逆コンパイラがすべてCT違反を排除し、分析結果を信頼できなくすることを証明している。

研究背景と動機

問題背景

タイミング側チャネル攻撃の脅威: 暗号化実装はタイミング側チャネル攻撃に対して脆弱であり、攻撃者はプログラム実行時間を観察することで秘密情報を推測できる
定時間戦略: CT戦略は、プログラム実行時間が秘密入力に依存しないことを要求し、秘密に依存するメモリアクセスと分岐ジャンプの実行を含まない
コンパイラセキュリティ脆弱性: 主流コンパイラの最適化により、安全なソースコードが定時間違反のあるバイナリコードにコンパイルされる可能性がある

中核的問題

既存の「逆コンパイル-分析」方法には根本的な欠陥がある。逆コンパイラは変換プロセス中にCT違反を排除する可能性があり、分析ツールが脆弱性のあるバイナリコードを誤って安全と判定する原因となる。

研究動機

実際的ニーズ: バイナリコードに対するCT分析が必要だが、既存ツールは主にソースコードを対象としている
方法の欠陥: 逆コンパイラをフロントエンドとして使用する現在の方法は信頼できない
理論的欠落: プログラム変換がCT分析に適しているかどうかを評価する理論的枠組みが不足している

中核的貢献

問題の発見と証明: Clangover等の事例を通じて、5つの主流逆コンパイラがすべてCT違反を排除し、分析結果を信頼できなくすることを証明
CT透明性理論の提案: CT透明性の概念を形式的に定義。すなわち、プログラム変換がCT違反を排除も導入もしない
証明技術の開発: シミュレーションベースの汎用方法を提案し、プログラム変換のCT透明性を証明
実用ツールの構築: 修正版RetDec逆コンパイラに基づくCT-RetDecツールを開発し、信頼できるバイナリCT分析を実現
ツール欠陥の発見: 既存のCT分析ツール(CT-VerifおよびBinSec)が内部で使用する変換も透明でなく、セキュリティ脆弱性があることを証明

反射性(Reflection): $\llbracket P \rrbracket$ がφ-CTであれば、Pはφ-CT
保持性(Preservation): Pがφ-CTであれば、 $\llbracket P \rrbracket$ はφ-CT
透明性(Transparency): 反射性と保持性の両方を満たす

シミュレーション技術

ロックステップシミュレーションと緩和シミュレーションの2つの方法を採用:

ロックステップシミュレーション: 出力プログラムの各ステップが入力プログラムの1ステップに対応

シミュレーション関係: $s \sim t$
観察変換器: $T : O_s \to O_t$
重要条件: Tは単射である必要がある

緩和シミュレーション: 入出力プログラムが異なるステップ数で実行することを許可

ステップ数関数: $ns : PC \to \mathbb{N}_{>0}$
サフィックス関数: $sf : PC \to O_s^*$
PC単射性: 各プログラムポイントに対して、観察変換器は単射である

技術的革新点

PC単射性の概念: 既存のCT保持技術を拡張し、各プログラムポイントで観察変換器が単射であることを要求することで反射性を保証
統一的枠組み: 複数のプログラム変換を同一の理論的枠組みの下で分析
実用性指向: 理論分析を提供するだけでなく、実際に使用可能なツールも開発

実験設定

データセット

逆コンパイラテスト: Clangover脆弱性と構築された最小反例を使用して5つの逆コンパイラをテスト
ベンチマークセット: 160個のバイナリプログラム。10種類の既知タイミング側チャネル脆弱性を含む
- コンパイラ: Clang 10/14/18/21
- 最適化レベル: -O0、-Os
- アーキテクチャ: x86-32、x86-64