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

TL;DR

DALC-CT is an open-source dynamic analysis tool that verifies constant-time properties of low-level code by comparing instruction traces across multiple inputs, effectively detecting timing deviations.

Contribution

This work introduces DALC-CT, a novel dynamic analysis method for verifying constant-time properties using instruction trace comparisons, addressing limitations of existing approaches.

Findings

DALC-CT achieved perfect detection of constant-time violations in tested examples.

Instruction trace comparison effectively identifies timing deviations.

The approach is lightweight and reliable for verifying constant-time properties.

Abstract

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.