💻 computer science

DALC-CT: Dynamic Analysis of Low-Level Code Traces for Constant-Time Verification

本文提出了一种名为 DALC-CT 的开源工具，通过动态分析低层执行轨迹并比较不同输入下的指令序列分布，为程序提供了轻量级且可靠的常量时间属性验证方法，有效克服了传统形式化方法抽象过度及基于时间测量易受噪声干扰的局限。

原作者： Nges Brian Njungle, Edwin P. Kayang, Mishel J. Paul, Michel A. Kinsy

发布于 2026-04-21

📖 1 分钟阅读☕ 轻松阅读

原作者： Nges Brian Njungle, Edwin P. Kayang, Mishel J. Paul, Michel A. Kinsy

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文介绍了一种名为 DALC-CT 的新工具，它的任务是帮助程序员检查他们的代码是否“守口如瓶”，不会通过时间泄露秘密。

为了让你更容易理解，我们可以把整个故事想象成**“侦探抓内鬼”**的游戏。

1. 背景：为什么“时间”会泄露秘密？

想象一下，你有一个绝密的保险箱密码（比如 123456）。

坏情况（非恒定时间）： 你派了一个笨拙的守卫去核对密码。
- 如果用户输入 123456，守卫会开心地核对完所有 6 位，然后说“通过”。
- 如果用户输入 123450（最后一位错了），守卫核对到第 6 位发现不对，立刻大喊“不行！”并停止。
- 问题出在哪？ 虽然守卫都说了“不行”，但他花的时间不一样！核对前 5 位正确时，他多花了一点点时间。黑客就像躲在暗处的间谍，拿着秒表在外面听：“哦，刚才那个输入多花了 0.001 秒，看来前 5 位是对的！”
- 通过反复尝试和计时，黑客就能像拼拼图一样，把密码一个个猜出来。这就是**“定时侧信道攻击”**。
好情况（恒定时间）： 聪明的守卫会怎么做？
- 不管用户输入什么，守卫都会假装把 6 位数字都核对一遍。即使第 1 位就错了，他也会继续核对剩下的 5 位，最后才说“不行”。
- 这样，无论密码对错，守卫花的时间永远一样。黑客拿着秒表也听不出任何区别，自然就无法猜出密码了。

2. 以前的方法有什么缺点？

在 DALC-CT 出现之前，人们检查代码是否“恒定时间”主要有两种笨办法：

看源代码（纸上谈兵）： 就像让程序员自己写保证书说“我代码写得很好”。但问题是，代码写好后，编译器（把代码变成机器能懂的语言的翻译官）可能会自作聪明地优化代码，把原本“恒定”的逻辑改坏了。这就好比翻译官把“假装核对”改成了“直接跳过”，程序员自己都不知道。
拿秒表测（听风辨位）： 在电脑上反复运行程序，用秒表记录时间。但这就像在嘈杂的菜市场里听一根针掉在地上的声音。电脑里其他程序在跑、风扇在转、甚至天气热了 CPU 变慢，都会产生噪音。如果黑客的计时差异很小，很容易被这些噪音淹没，导致误判。

3. DALC-CT 的绝招：数“积木”

DALC-CT 发明了一种全新的、更聪明的方法。它不再看源代码，也不拿秒表去测时间，而是直接数程序运行时用了多少种“积木”。

什么是“积木”？
计算机程序在底层是由成千上万条微小的指令组成的，就像乐高积木。有的积木是“加法”，有的是“存数据”，有的是“跳转”。
它的逻辑是这样的：
- 如果程序是恒定时间的，那么无论输入什么秘密（比如密码是 123 还是 999），它使用的积木种类和数量必须完全一样。就像守卫无论核对什么密码，都要搬动完全相同数量的积木块。
- 如果程序不恒定时间，那么输入不同，积木的组合方式就会变。比如密码错了，守卫少搬了两块积木（少执行了两步）。

DALC-CT 的工作流程：

它把程序变成二进制文件（机器码）。
它像是一个超级显微镜，盯着程序运行，记录它每一步用了什么指令（积木）。
它给这些指令分类（比如：加法类、存数类、跳转类），一共分了 13 类。
它让程序用不同的秘密输入跑几遍，然后对比这几遍的“积木清单”。
- 如果清单完全一样（比如都是 100 个加法积木，50 个存数积木）：恭喜！这是恒定时间的，安全！
- 如果清单不一样（比如输入 A 用了 100 个加法，输入 B 只用了 90 个）：警报！这里有问题，秘密可能泄露了！

