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

• URL: http://arxiv.org/abs/2604.16832v1
• Date: Sat, 18 Apr 2026 04:47:54 GMT
• Title: DALC-CT: Dynamic Analysis of Low-Level Code Traces for Constant-Time Verification
• Abstract summary: We propose a novel approach for verifying constant-time programs based on dynamic analysis of low-level execution traces.<n>We developed an open-source tool called DALC-CT, for the constant-time verification of programs using this approach.
• Score: 0.08749675983608168
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• DISARM: Target Electronic Device Informed Mitigation of Software Runtime Side-Channel Vulnerabilities [2.537406035246369]
  Program runtime or timing attacks exploit variations in a program's execution times to extract sensitive information.<n>We propose DISARM, a joint hardware-software methodology for mitigating runtime side-channel vulnerabilities.<n>We implement DISARM to support C, C++, and Java source codes and validate it across 22 standard benchmarks.
  arXiv  Detail & Related papers  (2026-06-18T05:22:38Z)
• QUACK! Making the (Rubber) Ducky Talk: A Systematic Study of Keystroke Dynamics for HID Injection Detection [60.105690843777666]
  We show that robust, privacy-preserving detection is achievable using lightweight models operating solely on timing features.<n>Our analysis reveals that attacker sophistication does not monotonically translate into improved evasion.
  arXiv  Detail & Related papers  (2026-04-17T08:53:24Z)
• AgentProcessBench: Diagnosing Step-Level Process Quality in Tool-Using Agents [50.481033105867205]
  We introduce AgentProcessBench, the first benchmark dedicated to evaluating step-level effectiveness in realistic, tool-augmented trajectories.<n>The benchmark comprises 1,000 diverse trajectories and 8,509 human-labeled step annotations with 89.1% inter-annotator agreement.<n>It features a ternary labeling scheme to capture exploration and an error propagation rule to reduce labeling ambiguity.
  arXiv  Detail & Related papers  (2026-03-15T16:13:58Z)
• Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
  Real-time online object tracking in videos constitutes a core task in computer vision.<n>We propose interpreting object tracking as a sequential hypothesis test, wherein evidence for or against tracking failures is gradually accumulated over time.<n>We propose both supervised and unsupervised variants by leveraging either ground-truth or solely internal tracking information.
  arXiv  Detail & Related papers  (2026-02-13T14:57:15Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
  arXiv  Detail & Related papers  (2025-10-03T16:21:14Z)
• Systematic Timing Leakage Analysis of NIST PQDSS Candidates: Tooling and Lessons Learned [2.4508658326953108]
  We develop a toolchain that automates configuration, execution, and result analysis for several widely used constant-time analysis tools.<n>We report 26 issues in total to the respective developers, and 5 of them have already been fixed.
  arXiv  Detail & Related papers  (2025-09-04T08:41:06Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• CodeFlow: Program Behavior Prediction with Dynamic Dependencies Learning [11.347234752942684]
  We present CodeFlow, a novel machine learning-based approach that predicts code coverage and detects runtime errors.<n>CodeFlow effectively represents all possible execution paths and the statistic relations between different statements.<n>Our empirical evaluation demonstrates that CodeFlow significantly improves code coverage prediction accuracy and effectively localizes runtime errors.
  arXiv  Detail & Related papers  (2024-08-05T20:32:00Z)
• Cassandra: Efficient Enforcement of Sequential Execution for Cryptographic Programs (Extended Version) [3.34371579019566]
  Constant-time programming is a widely deployed approach to harden cryptographic programs against side channel attacks.<n>Modern processors often violate the underlying assumptions of standard constant-time policies by transiently executing unintended paths of the program.<n>We propose Cassandra, a novel hardware/software mechanism to enforce sequential execution for constant-time cryptographic code.
  arXiv  Detail & Related papers  (2024-06-06T17:34:48Z)
• Towards Efficient Verification of Constant-Time Cryptographic Implementations [5.433710892250037]
  Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks. We put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Our approach is implemented as a cross-platform and fully automated tool CT-Prover.
  arXiv  Detail & Related papers  (2024-02-21T03:39:14Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  We propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core.
  arXiv  Detail & Related papers  (2023-08-15T13:19:17Z)
• Execution Time Program Verification With Tight Bounds [6.36836017515443]
  This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs.
  arXiv  Detail & Related papers  (2022-10-20T09:02:13Z)
• Change Point Detection in Time Series Data using Autoencoders with a Time-Invariant Representation [69.34035527763916]
  Change point detection (CPD) aims to locate abrupt property changes in time series data. Recent CPD methods demonstrated the potential of using deep learning techniques, but often lack the ability to identify more subtle changes in the autocorrelation statistics of the signal. We employ an autoencoder-based methodology with a novel loss function, through which the used autoencoders learn a partially time-invariant representation that is tailored for CPD.
  arXiv  Detail & Related papers  (2020-08-21T15:03:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.