Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

Decompiling for Constant-Time Analysis

T0 review · 3 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Standard decompilers erase the secret leaks that constant-time checks are meant to find, so the paper defines and enforces a transparency condition for safe decompilation.

desk verdict Solid formal core and a real warning about decompiler unsoundness, but the practical claim of reliable detection is partly in-sample and needs an out-of-sample evaluation. read the letter →

arxiv 2501.04183 v4 pith:6DTCLJ6J submitted 2025-01-07 cs.PL

Santiago Arranz-Olmos , Gilles Barthe , Lionel Blatter , Youcef Bouzid , Sören van der Wall , Zhiyuan Zhang This is my paper · ORCID
classification cs.PL
keywords constant-timedecompilationCTtransparencyside-channelanalysisRetDecLLVMIRsecurecompilationstatic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper establishes a soundness problem at the heart of the Decompile-then-Analyze approach to binary constant-time verification: off-the-shelf decompilers routinely simplify away the secret-dependent branches and memory accesses that a constant-time analyzer is supposed to detect, so non-CT binaries are certified as secure. It introduces CT transparency, the requirement that a program transformation neither removes nor introduces CT violations, and gives a proof technique for transparency based on simulations whose observation transformer is injective at each program point. With that technique it proves seven standard decompilation passes transparent and isolates three that are not: if conversion, branch coalescing, and memory-access elimination. It then builds CT-RetDec, an LLVM-based decompiler variant with non-transparent passes disabled, paired with CT-LLVM; on a benchmark of 160 binaries spanning four Clang versions, two optimization levels, and two architectures, it finds every ground-truth CT violation without false positives, where unmodified RetDec misses most of them.

What carries the argument

The load-bearing object is the program transformation between a source language and a target language, each equipped with a leakage semantics in which memory accesses leak their address and branches leak their condition. CT transparency is reflection plus preservation, and the proof method is a relaxed simulation diagram: every output step is mimicked by one or more input steps whose observation sequence is mapped to the output observation by a partial transformer $T$. The added condition is PC-injectivity: for a fixed program point, $T$ never maps two different input observation sequences to the same output observation, allowing a preservation proof to be flipped into a reflection proof. For the seven transparent passes, the paper provides explicit $T$, step-count, and suffix functions.

What would settle it

Run CT-RetDec on a fresh collection of non-CT binaries whose leaks come from patterns absent from the examples in Figures 1 and 9a-9d, and compare its verdicts with manual inspection of the assembly; if any secret-dependent branch or memory access survives decompilation yet CT-RetDec reports constant-time, the retained pass configuration is not transparent. The opposite direction, a CT binary flagged as violating, would refute preservation.

Watch

Extended reading notes

Core claim

The central claim is that the Decompile-then-Analyze approach is unsound unless every transformation applied before constant-time analysis is CT transparent: a transformation is transparent when it reflects CT (if the output is $\phi$-CT then the input is $\phi$-CT) and preserves CT (if the input is $\phi$-CT then the output is $\phi$-CT). The paper shows concretely that five decompilers violate reflection: RetDec turns Clangover's secret-dependent branch in ML-KEM into a conditional move, and Angr, BinaryNinja, Ghidra, Hex-Rays, and RetDec each remove at least one type of crafted violation. It also shows that CT-Verif and BinSec accept constructed non-CT programs because their internal converters erase the violation. The constructive result is CT-RetDec, a decompilation toolchain whose retained passes are proven or empirically transparent, which correctly detects all 160 test binaries' CT status while unmodified RetDec misses most violations.

Load-bearing premise

The practical claim about CT-RetDec rests on the assumption that the hand-picked set of leak snippets and the 160 benchmark binaries are representative enough that the ten disabled passes are the right ones for all other binaries; the paper states that the empirical tests do not guarantee the retained passes are transparent.

Editorial extensions

