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

Decompiling for Constant-Time Analysis

基本信息

  • 论文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 (Programming Languages)
  • 发表时间: 2025年1月 (arXiv预印本)
  • 论文链接: https://arxiv.org/abs/2501.04183

摘要

密码学库是时序侧信道攻击的主要目标。防御这类攻击的实用方法是遵循常数时间(CT)策略。然而，编写常数时间代码很困难，即使是常数时间的源代码也可能被主流编译器转换为存在漏洞的二进制代码。本文研究如何验证二进制代码是否满足常数时间要求。一种常见方法是使用反编译器作为前端，将二进制代码转换为源代码或中间表示，然后应用现有的CT分析工具。不幸的是，这种"反编译-分析"方法存在问题。本文通过Clangover漏洞等实例证明，五种流行的反编译器都会消除CT违规，使得分析结果不可靠。

研究背景与动机

问题背景

  1. 时序侧信道攻击威胁：密码学实现容易受到时序侧信道攻击，攻击者可以通过观察程序执行时间来推断秘密信息
  2. 常数时间策略：CT策略要求程序执行时间不依赖于秘密输入，包括不执行依赖秘密的内存访问和分支跳转
  3. 编译器安全漏洞：主流编译器的优化可能将安全的源代码编译成存在CT违规的二进制代码

核心问题

现有的"反编译-分析"方法存在根本性缺陷：反编译器在转换过程中可能消除CT违规，导致分析工具错误地认为存在漏洞的二进制代码是安全的。

研究动机

  1. 实际需求：需要对二进制代码进行CT分析，但现有工具主要针对源代码
  2. 方法缺陷：当前使用反编译器作为前端的方法不可靠
  3. 理论缺失：缺乏评估程序转换是否适合CT分析的理论框架

核心贡献

  1. 发现并证明问题：通过Clangover等实例证明五种主流反编译器都会消除CT违规，使分析结果不可靠
  2. 提出CT透明性理论：形式化定义CT透明性概念，即程序转换既不消除也不引入CT违规
  3. 开发证明技术：提出基于仿真的通用方法来证明程序转换的CT透明性
  4. 构建实用工具：开发CT-RetDec工具，基于修改版RetDec反编译器进行可靠的二进制CT分析
  5. 发现工具缺陷：证明现有CT分析工具(CT-Verif和BinSec)内部使用的转换也不透明，存在安全漏洞

方法详解

任务定义

输入：二进制程序 输出：CT分析结果(安全/不安全) 约束：分析结果必须准确反映二进制程序的实际CT属性

理论框架

CT透明性定义

对于程序转换 ⟦⋅⟧:Ls→Lt\llbracket \cdot \rrbracket : L_s \to L_t，定义三个属性：

  1. 反射性(Reflection)：如果 ⟦P⟧\llbracket P \rrbracket 是φ-CT，则P是φ-CT
  2. 保持性(Preservation)：如果P是φ-CT，则 ⟦P⟧\llbracket P \rrbracket 是φ-CT
  3. 透明性(Transparency)：同时满足反射性和保持性

仿真技术

采用锁步仿真和放松仿真两种方法：

锁步仿真：输出程序的每一步都对应输入程序的一步

  • 仿真关系：s∼ts \sim t
  • 观察转换器：T:Os→OtT : O_s \to O_t
  • 关键条件：T必须是单射的

放松仿真：允许输入输出程序执行不同步数

  • 步数函数：ns:PC→N>0ns : PC \to \mathbb{N}_{>0}
  • 后缀函数：sf:PC→Os∗sf : PC \to O_s^*
  • PC单射性：对每个程序点，观察转换器都是单射的

技术创新点

  1. PC单射性概念：扩展了现有的CT保持技术，通过要求观察转换器在每个程序点上单射来保证反射性
  2. 统一框架：将多种程序转换统一在同一理论框架下分析
  3. 实用性导向：不仅提供理论分析，还开发了实际可用的工具

实验设置

数据集

  1. 反编译器测试：使用Clangover漏洞和构造的最小反例测试5种反编译器
  2. 基准测试集：160个二进制程序，包含10种已知的时序侧信道漏洞
    • 编译器：Clang 10/14/18/21
    • 优化级别：-O0, -Os
    • 架构：x86-32, x86-64

