pith. sign in

arxiv: 2604.16832 · v1 · submitted 2026-04-18 · 💻 cs.CR · cs.PL

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

Nges Brian Njungle , Edwin P. Kayang , Mishel J. Paul , Michel A. Kinsy This is my paper

Pith reviewed 2026-05-10 07:16 UTC · model grok-4.3

classification 💻 cs.CR cs.PL
keywords constant-time verificationtiming side-channel attacksdynamic analysisinstruction tracescryptographic implementationsbinary analysisside-channel resistance
0
0 comments X

The pith

Comparing low-level instruction traces across inputs detects constant-time violations in programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a method to verify if cryptographic code runs in constant time by examining the sequence of instructions executed for different secret inputs. Instead of relying on formal proofs or noisy timing measurements, it runs the binary multiple times and checks whether the mix of instructions changes. If the distribution of instructions differs between traces, the code likely leaks information through timing variations. The authors built an open-source tool called DALC-CT that automates this comparison and tested it on standard examples, finding every constant-time violation they expected. This approach matters because timing side-channel attacks remain a practical threat to crypto implementations, and current verification methods either abstract away real hardware behavior or suffer from environmental noise.

Core claim

We propose DALC-CT, a dynamic analysis tool that verifies constant-time behavior by measuring and comparing instruction sequences across multiple input values for a given binary and function. Variations in the instruction mix distribution between any pair of traces indicate a deviation from constant-time principles. Evaluation on well-known constant-time and non-constant-time examples achieved perfect detection of issues, showing that instruction trace comparisons provide a lightweight and reliable verification method.

What carries the argument

The instruction mix distribution comparison across execution traces for different inputs, implemented in the DALC-CT tool.

Load-bearing premise

That any violation of constant-time behavior will produce detectable differences in the distribution of instructions executed for different inputs.

What would settle it

A program with an exploitable timing leak that nevertheless produces identical instruction mix distributions for all secret inputs.

Figures

Figures reproduced from arXiv: 2604.16832 by Edwin P. Kayang, Michel A. Kinsy, Mishel J. Paul, Nges Brian Njungle.

Figure 1
Figure 1. Figure 1: Architecture of DALC-CT. The framework takes a program binary, secret input values, and the target function, then uses a DBI engine to instrument execution rounds. The orchestrator manages DBI inputs, instrumentation while the instruction analyzer evaluates operand groups and instruction behavior to determine the constant-time status and generate a verification report. function under multiple input values.… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents DALC-CT, an open-source dynamic analysis tool that extracts low-level instruction traces from binaries, compares instruction sequences and mix distributions across multiple inputs to a target function, and flags any differences as violations of the constant-time property. It claims that this approach provides a lightweight, reliable verification method and reports perfect detection of issues on a set of well-known constant-time and non-constant-time examples.

Significance. If the central claim holds, the work would supply a practical, low-overhead complement to formal verification tools and noisy hardware timing measurements for checking constant-time cryptographic code. The open-source release and evaluation on standard examples are positive features that could aid reproducibility and adoption in the constant-time verification community.

major comments (2)
  1. [Abstract] Abstract, third paragraph: the assertion that 'any variations in the instruction mix distribution for any given pair of traces indicate a deviation from the constant-time principle' is incomplete for verifying the constant-time property. Many documented timing leaks (secret-dependent load/store addresses producing cache misses or branch-predictor effects) execute identical instruction sequences and mixes yet still leak via microarchitectural timing; the method as described would produce false negatives on these cases.
  2. [Evaluation] Evaluation description (the paragraph beginning 'We evaluated it on a set of well-known...'): the 'perfect detection of issues' result is reported without enumerating the specific test cases, classifying whether they include address-dependent or data-dependent leaks, or providing false-negative analysis. This is load-bearing because the claim of reliability rests on the completeness of the detection, not merely its precision on control-flow-dependent examples.