If this is right

  • Off-the-shelf decompilers and lifters should not be used as front-ends for constant-time analysis without auditing their passes for transparency.
  • CT analysis tools that convert programs before analysis, for example to Boogie or DBA IR, must document and prove the transparency of those converters, since even sound analyses can be made unsound by the conversion.
  • The proof technique gives decompiler developers a concrete recipe: prove a pass transparent by giving a simulation with a PC-injective observation transformer, and the pass can be safely retained in a CT-focused toolchain.
  • A binary-level CT tool built on transparent decompilation can detect compiler-induced vulnerabilities in shipped binaries, including cases where the source code is CT but the compiled code is not.
  • The same transparency framework extends to speculative constant-time, letting tools also check Spectre-style leakage after decompilation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the PC-injectivity simulation pattern is likely portable to other security properties defined as indistinguishability of observation sequences, such as memory-safety or data-only side channels; the paper itself only gestures at hardware-software contracts as future work.
  • The evaluation is partly in-sample: the pass selection for CT-RetDec was guided by the same Clangover example that also appears in the 160-binary benchmark, so a stronger test would run the fixed configuration on a fresh corpus of compiler-induced leaks that played no role in choosing the disabled passes.
  • Transparent decompilation could be combined with analyzers other than CT-LLVM, because transparency protects the transformation itself and does not depend on the downstream analysis.
  • A testable extension is to reuse the paper's minimal leak snippets (constant branch, dead load, dead store) as a regression suite for any CT tool that performs internal program conversion, checking whether the tool still reports the leak.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper studies the Decompile-then-Analyze (DtA) approach to constant-time verification, in which a decompiler is used as the front-end of a source/IR-level CT analysis. It defines CT transparency as the conjunction of CT reflection and CT preservation, introduces PC-injective observation transformers as a sufficient condition for proving transparency (Theorem 2), and reports a Rocq mechanization of the general theorem. The paper proves or sketches transparency for seven abstract transformations, gives counterexamples for if conversion, branch coalescing, and memory-access elimination, and shows empirically that five decompilers remove CT violations. As independent findings, it constructs non-CT programs accepted by CT-Verif and BinSec. Finally, it builds CT-RetDec by disabling ten RetDec passes and evaluates the tool on a benchmark of 160 binaries compiled from known CT-relevant vulnerabilities.

Significance. The formal framework is a clean and useful contribution: separating reflection from preservation and isolating PC-injectivity makes prior CT-preservation simulation proofs reusable for transparency, and the machine-checked proof of the general simulation theorem is a concrete strength. The negative results on current decompilers and on the internal converters of CT-Verif and BinSec are specific, reproducible in principle, and important for tool developers. The practical RQ3 claim is plausible but is currently supported only by an evaluation whose tuning and benchmark sets overlap, so the generalizability of CT-RetDec to unseen binaries is not yet demonstrated.

major comments (3)
  1. [§6.2–6.3, Table 3] The pass configuration of CT-RetDec is selected in §6.2 by empirically testing reflection on the patterns of Figures 1 and 9a–9d and preservation on Figure 10, yet the §6.3 benchmark on which Table 3 claims that CT-RetDec correctly finds all CT violations includes ct_clangover, the same Clangover pattern from Figure 1, and the paper itself states in §6 that the empirical tests do not guarantee that passes are transparent. The benchmark therefore is not an independent test of the fixed configuration, and the RQ3 conclusion that CT-RetDec is suitable for real-world binaries is stronger than the evidence. Please separate the tuning set from a held-out validation set, or at minimum report in-sample and out-of-sample results separately, and soften the Section 9 claim that CT-RetDec transparently decompiles the benchmark.
  2. [§5.2, Theorem 5 and Appendix A.3, Proposition 3] The proof of Dead Assignment Elimination transparency assumes a correctness guarantee for the dead-variable annotations D. The main text says "we omit the correctness guarantee," and Appendix A.3 states the needed property as Proposition 3 without proving it; the subsequent proof uses Proposition 3 to derive the inequality (D\{x})∪vars(e)⊆D', which is essential for showing that the simulation relation is preserved after deleting the assignment. Thus Theorem 5 is not established as stated. Please add a proof of Proposition 3, or of the underlying liveness-analysis correctness, or make explicit that the theorem is conditional on an unproved side condition.
  3. [§6 and §9] The paper oscillates between calling CT-RetDec transparent and acknowledging that transparency is not guaranteed for the actual pipeline. Definition 3 and Theorem 2 concern abstract transformations, while §6.2's "empirically transparent" is defined relative to CT-LLVM's reports on a few hand-crafted test cases, and §6 explicitly lists two residual reasons why the modified RetDec may still not be transparent: untested passes and implementation bugs. The conclusion in §9 that "CT-RetDec, which transparently decompiles our benchmark set" should be replaced by a claim about empirical detection on the evaluated binaries, and the abstract should be checked for the same overstatement.
