{"id":"055baee6-bcb1-4086-bdf8-962d295d5f2e","arxiv_id":"2501.04183","paper_version":4,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"partial","parameter_count":0,"one_line_summary":"Decompilation can silently erase constant-time violations, so the paper defines CT transparency and builds CT-RetDec, a RetDec variant that finds violations other decompilers miss.","lead":"This paper shows that decompilers, which turn binaries back into readable code, can erase the very security flaws that constant-time analysis is meant to find. It formalizes a standard called CT transparency and builds a modified decompiler that keeps those flaws visible.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"CT-RetDec's pass selection uses the same hand-crafted violation patterns that appear in the 160-binary benchmark, so the practical claim of reliable detection is partly in-sample and not yet shown to generalize.","rationale":"The reader's CONDITIONAL verdict is well calibrated. The strongest parts of the paper—the formal definition of CT transparency, the PC-injectivity simulation technique, and the machine-checked Theorem 2—are supported by the artifact and do not hinge on the empirical evaluation. The counterexamples against stock decompilers and the CT-Verif/BinSec converters are concrete and persuasive. The soft spot is the generalization of CT-RetDec. Passes were chosen by testing on five reflection patterns and one preservation pattern; the benchmark includes one of those patterns (Clangover) and is the same style of compiler-induced vulnerability. Thus the 160-binary evaluation is partly a validation of the tuning set, not an independent assessment. An out-of-sample evaluation with a different compiler and optimization level would settle whether the configuration is genuinely transparent for new code. If it fails, the paper's practical claim should be weakened to 'evidence of improved detection on a benchmark,' while the formal contribution stands. This does not change the reader's verdict, which already conditions on addressing this issue.","tokens_in":32534,"tokens_out":14109,"duration_ms":158865,"concrete_test":"Freeze the CT-RetDec pass configuration exactly as selected in §6.2 and run it on an out-of-sample corpus assembled from the Breaking Bad dataset [47] (e.g., BearSSL and HACL* snippets) compiled with GCC-12 at -O2, a toolchain absent from Table 3, with ground truth established by independent manual assembly review. Compare CT-RetDec's verdicts against that ground truth on every binary; any missed known CT violation would show the pass configuration does not generalize, while a perfect match would address the in-sample concern.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The practical pillar of the paper—that CT-RetDec 'correctly detects CT violations on a benchmark of 160 binaries'—rests on a pass configuration chosen in §6.2 by empirical transparency tests over the patterns in Figures 1 and 9a–9d plus one preservation test (Figure 10). Section 6.3's benchmark then includes ct_clangover, the same Clangover pattern used to guide the modifications, among its compiler-induced vulnerabilities. The paper itself states in §6 that the empirical tests do not guarantee passes are transparent, and the benchmark is at least partly in-sample for the pass-selection procedure. Because the selection process is manual and incremental, the 160-binary results are not an independent test of the hypothesis that disabling those ten passes yields a transparent decompiler; they show that the chosen configuration handles a set that overlaps with the tuning set. This is load-bearing for RQ3 and for the claim that CT-RetDec is suitable for real-world binaries. The formal framework (Theorem 2, mechanized in Rocq) and the negative results about stock decompilers and CT-Verif/BinSec do not depend on this generalization, so the concern is limited to the practical contribution.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":32770,"tokens_out":8894,"duration_ms":97576,"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":[{"comment":"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.","section":"§6.2–6.3, Table 3"},{"comment":"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.","section":"§5.2, Theorem 5 and Appendix A.3, Proposition 3"},{"comment":"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.","section":"§6 and §9"}],"minor_comments":[{"comment":"The caption contains the typo \"CT-RetDEc\" instead of \"CT-RetDec.\"","section":"Table 3"},{"comment":"The RetDec Utility Passes list contains retdec-value-protect twice, which makes the table of passes harder to read.","section":"Appendix B"},{"comment":"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.","section":"§6.2"},{"comment":"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.","section":"Appendix A"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth your time: the formal part is solid and the negative result on decompilers is real. The paper defines CT transparency as reflection plus preservation, extends CT simulations with PC-injectivity, and mechanizes the soundness theorem in Rocq. That is a genuine contribution. It reframes Decompile-then-Analyze as needing a transparency guarantee, not just semantic preservation, and it gives a reusable proof technique. The demonstrations that stock decompilers and the internal converters of CT-Verif and BinSec can drop CT violations are convincing and independently valuable, even if the examples are constructed.\n\nThe soft spot is exactly where the stress-test points. The pass configuration for CT-RetDec is chosen by empirical transparency tests over the same violation patterns that later appear in the 160-binary benchmark, and the benchmark includes the original Clangover case. The paper itself says in Section 6 that the empirical tests do not guarantee transparency. So the headline practical claim — that CT-RetDec reliably detects CT violations on 160 binaries — is not yet an independent generalization. It is an existence proof that a RetDec with ten passes disabled avoids the specific failures in that benchmark. That is still useful, but it is not the same as showing the configuration is transparent on unseen binaries.\n\nA smaller issue: the correctness guarantee for the dead-variable analysis in the Dead Assignment Elimination proof is stated as an assumption rather than proved. The general theorem is in the Rocq artifact, and the proof sketch is clear, but the omitted guarantee is a real gap in the appendix.\n\nNone of this undermines the formal framework. Theorem 2 is machine-checked, and the transformation proofs are detailed. The negative results about existing tools are independent of the in-sample issue. What is load-bearing is the practical claim of reliable detection, and that needs either an out-of-sample evaluation or an explicit statement that CT-RetDec is a tuned prototype rather than a verified transparent decompiler. On the citation front: the analysis backend is by two of the authors, but the paper's negative results are against stock tools and the formal theorem is in the artifact, so I do not see the self-reference as load-bearing.\n\nWho should read it: anyone working on binary-level CT verification, decompiler correctness, or secure compilation. It deserves a serious referee; the formal contribution and the empirical demonstration of unsoundness in current tools are worth referee time even if the practical section needs revision. I would bring it to the reading group and would cite the transparency definition in my own work.","headline":"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.","tokens_in":33278,"tokens_out":1871,"would_cite":true,"duration_ms":20578,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["constant-time","decompilation","CT transparency","side-channel analysis","RetDec","LLVM IR","secure compilation","static analysis"],"falsifier":"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.","tokens_in":32356,"feed_emoji":"🔓","tokens_out":7496,"duration_ms":70322,"temperature":0.7,"pith_summary":"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.","feed_headline":"Decompilers erase timing leaks, fooling constant-time checks","feed_subtitle":"A transparency criterion and a hardened RetDec catch all 160 test-binary violations.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the CT-Verif analyzer used in the motivating example and later shown to accept non-CT programs because its SMACK conversion removes dead loads.","marker":"[6]"},{"why":"Introduces the CT simulation technique that the paper extends with PC-injectivity to prove both reflection and preservation.","marker":"[12]"},{"why":"Supplies BinSec/Rel, the binary analysis tool whose non-transparent internal conversion is demonstrated, and contributes sorting-algorithm benchmark vulnerabilities.","marker":"[22]"},{"why":"RetDec is the decompiler that the paper modifies by disabling non-transparent passes to build CT-RetDec.","marker":"[37]"},{"why":"Documents the Clangover CVE-2024-37880 vulnerability that motivates the paper and is one of the benchmark cases.","marker":"[44]"},{"why":"SMACK is the converter inside CT-Verif that performs the non-transparent dead-load and dead-store elimination.","marker":"[45]"},{"why":"Supplies the BearSSL check-scalar and HACL* CMOVNZ vulnerabilities used in the benchmark.","marker":"[47]"},{"why":"Supplies the selection-algorithm compiler-induced vulnerabilities used in the 160-binary benchmark.","marker":"[51]"},{"why":"Provides the CT-LLVM analyzer paired with the modified RetDec in the CT-RetDec toolchain.","marker":"[58]"}],"fun_headline_variants":["Decompilers hide timing leaks, foiling constant-time checks","CT transparency needed: decompilers mask side-channel leaks","Hardened RetDec exposes all constant-time violations","Why decompilers undermine constant-time verification","Decompile-then-Analyze fails without CT transparency"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Decompilers hide timing leaks, foiling constant-time checks","CT transparency needed: decompilers mask side-channel leaks","Hardened RetDec exposes all constant-time violations","Why decompilers undermine constant-time verification","Decompile-then-Analyze fails without CT transparency"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000342,"raw_usage":{"total_tokens":1936,"prompt_tokens":1054,"completion_tokens":882,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":670,"completion_tokens_details":{"reasoning_tokens":807}},"tokens_in":670,"tokens_out":882,"duration_ms":6673,"temperature":1.0,"reasoning_tokens":807,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:39:36.752129+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the CT-Verif analyzer used in the motivating example and later shown to accept non-CT programs because its SMACK conversion removes dead loads."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"RetDec is the decompiler that the paper modifies by disabling non-transparent passes to build CT-RetDec."},{"cited_title":"2024.Clangover CVE","cited_arxiv_id":null,"evidence_quote":"Documents the Clangover CVE-2024-37880 vulnerability that motivates the paper and is one of the benchmark cases."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the CT-LLVM analyzer paired with the modified RetDec in the CT-RetDec toolchain."}],"review_version":1}