4. 为什么这个方法很厉害？

不听噪音，只看逻辑： 它不关心电脑风扇转得快慢，也不关心系统忙不忙。它只关心程序逻辑上到底执行了哪些指令。这就像不管外面多吵，只要看守卫手里搬的积木数量对不对，就能判断他有没有偷懒。
不受编译器欺骗： 不管编译器怎么优化代码，只要底层指令变了，DALC-CT 就能发现。它直接看最终执行的结果，而不是看程序员写了什么。
快速且准确： 论文里测试了很多例子（比如密码检查、加密计算），DALC-CT 只要跑几次，就能完美找出所有有问题的代码，而且没有误报。

5. 总结

这篇论文的核心思想就是：不要猜时间，要数指令。

以前我们担心程序会不会因为输入不同而“偷偷”改变执行步骤，从而泄露秘密。现在，DALC-CT 就像一位指令计数侦探，它通过对比不同输入下的“指令积木清单”，能一眼看穿程序是否在“演戏”。如果清单一样，说明程序守口如瓶；如果清单不一样，说明程序在“泄密”。

这是一种轻量级、可靠且实用的新方法，能帮助开发者在黑客利用时间差窃取密码之前，先把代码里的漏洞堵上。

论文技术总结：DALC-CT——基于低级执行痕迹动态分析的常量时间验证

1. 研究背景与问题 (Problem)

侧信道攻击与时间攻击：
计算机系统中的侧信道攻击（Side-channel attacks）利用系统物理或逻辑行为的间接信息泄露（如执行时间、功耗、电磁辐射等）来推断敏感数据。其中，时间侧信道攻击（Timing side-channel attacks）尤为危险，攻击者通过分析程序执行时间的微小差异（例如密码验证或模幂运算中的分支差异），可以逐步恢复出加密密钥等敏感信息。

现有验证方法的局限性：
为了防止此类攻击，密码学实现通常要求遵循**常量时间（Constant-Time）**原则，即程序的执行行为（包括指令序列、内存访问模式等）不应依赖于秘密输入。然而，验证程序是否真正满足常量时间性质极具挑战性：

形式化方法（Formal Methods）： 如 ct-verif、Binsec/Rel 等工具，通常基于源代码或中间表示（IR）进行抽象验证。这些方法往往无法完全捕捉编译优化、硬件微架构行为以及实际机器码的执行细节，导致理论与现实脱节。
基于统计的运行时测试： 如 Dudect，通过多次运行程序并测量执行时间来检测泄漏。这种方法极易受到操作系统噪声、并发进程和硬件环境波动的影响，难以区分微小的时间差异，且只能检测到产生显著时间方差的问题。

核心痛点： 缺乏一种既能反映真实硬件执行逻辑，又不过度依赖抽象模型或受噪声干扰的轻量级验证方法。

2. 方法论 (Methodology)

本文提出了一种名为 DALC-CT 的新方法，基于低级执行痕迹（Low-Level Execution Traces）的动态分析来验证常量时间属性。

核心思想

该方法不依赖源代码分析或外部时间测量，而是直接分析编译后的二进制文件在不同秘密输入下的指令执行序列。其核心假设是：如果一个程序是常量时间的，那么无论秘密输入值如何变化，其执行的**指令混合分布（Instruction Mix Distribution）**应当是完全一致的。

技术流程

动态二进制插桩 (DBI)：
- 使用 Valgrind 作为插桩引擎，对目标二进制文件中的特定函数进行动态执行跟踪。
- 系统接收编译后的二进制文件、目标函数名以及秘密输入变量作为输入。
指令分类与统计 (Instruction Classification)：
- 将收集到的指令序列按照指令类型和数据类型进行分类。
- 共定义了 13 个指令类别，包括：
  - 内存指令 (Memory)： 加载 (Load)、存储 (Store)。
  - 算术逻辑指令 (ALU)： 细分为轻量级 (Light)（如加减法、位运算，通常单周期）和重量级 (Heavy)（如乘除法、取模，通常多周期）。
  - 控制流指令 (Control-Flow)： 条件/无条件跳转。
  - 数据类型： 整数、浮点数、向量。
