Timing side-channel attacks exploit variations in program execution time to recover sensitive information. Cryptographic implementations are especially vulnerable to these attacks, since even small timing differences in operations such as modular exponentiation or key comparisons can be exploited to extract highly sensitive information, such as secret keys. To mitigate this threat, implementations of programs that handle sensitive information are often expected to adhere to constant-time principles, ensuring that execution behavior does not depend on secret inputs. However, validating the constant-time property of programs remains a major challenge in cryptography development. Formal method approaches to verify constant-time implementations rely on abstractions that often fail to capture real execution behavior, while timing-based measurement techniques are highly sensitive to noise from other programs and even hardware environments. In this work, we propose a novel approach for verifying constant-time programs based on dynamic analysis of low-level execution traces. Our method measures instruction sequences across multiple input values for any given binary and targeted function. Any variations in the instruction mix distribution for any given pair of traces indicate a deviation from the constant-time principle and behavior. We developed an open-source tool called DALC-CT, for the constant-time verification of programs using this approach. We evaluated it on a set of well-known constant-time and non-constant-time examples, achieving a perfect detection of issues. Our results demonstrate that analyzing the logical execution of programs via instruction trace comparisons provides a lightweight and reliable way to verify the constant-time property of programs.

翻译：定时侧信道攻击利用程序执行时间的差异来恢复敏感信息。加密实现尤其容易受到此类攻击，因为即使是模幂运算或密钥比较等操作中的微小时间差异，也可能被用于提取高度敏感的信息（如密钥）。为缓解这一威胁，处理敏感信息的程序实现通常需要遵守常量时间原则，确保执行行为不依赖于秘密输入。然而，验证程序的常量时间属性仍是密码学开发中的一项重大挑战。用于验证常量时间实现的形式化方法依赖于抽象模型，这些模型往往无法捕获真实的执行行为；而基于时序的测量技术则容易受到其他程序甚至硬件环境噪声的干扰。本文提出了一种基于低级执行轨迹动态分析的常量时间程序验证新方法。我们的方法针对任意给定的二进制程序和目标函数，测量其在多个输入值下的指令序列。当任意轨迹对之间的指令混合分布出现变化时，即表明程序偏离了常量时间原则及其行为。我们开发了一款名为DALC-CT的开源工具，采用该方法进行程序的常量时间验证。我们在多组已知的常量时间与非常量时间示例上进行了评估，实现了对问题的完美检测。结果表明，通过指令轨迹比较分析程序的逻辑执行，为验证程序的常量时间属性提供了一种轻量级且可靠的方式。