minor comments (4)
  1. [Table 3] The caption contains the typo "CT-RetDEc" instead of "CT-RetDec."
  2. [Appendix B] The RetDec Utility Passes list contains retdec-value-protect twice, which makes the table of passes harder to read.
  3. [§6.2] The statement that the empirical test set "checks for both reflection and preservation" is slightly overstated: there is only one preservation test case, shown in Figure 10, while the reflection cases cover five patterns.
  4. [Appendix A] The appendix says it provides detailed proofs for a selection of transformations, but the main text refers to Appendix A as containing the detailed proofs for the transformations in Section 5.2; the paper should state explicitly which proofs are fully formal, which are sketched, and which are not mechanized.

Circularity Check

1 steps flagged · score 4.0 of 10

The formal transparency framework is non-circular and machine-checked, but the practical benchmark partly reuses the Clangover example that guided CT-RetDec's pass selection, making that detection result in-sample.

  1. fitted input called prediction [Section 6.2 (Empirical Transparency) and Section 6.3 (Benchmark Set)]
    "For reflection, we use our test cases from Figures 1 and 9a to 9d. ... Specifically, we include the Clangover vulnerability [44], five vulnerabilities in selection algorithms [51], two vulnerabilities in sorting algorithms [22], the check scalar vulnerability in BearSSL [47] and the CMOVNZ vulnerability in HACL* [47]."

    The CT-RetDec pass configuration is the fitted parameter: Section 6.2 disables every RetDec pass that fails the reflection tests in Figures 1 and 9a-9d. Figure 1 is the Clangover binary, and Section 6.3 then evaluates CT-RetDec on a benchmark that includes ct_clangover, the same vulnerability. Reporting ct_clangover as correctly detected is therefore a restatement of the tuning criterion for that case, not an independent prediction. The other nine vulnerability families in the benchmark were not part of the pass-selection tests, so the circularity is partial; the formal Theorem 2 (mechanized in Rocq) and the negative findings about stock decompilers, CT-Verif, and BinSec do not depend on this in-sample evaluation.

full rationale

The core derivation is not circular. Definition 3 (transparency) is a conjunction of reflection and preservation, and Theorem 2 is a soundness theorem proved in the Rocq artifact; PC-injectivity is a genuinely new condition rather than a restatement of transparency. The per-pass transparency results in Section 5 are proved with explicit simulation relations and observation transformers, and the counterexamples in Section 5.3 are constructed independently. The unsoundness demonstrations for CT-Verif and BinSec are concrete programs whose violations are removed by specific converters, not consequences of the paper's own definitions. The main circularity-adjacent issue is empirical: the pass choices in CT-RetDec were selected using Figures 1 and 9a-9d, and the benchmark in Section 6.3 contains ct_clangover, which is Figure 1. Thus the benchmark's success on that case is partly in-sample and should not be presented as a fully independent confirmation; the paper itself concedes in Section 6 that the empirical tests do not guarantee transparency. Self-citation overlaps (CT-LLVM by two of the authors, CT simulations from [12]) are real but not load-bearing circularity: CT-LLVM is used as an executable analysis backend and [12] supplies prior simulation definitions that this paper extends and mechanizes. Overall, the formal and negative-contribution claims are self-contained; only the practical evaluation has a partial in-sample component, so a moderate score is appropriate.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No fitted numeric parameters appear in the paper; the design choices are pass selections governed by the empirical test suite. The formal results rely on a standard CT leakage model and on several assumed or unproved correctness conditions, including the dead-variable analysis guarantee and well-nested CFG regions for structural analysis.