- 这种分类旨在捕捉不同指令在硬件执行延迟上的差异，同时保持分析的可行性。
痕迹比较与验证：
- 对同一函数使用不同的秘密输入值进行多次执行（通过简单的 havoc 模糊测试生成随机输入）。
- 记录每次执行中各类指令的计数，形成指令混合向量 (Instruction Mix Vector)。
- 判定标准： 如果对于任意一对秘密输入，其指令混合向量存在任何差异（即某类指令的计数不同），则判定该程序违反了常量时间原则。
形式化定义：
- 定义指令轨迹 $\tau$ 的指令混合向量 $\Phi(\tau)$ 。
- 常量时间性质定义为：对于所有秘密输入 $s_1, s_2$ ， $\Phi(E(f, p, s_1)) = \Phi(E(f, p, s_2))$ 。
- 通过计算向量差的 $L_1$ 范数（Manhattan norm）来量化差异，若不为 0 则视为违规。

3. 主要贡献 (Key Contributions)

提出新的验证范式：
引入了一种基于低级执行痕迹动态分析的常量时间验证新方法。该方法独立于系统软件、编译器优化级别和硬件实现，直接关注程序在硬件上的逻辑执行行为，填补了理论验证与实际二进制执行之间的空白。
开发开源工具 DALC-CT：
实现了基于上述方法的开源工具。该工具能够自动分析二进制文件，通过比较不同输入下的指令混合计数来检测常量时间违规。
精细化的指令分类体系：
设计了包含 13 个类别的指令分类系统，特别是将 ALU 指令细分为“轻量级”和“重量级”，以反映不同指令在 CPU 周期上的显著差异，提高了检测的准确性，避免了将单周期和多周期指令混为一谈。
广泛的评估与验证：
在 22 个知名的常量时间和非常量时间示例（包括密码检查、模幂运算、AES 密钥扩展等）上进行了评估。结果显示，DALC-CT 能够完美检测出所有非常量时间案例，且在不同编译器（GCC, Clang）和优化级别（-O0, -O1, -O2）下表现一致。

4. 实验结果 (Results)

检测准确率： 在测试的所有非常量时间示例中，DALC-CT 均成功检测到了指令序列的差异（完美检测）。对于常量时间示例，所有输入下的指令混合计数均保持一致。
案例研究：
- 密码检查： 传统的“提前退出”实现（非常量时间）在输入匹配长度不同时，指令计数（特别是控制流和 ALU 指令）显著不同；而常量时间实现（使用 XOR 累积）在所有输入下指令计数完全一致。
- 模幂运算： 基于条件分支的朴素实现（非常量时间）根据指数位是 0 还是 1 执行不同的指令路径；而使用位掩码的常量时间实现则始终执行相同的指令序列。
鲁棒性： 实验表明，该方法不受编译器优化（如死代码消除、循环展开）的影响，因为它是直接分析最终生成的机器码指令序列。
效率： 仅需少数几次运行（通常少于 5 次）即可暴露时间差异，具有轻量级和高效的特点。

5. 意义与局限性 (Significance & Limitations)

意义

填补空白： 提供了一种介于形式化验证（理论强但难落地）和统计测试（易受噪声干扰）之间的实用且可靠的验证方案。
贴近现实： 直接分析编译后的二进制代码，能够捕捉编译器优化引入的意外时间泄漏，这是源代码分析难以做到的。
开发者友好： 作为一个轻量级工具，它可以帮助开发者在开发早期快速识别和修复常量时间漏洞，无需深厚的形式化验证背景。

局限性与未来工作

微架构侧信道： 当前方法主要关注逻辑指令序列，未直接模拟微架构效应（如缓存命中/未命中、分支预测、推测执行）。即使指令序列相同，硬件状态（如缓存）的不同仍可能导致时间差异（例如 Prime+Probe 攻击）。
输入覆盖： 作为动态分析，其验证范围受限于测试输入集。虽然使用了简单的模糊测试，但为了获得全面保证，未来计划结合更智能的模糊测试（Fuzzing）或符号执行（Symbolic Execution）来覆盖更多路径。
互补性： 作者建议将 DALC-CT 与统计方法或形式化方法结合使用，以提供更强的安全保证。

总结

DALC-CT 通过动态分析低级指令痕迹，为常量时间验证提供了一种具体、可靠且轻量的新途径。它有效地桥接了理论定义与实际执行行为，对于提升密码学软件抵御时间侧信道攻击的能力具有重要的实用价值。