minor comments (1)
  1. [Abstract] Abstract: the phrase 'instruction mix distribution' is used without a precise definition or pseudocode for how traces are normalized and compared; a short formalization would improve clarity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback, which helps clarify the scope and presentation of our work on DALC-CT. We address each major comment below and outline the revisions we will make to the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract, third paragraph: the assertion that 'any variations in the instruction mix distribution for any given pair of traces indicate a deviation from the constant-time principle' is incomplete for verifying the constant-time property. Many documented timing leaks (secret-dependent load/store addresses producing cache misses or branch-predictor effects) execute identical instruction sequences and mixes yet still leak via microarchitectural timing; the method as described would produce false negatives on these cases.

    Authors: We acknowledge that the statement in the abstract is overly broad. Our method detects deviations from constant-time behavior by identifying differences in instruction sequences and mix distributions across execution traces for different inputs. This approach reliably identifies cases where secret data influences control flow or the executed instructions. However, it does not detect timing leaks that arise solely from microarchitectural effects, such as secret-dependent memory addresses leading to cache misses, when the instruction sequence remains identical. We will revise the abstract to more precisely describe the capabilities of DALC-CT as a tool for detecting instruction-level variations, positioning it as a lightweight complement to formal methods and hardware measurements rather than a complete solution for all constant-time properties. This revision will be made in the next version of the manuscript. revision: yes

  2. Referee: [Evaluation] Evaluation description (the paragraph beginning 'We evaluated it on a set of well-known...'): the 'perfect detection of issues' result is reported without enumerating the specific test cases, classifying whether they include address-dependent or data-dependent leaks, or providing false-negative analysis. This is load-bearing because the claim of reliability rests on the completeness of the detection, not merely its precision on control-flow-dependent examples.

    Authors: The evaluation section indeed summarizes the results without providing the detailed breakdown requested. The test suite consists of well-known examples including constant-time cryptographic primitives (such as AES, RSA implementations known to be constant-time) and their non-constant-time counterparts with explicit secret-dependent branches or data accesses that alter instruction mixes. All cases with instruction mix variations were detected, and no false positives were observed on constant-time code. We will expand this section to enumerate the specific test cases, classify them by leak type (e.g., branch-dependent vs. data-dependent affecting mix), and include a discussion of false negatives for microarchitectural leaks not altering traces. This will provide a more transparent assessment of the method's strengths and limitations. revision: yes

Circularity Check

0 steps flagged

No circularity; direct measurement technique validated on external examples

full rationale

The paper proposes a dynamic analysis method (DALC-CT) that compares instruction sequences and mix distributions across traces for different inputs to detect deviations from constant-time behavior. The central claim is supported by direct evaluation on a set of well-known external constant-time and non-constant-time examples, reporting perfect detection. No equations, derivations, fitted parameters, or self-citations appear as load-bearing elements. The approach is defined directly as a trace-comparison technique and tested against independent benchmarks, making the result self-contained rather than reducing to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that instruction mix variations are a sufficient proxy for timing side-channel leakage and that the dynamic tracing captures representative execution behavior.

axioms (1)
  • domain assumption Variations in instruction mix distribution across traces for different inputs indicate deviation from constant-time behavior.
    This is the core detection rule stated in the abstract.

pith-pipeline@v0.9.0 · 5570 in / 1196 out tokens · 41830 ms · 2026-05-10T07:16:55.876531+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