assumptions (6)
  • domain assumption Observations reveal the program point, memory accesses leak their address, and branches leak their condition (standard CT leakage model).
    Section 3, Leakage and Figure 3; all transparency proofs and counterexamples are relative to this model.
  • standard math Program semantics is deterministic and safe, meaning every non-final state has a successor.
    Section 3, Program Behavior; required for the behavior and simulation definitions.
  • domain assumption Conditional move instructions do not leak their condition (Intel DOIT).
    Used in the If Conversion counterexample (Section 5.3 and Figure 1), where removing a branch is claimed to remove the leak; relies on reference [34].
  • ad hoc to paper Dead-variable annotations D used by Dead Assignment Elimination are correct (Proposition 3), but the paper omits the proof.
    Section 5.2 and Appendix A.3: 'We assume that a previous analysis annotated assignment instructions with a set D of dead variables at that point (we omit the correctness guarantee).' Transparency of this pass depends on it.
  • domain assumption Structural Analysis receives CFGs whose control regions are well-nested and match simple loop and conditional patterns.
    Appendix A.4 imposes well-nestedness and single-entry and single-exit conditions; decompiled binaries may not satisfy these, limiting the theorem's coverage.
  • domain assumption Unspilling assumes no function calls, so the stack pointer is constant, and spills occur at constant offsets.
    Section 5.2, Unspilling: 'recall that we do not consider function calls in our language'.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Decompiling for Constant-Time Analysis." pith.science (2026). https://pith.science/paper/6DTCLJ6J

@misc{pith2026250104183,
  author       = {Pith},
  title        = {Pith review of: Decompiling for Constant-Time Analysis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6DTCLJ6J}},
  note         = {Machine review of arXiv:2501.04183}
}
read the original abstract

The CT programming discipline is commonly used to protect cryptographic libraries against side-channel attacks. However, it is hard to write CT code; moreover, compilers can introduce CT violations. Therefore, it is important to ensure that assembly code is CT. One approach is to show that source programs are CT, and that CT is preserved by compilation. In this paper, we explore the methodological soundness and scalability of the Decompile-then-Analyze (DtA) approach, a less conventional alternative that has been suggested in the broader setting of static analysis. Informally, the DtA approach uses decompilers a front-end for static analysis tools. As a motivation for our study, we show that current decompilers eliminate CT vulnerabilities before CT analysis, leading to non-CT programs being accepted as CT. Independently, we provide *constructed* examples of non-CT, exploitable, programs that are accepted by two popular CT analysis tools; in both cases the culprit are program transformations that are used internally prior to CT analysis and eliminate CT violations. While our examples do not invalidate the general approach of these tools, they emphasize the need for studying the DtA approach. On the methodological side, we define the notion of *CT transparency*. Informally, a program transformation is CT transparent if does not eliminate nor introduce CT violations. We also provide general methods for proving that a transformation is CT transparent, and show that several transformations of interest are transparent. We also sketch an extension of CT transparency to speculative CT, which is used by cryptographic software as a protection against Spectre attacks. On the practical side, we build a CT-transparent version of the popular LLVM-based decompiler RETDEC, and combine it with CT-LLVM, an existing CT verification...

Figures

Figures reproduced from arXiv: 2501.04183 by the authors.

