{"id":"0bb90b08-f5c9-4d4b-b448-19ffa34ae914","arxiv_id":"2506.13323","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":8,"one_line_summary":"Tady enforces disassembly validity by detecting and pruning instructions that violate post-dominance and non-overlap constraints, while reporting instruction-level accuracy close to strong baselines.","lead":"This paper describes Tady, a neural disassembler that uses post-dominance relations in a control-flow graph to detect and prune structurally invalid instructions. It reports that the resulting disassembly has no overlapping instructions, dead-end sequences, or missing post-dominators while keeping instruction-level accuracy close to existing tools.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Non-overlap is not actually enforced across weakly connected components or for control-flow/non-control-flow pairs, so the pruning guarantee can fail.","rationale":"The reader's identified assumption (PDT semantic fidelity, Section 2.2) is real but secondary: even if post-dominance were exact, the pruning algorithm would still not enforce non-overlap in the cross-WCC or CF/NCF cases. The paper's own E3 definition and Algorithm 3 only prevent a node from having multiple true NCF children, which is a local sibling condition. Overlapping instructions can be separated by control flow or by WCC boundaries, so no PDT node ever sees both. This makes the headline claim false as an unconditional statement, not merely dependent on an imperfect graph. The paper's contributions remain useful: the error detection finds many real label/tool errors, and the pruning improves consistency for common cases. A conditional verdict is appropriate: require either a proof that Algorithm 3 enforces byte-interval non-overlap, an explicit overlap-resolution pass, or a qualified claim that non-overlap is enforced only for the detected sibling pattern. The concrete test above would settle whether the gap actually manifests; if both instructions survive, the current 'completely eliminate' claim must be revised.","tokens_in":25031,"tokens_out":10268,"duration_ms":103127,"concrete_test":"Using the released artifact, run the pruning post-processor on the minimal .text byte sequence E9 01 00 00 00 01 00 C3 90 C3, with positive weights assigned to both 0x100 (jmp 0x106) and 0x101 (add [rax],eax), and appropriate weights for 0x103, 0x105, and 0x106. Inspect the final pruned output: if both 0x100 and 0x101 are emitted, the non-overlap guarantee is disproved. Independently verify by comparing the byte intervals of every emitted instruction pair; any overlap contradicts the abstract's claim. This check isolates pruning behavior from model-score effects.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The abstract and Section 7 claim Tady 'completely eliminate[s]' structural constraint violations, including overlapping instructions. The enforcement, however, only catches overlaps that manifest as multiple true non-control-flow children of a single PDT node (Algorithm 1, E3; Algorithm 3, maxFT selection). This is a sufficient test for one local pattern, but not a necessary condition for non-overlap. The superset CFG (Section 2.2) contains only control-flow edges, so two valid instructions whose byte intervals overlap can reside in different weakly connected components, or one can be a control-flow instruction and the other non-control-flow; they then never share a PDT parent and are never compared. Example bytes: E9 01 00 00 00 01 00 C3 90 C3. The chain 0x100 jmp 0x106 and the chain 0x101 add [rax],eax; 0x103 ret are separate WCCs. Each parent has at most one NCF child, so Algorithm 3 can retain both when both scores are positive, producing overlapping instructions in the final disassembly. The 'no violations' result is therefore an artifact of the PDT's sibling structure, not a guarantee about byte-interval non-overlap.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper introduces Tady, a neural disassembler for x86/x86-64 that combines a transformer-based model with a post-dominator tree (PDT) based post-processing step. The authors formalize three structural constraint violations (missing post-dominator, dead-end sequence, overlapping instructions), show that such violations appear in the outputs of existing neural and rule-based disassemblers and even in dataset labels, and propose a linear-time violation detection algorithm. The post-processing step prunes the PDT to remove inconsistent nodes while maximizing the sum of confidence scores, and the authors claim this completely eliminates all structural constraint violations. Evaluation on Pangine, Assemblage, x86-sok, RW, Obf-Benchmark, and Quarks shows competitive F1 scores and high efficiency. The paper also releases code and models.","tokens_in":25276,"tokens_out":8871,"duration_ms":83280,"significance":"If the central claim were correct, Tady would be a practically important contribution: a fast, learning-based disassembler whose output is guaranteed to satisfy basic structural soundness, with a reusable post-processing step for other neural disassemblers. The paper has clear strengths: the algorithms are specified in sufficient detail to reproduce, the evaluation covers diverse datasets including obfuscated binaries, the detection tool finds real label errors without ground truth, and the artifact is publicly released. However, the guarantee of complete elimination of violations is not actually delivered by the pruning algorithm as described, which limits the significance of the main claim to the narrower set of constraints that the PDT sibling structure can express.","major_comments":[{"comment":"The pruning algorithm enforces non-overlap only by keeping at most one non-control-flow (NCF) child per PDT node (Algorithm 3, lines 11–15 and 21–25). This is insufficient to guarantee the absence of overlapping instructions. Two overlapping instructions need not be siblings under the PDT: they can lie in different weakly connected components (e.g., an unconditional jump at 0x100 and an overlapping instruction starting at 0x101, with separate WCCs because call edges are omitted and no control-flow edge connects them), or one can be a control-flow instruction and the other a non-control-flow instruction at different depths. In both cases no PDT node has two NCF children, so both candidates are retained if their scores are positive, and the final output contains overlapping instructions. Consequently, the abstract and Section 7 claims that Tady 'eliminates' or 'completely eliminates' structural constraint violations are not supported by the algorithm as described; at most it eliminates the specific pattern of multiple NCF siblings under one PDT node, and no overlap that is not of that form.","section":"Section 2.2 and Algorithm 3"},{"comment":"Because the pruning guarantee is incomplete, the sentence 'Since our pruning algorithm eliminates all of the violations, we report the error rate before pruning' overstates the result. The after-pruning violation counts, in particular overlapping-instruction counts, should be reported. The current Table 1 gives only before-pruning error rates, so the reader cannot verify the central claim. This is not purely cosmetic: the counterexample in the previous comment shows that after-pruning OI violations can remain, so the reported numbers would not be zero in general, and Table 2's OI statistics, which rely on the same E3 sibling-check, likely undercount the true number of overlapping-instruction errors in the labels.","section":"Section 4.2"},{"comment":"The paper itself concedes that the post-dominance assumption underlying the constraints fails for signal-based hardware exceptions. This is a legitimate scoping statement, but it contradicts the unconditional wording used in the abstract ('without structural constraint violations') and in the conclusion ('completely eliminate the violations'). The claims need to be restated with the scope that the paper actually establishes, and the algorithm should be described as enforcing constraints modulo the admitted exception, not as eliminating all possible violations.","section":"Section 5"},{"comment":"The statement that the pruned tree 'represents a valid disassembly solution that maximizes confidence scores while satisfying all structural constraints' is ambiguous. The dynamic program in Algorithms 2–3 maximizes the sum of scores subject to the two invariants it actually encodes (path integrity and at most one NCF child per node), not subject to the full non-overlap constraint as defined in Section 2.1. Because the constraint set is not fully enforced, the optimality claim should be scoped to the implemented invariants rather than to 'all structural constraints'.","section":"Section 3.2"}],"minor_comments":[{"comment":"The caption should define the 'B' and 'A' states as before and after pruning, and it should explain that TadyA is the model trained on the composite dataset, since the name first appears in the table without definition in the main text.","section":"Table 3"},{"comment":"The dataset name is written inconsistently as 'x86-sok' in the text and 'X86-Sok' in Tables 1 and 2; please unify the spelling.","section":"Throughout"},{"comment":"The workflow description says the superset CFG edges include call edges, while Section 2.2 says call edges are not connected during WCC construction; this apparent contradiction should be clarified so the reader understands that call edges are present in the CFG but deliberately omitted for the PDT construction.","section":"Sections 2.2 and 3"},{"comment":"The description of the reachability mask says collection 'stops when encountering conditional jumps for simplicity'; this design choice may limit the mask's ability to represent long-range reachability, and it would be helpful to state its impact on the model's capability.","section":"Section 3.1.2"}],"recommendation":"major_revision","confidential_remarks":"As stated, the abstract's central claim is not supported by the pruning algorithm, which fails to enforce non-overlap across weakly connected components and across control-flow/non-control-flow pairs. However, the flaw is local and fixable, for instance by adding a global overlap check after pruning or by re-scoping the claims to the invariants actually enforced. The paper has merit, particularly the efficient PDT-based detection and the artifact release, and I would support publication after major revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things you should know about arXiv:2506.13323. First, the post-dominator tree as a backbone for disassembly consistency is genuinely new and pays off in practice. Second, the headline claim—that Tady \"completely eliminates\" structural constraint violations—does not survive contact with the algorithm. Non-overlap is only enforced when multiple true non-control-flow children share a single PDT parent. Overlapping instructions that live in different weakly connected components, or that pair a control-flow instruction with a non-control-flow instruction, are never compared. The stress-test example is valid: bytes E9 01 00 00 00 01 00 C3 90 C3 produce a jmp at 0x100 targeting 0x106 and an add at 0x101 with a ret at 0x103; those two chains sit in separate WCCs and both survive pruning. The \"no violations\" result is an artifact of the PDT's sibling structure, not a guarantee about byte intervals.\n\nWhat is genuinely good: the PDT is a better organizing structure than the pairwise constraints in Pdisasm, D-Arm, or the WIS approach in ddisasm-WIS. Detection is linear-time, which matters at superset scale. The pruning algorithm is a clean dynamic program, and the ablation shows the masked reachability attention contributes. The evaluation is broad—six benchmarks, obfuscated binaries, a VMProtect case—and the artifacts are public. Showing that the pruner can improve other disassemblers' outputs, especially XDA, is a practical result worth having.\n\nWhere it's soft: the paper oversells. Section 5 honestly admits the exception-handling caveat, but the cross-component overlap gap is not acknowledged. The evaluation also excludes timeouts and crashes per tool, which can bias comparisons depending on how tools fail. And reporting \"zero violations\" after pruning is not an empirical measurement; it's a restatement of the algorithm's definition. That's acceptable if framed as \"enforced by construction,\" but the paper doesn't frame it that way. The PDT also depends on a superset CFG with call edges omitted; the constraints are only as meaningful as that graph.\n\nWho this is for: anyone building or benchmarking neural disassemblers, and the dataset-label error detection angle is useful to the binary-analysis community. The core is sound for ordinary compiled code; the issues are fixable by weakening the claim, adding an independent violation check, and either handling cross-component/CF-NCF overlaps or explicitly scoping them out. I would send it to serious peer review and push for major revision on those points.","headline":"A genuinely new PDT-based approach to disassembly consistency, but the 'zero violations' claim only holds for the patterns the PDT happens to catch; cross-component and CF/NCF overlaps get through.","tokens_in":25820,"tokens_out":4163,"would_cite":true,"duration_ms":38494,"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":"Tady claims that post-dominance-based pruning eliminates all structural constraint violations in neural disassembly while preserving instruction-level accuracy.","keywords":["binary disassembly","post-dominator tree","structural constraints","neural disassembler","control-flow integrity","dynamic programming pruning","reverse engineering","x86-64"],"falsifier":"Construct a small x86-64 binary whose function installs a signal handler, cause a division-by-zero after a fall-through instruction, and run Tady; if the handler entry is pruned or the fall-through successor is forced to remain, the post-dominator assumption is violated and the no-violations guarantee does not correspond to real execution. The paper itself identifies signal-based control flow as a limitation, so this is the sharpest place to test the claim.","tokens_in":24804,"feed_emoji":"🛠️","tokens_out":6627,"duration_ms":61806,"temperature":0.7,"pith_summary":"This paper tries to establish that the structural failures common in neural disassembly—missing jump targets, dead-end instruction sequences, and overlapping instructions—can be characterized by post-dominance relations, detected in linear time, and eliminated by construction through a pruning step. The proposed system, Tady, combines a trace-aware neural model with a post-dominator-tree-based post-processor, and reports that its final output has zero structural constraint violations while keeping instruction-level precision and recall competitive with existing rule-based and neural disassemblers. A sympathetic reader would care because disassembly consistency, not just per-instruction accuracy, is what downstream tools such as decompilers and binary similarity detectors actually consume; outputs that violate control-flow structure are unusable no matter how high their F1 score looks. The same detection machinery also exposes errors in existing dataset labels that had previously been treated as ground truth.","feed_headline":"One tree enforces valid disassembly, with no structural violations","feed_subtitle":"A post-dominator tree and dynamic-programming pruning remove broken paths and overlapping instructions from neural disassembly output.","key_machinery":"The load-bearing object is the post-dominator tree (PDT) of the superset control-flow graph, in which every byte address is a candidate instruction node and each weakly connected component is rooted at an artificial virtual exit. Because post-dominance captures 'every path from a node to the exit,' a false node above a true node is proof of a broken path, and two true non-control-flow children under one parent are proof of overlap. The dynamic-programming pruning algorithm—weight propagation upward through the tree followed by breadth-first collection—selects the maximum-confidence subtree that respects the tree's structure, which is what turns probabilistic predictions into a guaranteed-consistent disassembly.","core_discovery":"On the paper's own terms, the central claim is that a valid disassembly is exactly a subset of candidate instructions whose post-dominator tree satisfies two properties—path integrity, where every true instruction's ancestors up to the root are true, and non-overlap, where no node has two true non-control-flow children—and that the disassembly problem can be regularized by enforcing these properties on a superset control-flow graph. Tady builds the post-dominator tree of the superset graph, assigns every candidate node a neural confidence score, and then solves a maximum-weight subtree problem over that tree using dynamic programming. The paper reports that this removes 100 percent of the detected structural violations in Tady's output across all evaluated binaries, including obfuscated ones, and that the same post-processor also cleans the outputs of other neural disassemblers while often improving their F1 scores.","pith_inferences":["A natural next test, beyond the paper, is whether the same post-dominator pruning transfers to other instruction set architectures; the constraints as formulated are architecture-agnostic, but the paper only evaluates x86 and x86-64 binaries.","The guarantee is conditional on the quality of the superset control-flow graph: if real execution can follow a path the graph omits, such as signal-handler transfer, pruning can still declare a valid output that is invalid with respect to the actual hardware. The paper acknowledges this for exception-induced control flow but does not model it.","A testable extension is to use the violation detector as a training-signal generator: relabel the false positives and false negatives it finds in training corpora and retrain the model, which should reduce the residual errors that pruning currently has to clean up."],"forward_implications":["Downstream tools can consume Tady's output without first repairing control-flow graphs, since path integrity and non-overlap hold by construction.","The post-dominator traversal becomes a cheap, label-free quality gate: it flags labeling errors in disassembly datasets, so dataset maintainers can locate false positives and false negatives without a second tool.","The pruning step is a drop-in regularizer for neural disassemblers: feeding another model's scores through the same maximum-weight-subtree procedure removes structural violations and, in most reported cases, raises F1 rather than lowering it.","Because the whole pipeline is linear in binary size, consistency enforcement does not change the practical scalability of superset disassembly."],"supporting_citations":[{"why":"Supplies the Lengauer-Tarjan algorithm adapted to compute immediate post-dominators for the superset CFG.","marker":"[19]"},{"why":"The graph-neural-network disassembler that motivates the constraint framework and provides the main neural baseline.","marker":"[46]"},{"why":"The sequence-model disassembler used as a neural baseline; its output is shown to improve after the pruning step.","marker":"[32]"},{"why":"The Datalog-based rule disassembler used as a rule-based baseline.","marker":"[8]"},{"why":"Prior work modeling disassembly as weighted interval scheduling with learned weights, and an earlier observation that dataset labels contain errors.","marker":"[7]"},{"why":"The x86-Sok dataset whose labels Tady's detector shows to contain widespread violations, motivating the dataset-error contribution.","marker":"[31]"},{"why":"The Pangine dataset, with labels derived from compilation intermediates, used to train the model.","marker":"[20]"},{"why":"The binary-level anti-disassembly obfuscation benchmark used to show that all disassemblers, including rule-based ones, violate constraints under obfuscation.","marker":"[24]"}],"fun_headline_variants":["Tady: Neural disassembly with zero structural violations","Post-dominance tree pruning yields valid disassembly","No structural violations: Tady's post-dominator constraint","Tady enforces post-dominance for valid disassembly","Structural constraints eliminate invalid disassembly paths"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The central assumption is that the post-dominator tree built from a superset graph, in which call edges are omitted, indirect jumps may be unresolved, and each weakly connected component is given an artificial exit, faithfully represents the binary's real execution paths; if that graph is wrong, the pruning guarantee only certifies consistency with the wrong graph.","fun_headline_variants_meta":{"raw":{"variants":["Tady: Neural disassembly with zero structural violations","Post-dominance tree pruning yields valid disassembly","No structural violations: Tady's post-dominator constraint","Tady enforces post-dominance for valid disassembly","Structural constraints eliminate invalid disassembly paths"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000649,"raw_usage":{"total_tokens":2934,"prompt_tokens":857,"completion_tokens":2077,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":473,"completion_tokens_details":{"reasoning_tokens":2000}},"tokens_in":473,"tokens_out":2077,"duration_ms":14509,"temperature":1.0,"reasoning_tokens":2000,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:04:52.280524+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a small x86-64 binary whose function installs a signal handler, cause a division-by-zero after a fall-through instruction, and run Tady; if the handler entry is pruned or the fall-through successor is forced to remain, the post-dominator assumption is violated and the no-violations guarantee does not correspond to real execution. The paper itself identifies signal-based control flow as a limitation, so this is the sharpest place to test the claim.","supporting_citations":[{"cited_title":"A fast algorithm for finding dominators in a flowgraph","cited_arxiv_id":null,"evidence_quote":"Supplies the Lengauer-Tarjan algorithm adapted to compute immediate post-dominators for the superset CFG."},{"cited_title":"DeepDi: Learning a relational graph convolutional network model on instructions for fast and accurate disassem- bly","cited_arxiv_id":null,"evidence_quote":"The graph-neural-network disassembler that motivates the constraint framework and provides the main neural baseline."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The Datalog-based rule disassembler used as a rule-based baseline."},{"cited_title":"Disas- sembly as Weighted Interval Scheduling with Learned Weights","cited_arxiv_id":null,"evidence_quote":"Prior work modeling disassembly as weighted interval scheduling with learned weights, and an earlier observation that dataset labels contain errors."},{"cited_title":"SoK: All you ever wanted to know about x86/x64 bi- nary disassembly but were afraid to ask","cited_arxiv_id":null,"evidence_quote":"The x86-Sok dataset whose labels Tady's detector shows to contain widespread violations, motivating the dataset-error contribution."},{"cited_title":"On the generation of disassembly ground truth and the evalua- tion of disassemblers","cited_arxiv_id":null,"evidence_quote":"The Pangine dataset, with labels derived from compilation intermediates, used to train the model."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The binary-level anti-disassembly obfuscation benchmark used to show that all disassemblers, including rule-based ones, violate constraints under obfuscation."}],"review_version":1}