35 extracted references · 1 canonical work pages

  1. [1]

    April: A processor architecture for multiprocessing

    Anant Agarwal, Beng-Hong Lim, David Kranz, and John Kubiatowicz. April: A processor architecture for multiprocessing. InProceedings of the 17th annual international symposium on Computer Architecture, pages 104–114, 1990

    1990

  2. [2]

    Lucky thirteen: Breaking the tls and dtls record protocols

    Nadhem J Al Fardan and Kenneth G Paterson. Lucky thirteen: Breaking the tls and dtls record protocols. In2013 IEEE symposium on security and privacy, pages 526–540. IEEE, 2013

    2013

  3. [3]

    pearson Education, 2007

    V Aho Alfred, S Lam Monica, and D Ullman Jeffrey.Compilers principles, techniques & tools. pearson Education, 2007

    2007

  4. [4]

    Formal verification of side-channel countermeasures using self- composition.Science of Computer Programming, 78(7):796–812, 2013

    J Bacelar Almeida, Manuel Barbosa, Jorge S Pinto, and B ´arbara Vieira. Formal verification of side-channel countermeasures using self- composition.Science of Computer Programming, 78(7):796–812, 2013

    2013

  5. [5]

    Verifying{Constant-Time}implementations

    Jos ´e Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franc ¸ois Dupres- soir, and Michael Emmi. Verifying{Constant-Time}implementations. In25th USENIX Security Symposium (USENIX Security 16), pages 53– 70, 2016

    2016

  6. [6]

    Amir H Ashouri, Andrea Bignoli, Gianluca Palermo, Cristina Silvano, Sameer Kulkarni, and John Cavazos. Micomp: Mitigating the compiler phase-ordering problem using optimization sub-sequences and machine learning.ACM Transactions on Architecture and Code Optimization (TACO), 14(3):1–28, 2017

    2017

  7. [7]

    A comprehensive review of cyber security vulnerabilities, threats, attacks, and solutions.Electronics, 12(6):1333, 2023

    ¨Omer Aslan, Semih Serkant Aktu ˘g, Merve Ozkan-Okay, Abdullah Asim Yilmaz, and Erdal Akin. A comprehensive review of cyber security vulnerabilities, threats, attacks, and solutions.Electronics, 12(6):1333, 2023

    2023

  8. [8]

    Mcbits: fast constant-time code-based cryptography

    Daniel J Bernstein, Tung Chou, and Peter Schwabe. Mcbits: fast constant-time code-based cryptography. InInternational Conference on Cryptographic Hardware and Embedded Systems, pages 250–272. Springer, 2013

    2013

  9. [9]

    Verifying constant- time implementations by abstract interpretation.Journal of Computer Security, 27(1):137–163, 2019

    Sandrine Blazy, David Pichardie, and Alix Trieu. Verifying constant- time implementations by abstract interpretation.Journal of Computer Security, 27(1):137–163, 2019

    2019

  10. [10]

    Remote timing attacks are practical

    David Brumley and Dan Boneh. Remote timing attacks are practical. Computer Networks, 48(5):701–716, 2005

    2005

  11. [11]

    Password interception in a ssl/tls channel

    Brice Canvel, Alain Hiltgen, Serge Vaudenay, and Martin Vuagnoux. Password interception in a ssl/tls channel. InAnnual International Cryptology Conference, pages 583–599. Springer, 2003

    2003

  12. [12]

    Fact: A flexible, constant- time programming language

    Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, and Deian Stefan. Fact: A flexible, constant- time programming language. In2017 IEEE Cybersecurity Development (SecDev), pages 69–76. IEEE, 2017

    2017

  13. [13]

    Constant-timeness verification tools

    ct-tools. Constant-timeness verification tools. https://github.com/ crocs-muni/ct-tools, 2023. Accessed: 2026-01-10

    2023

  14. [14]

    Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level

    Lesly-Ann Daniel, S ´ebastien Bardin, and Tamara Rezk. Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. In2020 IEEE Symposium on Security and Privacy (SP), pages 1021–

  15. [15]

    With great power come great side channels: Statistical timing{Side-Channel}anal- yses with bounded type-1 errors

    Martin Dunsche, Marcel Maehren, Nurullah Erinola, Robert Merget, Nicolai Bissantz, Juraj Somorovsky, and J ¨org Schwenk. With great power come great side channels: Statistical timing{Side-Channel}anal- yses with bounded type-1 errors. In33rd USENIX Security Symposium (USENIX Security 24), pages 6687–6704, 2024

    2024

  16. [16]

    these results must be false

    Marcel Fourn ´e, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. “these results must be false”: A usability evaluation of constant-time analysis tools. InProceedings of the 33rd USENIX Security Symposium, pages 6705–6722. USENIX Association, 2024

    2024

  17. [17]

    Taxonomies of attacks and vulnerabilities in computer systems.IEEE Communications Surveys & Tutorials, 10(1):6–19, 2008

    Vinay M Igure and Ronald D Williams. Taxonomies of attacks and vulnerabilities in computer systems.IEEE Communications Surveys & Tutorials, 10(1):6–19, 2008

    2008

  18. [18]

    they’re not that hard to mitigate

    Jan Jancar, Marcel Fourn ´e, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. “they’re not that hard to mitigate”: What cryptographic library develop- ers think about timing attacks. In2022 IEEE Symposium on Security and Privacy (SP), pages 632–649. IEEE, 2022

    2022

  19. [19]

    they’re not that hard to mitigate

    Jan Jancar, Marcel Fourn ´e, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. “they’re not that hard to mitigate”: What cryptographic library develop- ers think about timing attacks. In43rd IEEE Symposium on Security and Privacy, San Francisco, 2022. IEEE

    2022

  20. [20]

    Symbolic execution and program testing, 1976

    James C King. Symbolic execution and program testing, 1976

    1976

  21. [21]

    Spectre attacks: Exploiting speculative execution

    Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, et al. Spectre attacks: Exploiting speculative execution. Communications of the ACM, 63(7):93–101, 2020

    2020

  22. [22]

    Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems

    Paul C Kocher. Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. InAnnual international cryptology conference, pages 104–113. Springer, 1996

    1996

  23. [23]

    ctgrind—checking that functions are constant time with valgrind, 2010.URL https://github

    Adam Langley. ctgrind—checking that functions are constant time with valgrind, 2010.URL https://github. com/agl/ctgrind, 84, 2010

    2010

  24. [24]

    Llvm: A compilation framework for lifelong program analysis & transformation

    Chris Lattner and Vikram Adve. Llvm: A compilation framework for lifelong program analysis & transformation. InInternational symposium on code generation and optimization, 2004. CGO 2004., pages 75–86. IEEE, 2004

    2004

  25. [25]

    Meltdown

    Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. Meltdown.arXiv preprint arXiv:1801.01207, 2018

    work page Pith review arXiv 2018

  26. [26]

    Valgrind: a framework for heavyweight dynamic binary instrumentation.ACM Sigplan notices, 42(6):89–100, 2007

    Nicholas Nethercote and Julian Seward. Valgrind: a framework for heavyweight dynamic binary instrumentation.ACM Sigplan notices, 42(6):89–100, 2007

    2007

  27. [27]

    Silent breaches: Exploring emerging threats and defenses in side channel attacks.researchgate

    Gayani Palihawadana. Silent breaches: Exploring emerging threats and defenses in side channel attacks.researchgate. net,. researchgate. net

  28. [28]

    Prentice Hall Professional, 2012

    Charles P Pfleeger and Shari Lawrence Pfleeger.Analyzing computer security: A threat/vulnerability/countermeasure approach. Prentice Hall Professional, 2012

    2012

  29. [29]

    Linkers and loaders.ACM Computing Surveys (CSUR), 4(3):149–167, 1972

    Leon Presser and John R White. Linkers and loaders.ACM Computing Surveys (CSUR), 4(3):149–167, 1972

    1972

  30. [30]

    Dude, is my code constant time? InDesign, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pages 1697–1702

    Oscar Reparaz, Josep Balasch, and Ingrid Verbauwhede. Dude, is my code constant time? InDesign, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pages 1697–1702. IEEE, 2017

    2017

  31. [31]

    Sparse representation of implicit flows with applications to side- channel detection

    Bruno Rodrigues, Fernando Magno Quint ˜ao Pereira, and Diego F Aranha. Sparse representation of implicit flows with applications to side- channel detection. InProceedings of the 25th International Conference on Compiler Construction, pages 110–120, 2016

    2016

  32. [32]

    Introduction to side-channel attacks

    Franc ¸ois-Xavier Standaert. Introduction to side-channel attacks. In Secure integrated circuits and systems, pages 27–42. Springer, 2009

    2009

  33. [33]

    Survey of cpu cache-based side-channel attacks: Systematic analysis, security models, and countermeasures

    Chao Su and Qingkai Zeng. Survey of cpu cache-based side-channel attacks: Systematic analysis, security models, and countermeasures. Security and Communication Networks, 2021(1):5559552, 2021

    2021

  34. [34]

    Timing and side channel attacks

    Nezer Zaidenberg and Amit Resh. Timing and side channel attacks. In Cyber Security: Analytics, Technology and Automation, pages 183–194. Springer, 2015

    2015

  35. [35]

    Fuzzing: a survey for roadmap.ACM Computing Surveys (CSUR), 54(11s):1–36, 2022

    Xiaogang Zhu, Sheng Wen, Seyit Camtepe, and Yang Xiang. Fuzzing: a survey for roadmap.ACM Computing Surveys (CSUR), 54(11s):1–36, 2022

    2022