Decompiling for Constant-Time Analysis

Arranz-Olmos, Santiago

Decompiling for Constant-Time Analysis

2026-04-01

0

PRE

AI

A

Arranz-Olmos, Santiago *

DOI：

原文求助

摘要

En 中文

恒定时间编程规范常用于保护密码学库免受侧信道攻击。然而，编写恒定时间代码很困难；此外，编译器可能引入恒定时间违规。因此，确保汇编代码是恒定时间的至关重要。一种方法是证明源程序是恒定时间的，并且编译过程保持了恒定时间的特性。在本文中，我们探讨了“先反编译再分析”方法的方法论正确性和可扩展性，这是一种在静态分析更广泛背景下提出的非传统替代方案。非正式地讲，“先反编译再分析”方法使用反编译器作为静态分析工具的前端。为了说明我们的研究动机，我们表明当前的反编译器在恒定时间分析之前消除了CT漏洞，导致非恒定时间程序被接受为恒定时间。独立地，我们提供了两个流行的CT分析工具接受的非恒定时间、可利用程序的构造示例；在这两种情况下，罪魁祸首是在恒定时间分析之前内部使用的程序转换，它们消除了恒定时间违规。虽然我们的示例并未否定这些工具的一般方法，但它们强调了研究“先反编译再分析”方法的必要性。在方法论方面，我们定义了CT透明性的概念。非正式地讲，如果一个程序转换既不消除也不引入CT违规，则它是CT透明的。我们还提供了证明转换是CT透明的一般方法，并表明几个感兴趣的转换是透明的。我们还概述了将CT透明性扩展到推测恒定时间的扩展，后者被密码学软件用作对抗Spectre攻击的保护措施。在实践方面，我们构建了一个CT透明的基于LLVM的反编译器RETDEC的版本，并将其与现有的针对LLVM的CT验证工具CT-LLVM相结合。我们在一组包含二进制文件中真实世界漏洞的基准测试集上评估了由此产生的工具（称为CT-RETDEC），并表明这些修改对CT-RETDEC的性能产生了显著影响。

Keyword:

Decompilation

Static Analysis

Constant-Time

Side Channel

Decompiling for Constant-Time Analysis

摘要

期刊

机构

引用论文