Figure 1
Figure 1. Decompiling Clangover removes the CT vulnerability. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Multi-step execution semantics. or keeps the CT violation. The result is that each of the five decompilers removes CT violations. Therefore, the issue is indeed systematic throughout practical decompilers. 3 Transparency This section reviews the constant-time property using an abstract model of computation and introduces the notion of transparent transformations. We keep the programming language abstract and say tha… view at source ↗
Figure 3
Figure 3. Single-step execution semantics. 5 Transparent and Nontransparent Transformations In this section, we consider the CT transparency of ten common transformations. We prove that seven of them are transparent and provide counterexamples to transparency for the remaining three. We summarize our findings in [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: Relaxed simulation instantiations of 𝑇 , ns, and sf for Dead Branch Elimination. (i) Since the evaluated expressions produce the same value (Proposition 1), every step in the output program matches exactly one step in the input program, and they produce the same regist…
Figure 5
Figure 5. Figure 5: Relaxed simulation instantiations of 𝑇 , ns, and sf for Dead Assignment Elimination. Dead Assignment Elimination. This transformation removes assignments to dead variables, i.e., when the assignments have no impact on the execution of the program. For example, it repla…
Figure 6
Figure 6. Figure 6: Semantics of the CFG language. variables introduced by the transformation; the memories 𝜇 and 𝜇 ′ coincide except on spilled stack offsets; and each spilled offset 𝑛 holds the value of its fresh variable 𝑦, i.e., 𝜇(sp + 𝑛) = 𝜌 ′ (𝑦). Since each output program step is s…
Figure 7
Figure 7. Figure 7: Example CFG patterns. The left pattern corresponds to a while loop, the right one to a conditional. [PITH_FULL_IMAGE:figures/full_fig_p014_7.png]
Figure 8
Figure 8. Figure 8: Loop Rotation duplicates the loop entry and then moves the entry point of the loop by one instruction. [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Counterexamples for nontransparent passes. [PITH_FULL_IMAGE:figures/full_fig_p015_9.png]
Figure 10
Figure 10. Figure 10: Inverse If Conversion. Expression Substitution. This category contains four passes that perform various expression substitution optimizations. Specifically, RetDec invokes constprop, correlated-propagation and scp to propagate constants, and constmerge to merge duplic…
Figure 11
Figure 11. Figure 11: Non-CT program accepted by CT-Verif. 7.1 CT-Verif CT-Verif [6] is a state-of-the-art CT analysis tool for LLVM-IR programs. CT-Verif is based on a product program construction, which is sound (non-CT programs are never deemed CT) and relatively complete (under certain…
Figure 12
Figure 12. Figure 12: Non-CT program accepted by BinSec. Conversion. BinSec lifts a binary program to an IR called DBA (for Dynamic Bitvector Automata) before it performs relational symbolic execution on the DBA program. When lifting a binary program to DBA IR, BinSec converts conditional …

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Fun with flags: How Compilers Break and Fix Constant-Time Code

    cs.CR 2025-07 conditional novelty 6.0 of 10

    Disabling a small set of optimization passes in GCC and LLVM removes the constant-time violations those compilers introduce, at modest average performance cost.

Reference graph

Works this paper leans on

61 extracted references · 38 canonical work pages · cited by 1 Pith paper

  1. [1]

    Vector 35. 2016. Binary Ninja. https://binary.ninja/

    work page 2016

  2. [2]

    2025.Dogbolt

    Vector 35. 2025.Dogbolt. https://dogbolt.org/

    work page 2025

  3. [3]

    Carmine Abate, Roberto Blanco, Ştefan Ciobâcă, Adrien Durier, Deepak Garg, Catalin Hri t,cu, Marco Patrignani, Éric Tanter, and Jérémy Thibault. 2021. An Extended Account of Trace-relating Compiler Correctness and Secure Compilation.ACM Trans. Program. Lang. Syst.43, 4 (2021), 14:1–14:48. doi:10.1145/3460860

    doi:10.1145/3460860 2021

  4. [4]

    Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hrit,cu, Marco Patrignani, and Jérémy Thibault. 2019. Journey Be- yond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019. IEEE, 256–271. doi:10.1109/CSF.2019.00025 Decompiling ...

    arXiv 2019

  5. [5]

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. InProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security(Dallas, Texas, USA) (CCS ’17). Associa...

    arXiv 2017

  6. [6]

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying Constant- Time Implementations. InUSENIX Security. 53–70. https://www .usenix.org/conference/usenixsecurity16/technical- sessions/presentation/almeida

    work page 2016

  7. [7]

    Dennis Andriesse, Xi Chen, Victor van der Veen, Asia Slowinska, and Herbert Bos. 2016. An In-Depth Analysis of Disassembly on Full-Scale x86/x64 Binaries. In25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10-12, 2016, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 583–600. https://www .usenix.org/ conference/usenix...

    work page 2016

  8. [8]

    Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, and Serdar Tasiran. 2018. Sidetrail: Verifying time-balancing of cryptosystems. InVSTTE. 215–228

    work page 2018

Show all 61 references
  1. [10]

    Gilles Barthe, Gustavo Betarte, Juan Campo, Carlos Luna, and David Pichardie. 2014. System-level non-interference for constant-time cryptography. InCCS. 1267–1279

    2014

  2. [11]

    Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2020. Formal verification of a constant-time preserving C compiler.Proc. ACM Program. Lang.4, POPL (2020), 7:1–7:30. doi:10.1145/3371075

    2020 doi

  3. [12]

    Constant-Time

    Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". In31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018. IEEE Computer Soc...

    2018

  4. [13]

    Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2021. Structured Leakage and Applications to Cryptographic Constant-Time and Cost. InCCS ’21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 -...

    2021

  5. [14]

    Zion Leonahenahe Basque, Ati Priya Bajaj, Wil Gibbs, Jude O’Kain, Derron Miao, Tiffany Bao, Adam Doupé, Yan Shoshitaishvili, and Ruoyu Wang. 2024. Ahoy SAILR! There is No Need to DREAM of C: A Compiler-Aware Structuring Algorithm for Binary Decompilation. InUSENIX Security. ht...

    2024

  6. [15]

    Daniel J Bernstein. 2005. Cache-timing attacks on AES. (2005)

    2005

  7. [16]

    Sandrine Blazy, David Pichardie, and Alix Trieu. 2017. Verifying Constant-Time Implementations by Abstract Interpretation. InComputer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I (L...

    2017 doi

  8. [17]

    Rustan M

    Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In26th USENIX Security Symposium, USENIX Security 2017, Vanc...

    2017

  9. [18]

    Schwartz, and Maverick Woo

    David Brumley, JongHyup Lee, Edward J. Schwartz, and Maverick Woo. 2013. Native x86 Decompilation Using Semantics-Preserving Structural Analysis and Iterative Control-Flow Structuring. InUSENIX Security. 353–368. https: //www.usenix.org/conference/usenixsecurity13/technical-se...

    2013

  10. [19]

    Kevin Burk, Fabio Pagani, Christopher Kruegel, and Giovanni Vigna. 2022. Decomperson: How Humans Decompile and What We Can Learn From It. InUSENIX Security. 2765–2782. https://www .usenix.org/conference/usenixsecurity22/ presentation/burk

    2022

  11. [20]

    Luwei Cai, Fu Song, and Taolue Chen. 2024. Towards Efficient Verification of Constant-Time Cryptographic Imple- mentations.Proceedings of the ACM on Software Engineering1, FSE (2024), 1019–1042

    2024

  12. [21]

    Ying Cao, Runze Zhang, Ruigang Liang, and Kai Chen. 2024. Evaluating the Effectiveness of Decompilers. InProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, Vienna, Austria, September 16-20, 2024, Maria Christakis and Micha...

    2024

  13. [22]

    Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2020. Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level. InSP. 1021–1038. doi:10.1109/SP40000.2020.00074

    2020

  14. [23]

    Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2021. Hunting the Haunter - Efficient Relational Symbolic Execution for Spectre with Haunted RelSE. InNDSS. https://www .ndss-symposium.org/ndss-paper/hunting-the- haunter-efficient-relational-symbolic-execution-for-spectre-...

    2021

  15. [24]

    Craig Disselkoen, Sunjay Cauligi, Dean Tullsen, and Deian Stefan. 2020. Finding and eliminating timing side-channels in crypto code with pitchfork. InTECHCON

    2020

  16. [25]

    Schwartz, Bogdan Vasilescu, and Claire Le Goues

    Luke Dramko, Jeremy Lacomis, Edward J. Schwartz, Bogdan Vasilescu, and Claire Le Goues. 2024. A Taxonomy of C Decompiler Fidelity Issues. InUSENIX Security. https://www .usenix.org/conference/usenixsecurity24/presentation/ dramko

    2024

  17. [26]

    Vijay D’Silva, Mathias Payer, and Dawn Xiaodong Song. 2015. The Correctness-Security Gap in Compiler Optimization. In2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, May 21-22, 2015. IEEE Computer Society, 73–87. doi:10.1109/SPW.2015.33

    2015 doi

  18. [27]

    Behner, Niklas Bergmann, Mariia Rybalka, Elmar Padilla, Er Xue Hui, Henry Low, and Nicholas Sim

    Steffen Enders, Eva-Maria C. Behner, Niklas Bergmann, Mariia Rybalka, Elmar Padilla, Er Xue Hui, Henry Low, and Nicholas Sim. 2022. dewolf: Improving Decompilation by leveraging User Surveys.CoRRabs/2205.06719 (2022). arXiv:2205.06719 doi:10.48550/ARXIV.2205.06719

    2022 doi arXiv

  19. [28]

    Felix Engel, Rainer Leupers, Gerd Ascheid, Max Ferger, and Marcel Beemster. 2011. Enhanced structural analysis for C code reconstruction from IR code. In14th International Workshop on Software and Compilers for Embedded Systems, SCOPES ’11, St. Goar, Germany, June 27-28, 2011,...

    2011

  20. [29]

    Antoine Geimer and Clementine Maurice. 2025. Fun with flags: How Compilers Break and Fix Constant-Time Code. arXiv preprint arXiv:2507.06112(2025)

    2025 arXiv

  21. [30]

    Antoine Geimer, Mathéo Vergnolle, Frédéric Recoules, Lesly-Ann Daniel, Sébastien Bardin, and Clémentine Maurice

  22. [31]

    Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware-Software Contracts for Secure Speculation. In42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. IEEE, 1868–1883. doi:10.1109/SP40001.2021.00036

    2021

  23. [32]

    Andrea Gussoni, Alessandro Di Federico, Pietro Fezzardi, and Giovanni Agosta. 2020. A Comb for Decompiled C Code. InASIA CCS ’20: The 15th ACM Asia Conference on Computer and Communications Security, Taipei, Taiwan, October 5-9, 2020, Hung-Min Sun, Shiuh-Pyng Shieh, Guofei Gu,...

    2020

  24. [33]

    Hex-Rays. 2023. Ida Pro. https://www.hex-rays.com/products/ida

    2023

  25. [34]

    2023.Data Operand Independent Timing Instructions

    Intel. 2023.Data Operand Independent Timing Instructions. https://www .intel.com/content/www/us/en/developer/ articles/technical/software-security-guidance/resources/data-operand-independent-timing-instructions .html Ac- cessed: 2025-10-06

    2023

  26. [35]

    They’re not that hard to mitigate

    Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. 2022. "They’re not that hard to mitigate": What Cryptographic Library Developers Think About Timing Attacks. In43rd IEEE Symposium on Security...

    2022

  27. [36]

    Paul C. Kocher. 1996. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Advances in Cryptology – CRYPTO’96 (LNCS, Vol. 1109). SV, 104–113. http://www .cryptography.com/public/pdf/ TimingAttacks.pdf

    1996

  28. [37]

    Jakub Křoustek, Peter Matula, and Petr Zemek. 2017. Retdec: An open-source machine-code decompiler. https: //github.com/avast/retdec

    2017

  29. [38]

    Zhibo Liu and Shuai Wang. 2020. How far we have come: testing decompilation correctness of C decompilers. In ISSTA ’20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, USA, July 18-22, 2020, Sarfraz Khurshid and Corina S. Pasareanu (Ed...

    2020

  30. [39]

    Zhibo Liu, Yuanyuan Yuan, Shuai Wang, and Yuyan Bao. 2022. SoK: Demystifying Binary Lifters Through the Lens of Downstream Applications. In43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 1100–1119. doi:10.1109/SP46214.2022.9833799

    2022

  31. [40]

    Alessandro Mantovani, Luca Compagna, Yan Shoshitaishvili, and Davide Balzarotti. 2022. The Convergence of Source Code and Binary Vulnerability Discovery - A Case Study. InASIA CCS ’22: ACM Asia Conference on Computer and Communications Security, Nagasaki, Japan, 30 May 2022 - ...

    2022

  32. [41]

    James Mattei, Madeline McLaughlin, Samantha Katcher, and Daniel Votipka. 2022. A Qualitative Evaluation of Reverse Engineering Tool Usability. InAnnual Computer Security Applications Conference, ACSAC 2022, Austin, TX, USA, December 5-9, 2022. ACM, 619–631. doi:10.1145/3564625.3567993

    2022

  33. [42]

    David Molnar, Matt Piotrowski, David Schultz, and David A. Wagner. 2005. The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks. InInformation Security and Cryptology - ICISC 2005, 8th International Conference, Seoul, Korea, De...

    2005 doi

  34. [43]

    National Security Agency (NSA). 2018. Ghidra. https://www.nsa.gov/resources/everyone/ghidra/

    2018

  35. [44]

    2024.Clangover CVE

    Antoon Purnal. 2024.Clangover CVE. https://nvd.nist.gov/vuln/detail/CVE-2024-37880 Accessed: 2025-10-03

    2024

  36. [45]

    Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implemen- tations. InComputer Aided Verification - 26th International Conference, CA V 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 20...

    2014 doi

  37. [46]

    Bruno Rodrigues, Fernando Magno Quintão Pereira, and Diego F. Aranha. 2016. Sparse representation of implicit flows with applications to side-channel detection. InCC. 110–120. doi:10.1145/2892208.2892230

    2016

  38. [47]

    Moritz Schneider, Daniele Lain, Ivan Puddu, Nicolas Dutly, and Srdjan Capkun. 2024. Breaking Bad: How Compilers Break Constant-Time Implementations. arXiv:2410.13489 [cs.CR] https://arxiv.org/abs/2410.13489

    2024 arXiv

  39. [48]

    Eric Schulte, Jason Ruchti, Matt Noonan, David Ciarletta, and Alexey Loginov. 2018. Evolving exact decompilation. In Workshop on Binary Analysis Research (BAR)

    2018

  40. [49]

    Schwartz and JongHyup Lee

    Edward J. Schwartz and JongHyup Lee. 2013. Decompilation of Binary Programs Using Control-Flow Structur- ing and Semantic-Preserving Transformations. InUSENIX Security. 369–384. https://www .usenix.org/conference/ usenixsecurity13/technical-sessions/presentation/schwartz

    2013

  41. [50]

    Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Krügel, and Giovanni Vigna. 2016. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis. InSP. 138–157. doi...

    2016 doi

  42. [51]

    Anderson

    Laurent Simon, David Chisnall, and Ross J. Anderson. 2018. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. In2018 IEEE European Symposium on Security and Privacy, EuroS&P 2018, London, United Kingdom, April 24-26, 2018. IEEE, 1–15. doi:10.1109/E...

    2018

  43. [52]

    Chungha Sung, Brandon Paulsen, and Chao Wang. 2018. CANAL: a cache timing analysis framework via LLVM transformation. InProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (Montpellier, France)(ASE ’18). Association for Computing Machine...

    2018

  44. [53]

    Bockenek, Zhoulai Fu, and Binoy Ravindran

    Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, and Binoy Ravindran. 2022. Formally verified lifting of C-compiled x86-64 binaries. InPLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, R...

    2022

  45. [54]

    Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, and Dinghao Wu. 2019. Identifying Cache-Based Side Channels through Secret-Augmented Abstract Interpretation. InUSENIX Security. 657–674. https://www .usenix.org/ conference/usenixsecurity19/presentation/wang-shuai

    2019

  46. [55]

    Jianhao Xu, Kangjie Lu, Zhengjie Du, Zhu Ding, Linke Li, Qiushi Wu, Mathias Payer, and Bing Mao. 2023. Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs. In32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calan...

    2023

  47. [56]

    Khaled Yakdan, Sergej Dechand, Elmar Gerhards-Padilla, and Matthew Smith. 2016. Helping johnny to analyze malware: A usability-optimized decompiler and malware analysis user study. In2016 IEEE Symposium on Security and Privacy (SP). IEEE, 158–177

    2016

  48. [57]

    Khaled Yakdan, Sebastian Eschweiler, Elmar Gerhards-Padilla, and Matthew Smith. 2015. No More Gotos: De- compilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations. In NDSS. https://www .ndss-symposium.org/ndss2015/no-more-gotos-deco...

    2015

  49. [58]

    Zhiyuan Zhang and Gilles Barthe. 2025. CT-LLVM: Automatic Large-Scale Constant-Time Analysis. Cryptology ePrint Archive, Paper 2025/338. https://eprint.iacr.org/2025/338

    2025

  50. [59]

    Anshunkang Zhou, Chengfeng Ye, Heqing Huang, Yuandao Cai, and Charles Zhang. 2024. Plankton: Reconciling Binary Code and Debug Information. InProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2...

    2024

  51. [60]

    Quan Zhou, Sixuan Dang, and Danfeng Zhang. 2024. CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming. InECOOP (LIPIcs, Vol. 313). 46:1–46:26. doi:10.4230/LIPICS.ECOOP.2024.46

    2024 doi

  52. [61]

    Muqi Zou, Arslan Khan, Ruoyu Wu, Han Gao, Antonio Bianchi, and Dave (Jing) Tian. 2024. D-Helix: A Generic Decompiler Testing Framework Using Symbolic Differentiation. In33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024, Davide Balz...

    2024

  53. [2023]

    A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic Libraries. InCCS. ACM, 1690–1704. doi:10.1145/3576915.3623112

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.