评价指标

  • 准确性：是否正确识别CT违规
  • 完整性：是否遗漏真实漏洞
  • 误报率：是否将安全代码标记为不安全

对比方法

  • 原版RetDec + CT-LLVM
  • CT-RetDec (修改版)
  • 手工分析作为ground truth

实现细节

  • 禁用RetDec中10个非透明的优化pass
  • 保留52个pass，其中7个经理论证明透明
  • 使用CT-LLVM进行最终的CT分析

实验结果

主要结果

反编译器透明性测试

所有5种测试的反编译器都会消除某些CT违规：

反编译器ClangoverBranch CoalescingEmpty BranchDead LoadDead Store
Angr✗✗-✗-
BinaryNinja-✗✗✗✗
Ghidra--✗✗-
Hex-Rays-✗✗✗-
RetDec✗✗✗✗✗

CT-RetDec性能评估

在160个基准程序上：

  • 准确率：100%（无误报，无漏报）
  • 原版RetDec：遗漏大部分CT违规
  • 改进效果：显著提升了CT分析的可靠性

程序转换分析

分析了10种常见程序转换的透明性：

透明转换（7种）：

  • 表达式替换（常量折叠、展开等）
  • 死分支消除
  • 死赋值消除
  • 反溢出优化
  • 结构化分析
  • 循环旋转

非透明转换（3种）：

  • 分支合并
  • If转换
  • 内存访问消除

工具漏洞发现

发现CT-Verif和BinSec工具存在安全漏洞：

  • CT-Verif：SMACK转换器会消除死加载，导致接受非CT程序
  • BinSec：DBA提升过程会合并空分支，消除CT违规

相关工作

侧信道分析

现有CT分析工具主要基于：

  • 乘积程序构造（CT-Verif）
  • 类型系统（Jasmin）
  • SMT求解器（Vale）
  • 抽象解释（Blazy等）
  • 符号执行（BinSec）

安全编译

相关研究关注编译器如何保持安全属性：

  • CT仿真技术（Barthe等）
  • 泄漏转换器方法
  • Jasmin和CompCert编译器的CT保持证明

反编译正确性

现有工作主要关注功能正确性，较少考虑安全属性保持。

结论与讨论

主要结论

  1. 问题普遍性：主流反编译器普遍存在CT透明性问题
  2. 理论必要性：需要形式化理论来评估和保证程序转换的透明性
  3. 实用可行性：通过理论指导可以构建可靠的二进制CT分析工具
  4. 工具缺陷：现有CT分析工具本身也存在透明性问题

局限性

  1. 覆盖范围：仅分析了基本CT策略，未涉及解密和精细化泄漏模型
  2. 转换类型：理论分析仅覆盖10种常见转换，RetDec包含62个pass
  3. 实现缺陷：即使理论透明的转换，实现中也可能存在bug

未来方向

  1. 扩展理论：支持更复杂的安全属性和泄漏模型
  2. 自动化验证：开发自动验证转换透明性的工具
  3. 编译器改进：将透明性要求集成到编译器设计中

深度评价

优点

  1. 问题重要性：解决了实际安全分析中的关键问题
  2. 理论贡献：提出了完整的CT透明性理论框架
  3. 实证充分：通过多个实例和基准测试验证了理论
  4. 实用价值：开发了可用的工具并发现了现有工具的漏洞
  5. 形式化严谨：提供了Coq机械化证明

不足

  1. 理论覆盖：仅分析了部分程序转换类型
  2. 实验规模：基准测试虽然包含真实漏洞，但规模相对有限
  3. 工具完善度：CT-RetDec仍基于经验方法禁用部分pass

影响力

  1. 学术价值：为程序转换的安全性分析提供了新的理论框架
  2. 实用意义：直接影响密码学软件的安全分析实践
  3. 工具影响：发现的工具漏洞将促进相关工具的改进

适用场景

  1. 密码学软件分析：适用于需要对二进制密码学实现进行CT分析的场景
  2. 编译器开发：为编译器优化的安全性验证提供理论基础
  3. 安全工具开发：为开发可靠的二进制安全分析工具提供指导

参考文献

论文引用了61篇相关文献，涵盖侧信道分析、安全编译、反编译技术等多个领域的重要工作，为研究提供了坚实的理论基础。