{"id":"1d1b451a-7839-40ea-ae60-c5c62570c090","arxiv_id":"2608.10265","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":3.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Adding six rule-based filters to Mythril cut false positives by 50.0% on clean contracts and 89.2% on vulnerable contracts in the Gigahorse benchmark, while keeping true positives roughly unchanged.","lead":"This paper applies six hand-written rules to Mythril, an Ethereum smart contract analyzer, to remove false bug reports. If the improvement is real, smart contract auditors would spend less time chasing false alarms and more on real vulnerabilities.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"False-positive reduction is measured against incomplete benchmark labels; unlabeled real vulnerabilities may be counted as false positives and silently suppressed.","rationale":"The reader's weakest assumption identifies the same load-bearing concern: the evaluation treats Gigahorse labels as complete ground truth. The central claim requires that the suppression of 116 reports on the vulnerable set (130→14) removes only false alarms and not real vulnerabilities. Table I provides no true-positive evidence for five of the six targeted classes, so the benchmark labels cannot validate that those suppressions were actually false positives. The paper's own limitation statement about the integer-arithmetic class further weakens the claim, since that class is the only source of labeled true positives and its FP count increased on both datasets under the proposed rule. This does not disprove the result, but it makes the headline reduction conditional on an independent audit or a held-out benchmark with complete labels. No verdict change is needed because the reader already issued CONDITIONAL for essentially this reason.","tokens_in":13778,"tokens_out":7895,"duration_ms":79004,"concrete_test":"Independently audit a random sample of 50 of the 130 baseline \"false positive\" reports on the GH Vulnerable set, prioritizing the five non-integer classes, by having two annotators inspect the contract source and classify each report as a real vulnerability or a false alarm without access to Gigahorse labels. If any sampled report is confirmed as a genuine vulnerability, the reported FP reduction overstates the improvement and the central claim fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim depends on treating Gigahorse labels as complete and authoritative, but Section IV states: \"Any vulnerability flagged by Mythril but absent in the ground truth reference was considered a false positive.\" This conflates \"not labeled\" with \"not a vulnerability.\" Table I shows that all true positives and false negatives are concentrated in Integer Arithmetic (TP 12→13, FN 4→3); the other five vulnerability classes have zero true positives on the entire vulnerable set. The headline vulnerable-set FP reduction from 130 to 14 is therefore achieved almost entirely by suppressing 116 reports in classes where the benchmark provides no evidence that any report is real. If those suppressed reports include genuine reentrancy, predictable-environment, external-call, or multiple-call issues that simply lack a Gigahorse label, the improved tool has traded false positives for false negatives and the claim \"without compromising the detection of true vulnerabilities\" is untested. The paper's own outlier finding aggravates this: the only class with TP evidence, Integer Arithmetic, saw FPs increase on both datasets (34→50 invulnerable, 11→12 vulnerable), so the improvement rests on one net new TP while FP counts worsened in the one class with confirmed labels.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper addresses the false-positive problem in symbolic execution-based smart contract vulnerability detection by proposing six rule-based modifications to Mythril, one per vulnerability class. The rules are derived from an analysis of Mythril's baseline reports on the Gigahorse benchmark. The authors evaluate the enhanced Mythril on the same benchmark (40 invulnerable and 100 vulnerable contracts), reporting a reduction in false positives from 102 to 51 on the invulnerable set and from 130 to 14 on the vulnerable set, while true positives increase from 12 to 13, raising the F1-score from 0.152 to 0.605.","tokens_in":13948,"tokens_out":4729,"duration_ms":42586,"significance":"If the reported reductions were representative of out-of-sample behavior, the paper would provide a practical, lightweight recipe for improving the precision of symbolic execution tools. The strengths are the reproducible setup (pinned commit hashes for Mythril and the benchmark), the internally consistent counts in Table I, and the candid acknowledgment of the integer-arithmetic outlier. However, the evaluation design limits what can be concluded: the rules are developed and measured on the same dataset, and the ground-truth labels are treated as complete. The contribution is therefore an engineering demonstration on a single benchmark rather than a validated general method.","major_comments":[{"comment":"The rules are designed from the baseline false positives observed on the Gigahorse benchmark (Section IV) and then evaluated on the same Gigahorse benchmark (Section VI), making the reported FP reductions in-sample results rather than out-of-sample predictions. For example, the 'State access after an external call' rule in Section V.A is described as eliminating false positives by changing how reentrancy checks are invoked, which directly addresses the 15 invulnerable-set FPs counted in Table I. Because no held-out dataset or cross-validation is used, the headline numbers (102→51 and 130→14) may overstate the improvement on new contracts. The authors should evaluate the same rules on a separate benchmark (e.g., SmartBugs Wild or a manually audited contract set) to support the generalizability claim.","section":"Sections IV–VI"},{"comment":"The evaluation defines 'Any vulnerability flagged by Mythril but absent in the ground truth reference was considered a false positive,' which conflates 'not labeled' with 'not a vulnerability.' Since Table I shows zero true positives for five of the six targeted classes on the vulnerable set, the entire vulnerable-set FP reduction in those classes (e.g., 57→0 for State Access after an External Call and 18→0 for Dependence on Predictable Environment Variable) consists of reports whose status is unverified. If a suppressed report corresponds to an unlabeled real vulnerability, the tool has silently traded false positives for false negatives. The claim 'without compromising the detection of true vulnerabilities' is therefore untested for the classes that contribute most of the reported FP reduction. A manual audit of a sample of the suppressed reports, or a comparison against a more complete vulnerability database, is needed.","section":"Section IV"},{"comment":"The single class with confirmed true positives and false negatives is Integer Arithmetic (TP 12→13, FN 4→3), yet Table I shows that in this class the improved Mythril increases FPs on the invulnerable set from 34 to 50 and on the vulnerable set from 11 to 12. The paper acknowledges this as an 'outlier,' but because this class is the only one where the benchmark provides TP evidence, the overall improvement of F1 from 0.152 to 0.605 rests on suppressing reports in classes with no positive evidence while the confirmed class gets worse in FPs. This undermines the abstract's statement that the reduction is achieved 'without compromising the detection of true vulnerabilities' for the vulnerability type where detection is actually observable.","section":"Table I and Section VI.B"},{"comment":"The claim of a 'significant reduction' in false positives is not supported by any statistical test or uncertainty quantification. The counts are small (e.g., 12 vs. 13 true positives, 130 vs. 14 FPs), and the F1 increase from 0.152 to 0.605 is a point estimate. A simple McNemar test on the paired contract-level TP/FP outcomes across the 140 contracts, or bootstrap confidence intervals on the F1 difference, would establish whether the observed improvement is likely to be reproducible. Without this, 'significant' is an informal descriptor rather than a statistical claim.","section":"Section VI and Table III"}],"minor_comments":[{"comment":"The word 'benchamarks' is a typo and should be 'benchmarks.'","section":"Section III.C"},{"comment":"The total row reads 'Total Functions Flgged'; this should be corrected to 'Total Functions Flagged.'","section":"Table I"},{"comment":"The related work section is a series of per-paper summaries rather than a synthesis, and several references are inconsistently formatted (e.g., [4] and [13] have malformed author lists).","section":"Section II"},{"comment":"Algorithm 1 is incomplete and detached from the surrounding text: the numbered list describes steps that do not correspond one-to-one to the algorithm's pseudocode, making it hard to reproduce the rule from the text alone.","section":"Section V.A"},{"comment":"The paper has two future-work sections: Section VIII (Conclusion and Future Work) is followed by Section IX (Future Work). These should be merged into a single section.","section":"Sections VIII–IX"},{"comment":"The claim that Oyente and Manticore are 'conceptually suited' for porting the rules is speculative, since no implementation on those tools is provided; the portability claim is unsubstantiated beyond the stated prerequisites.","section":"Section VII.C"}],"recommendation":"major_revision","confidential_remarks":"The paper is a workmanlike engineering contribution with a clear scope, but the evaluation design is the main weakness: the rules are fitted to and measured on the same benchmark, and the ground-truth completeness assumption is strong given the zero-TP classes. The authors may be able to address this with a held-out evaluation and a manual audit of suppressed alerts. The manuscript also needs substantial editorial cleanup before it meets journal standards."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a plausible engineering contribution with an evaluation that doesn't support its strongest claim. The authors hand-patched Mythril to suppress false positives across six vulnerability classes and measured 50% and 89% FP reductions on the Gigahorse benchmark. The numbers are internally consistent, but the rules were designed from that same benchmark's false positives, and the benchmark labels are treated as if they were complete. That makes the headline result an in-sample improvement, not a general one.\n\nWhat's genuinely useful: the paper documents concrete rule ideas—path feasibility checks, taint tracking, call classification, state-effect checks—and gives enough detail (algorithms and partial code descriptions) that someone could port them to another tool. It also honestly reports the integer overflow outlier, where FPs got worse on both datasets while it was the only class with confirmed true positives.\n\nThe soft spots are the usual ones, but they bite hard here. First, no held-out evaluation. The rules are hand-crafted after inspecting the very false positives they're then measured against. Second, the FP definition is 'not in the ground truth reference,' which conflates 'not labeled' with 'not a vulnerability.' On the vulnerable set, five of the six classes have zero true positives, so 116 of the 130 baseline FPs are reports in classes where the benchmark provides no evidence that any report is real. Suppressing those alerts might be suppressing genuine findings. Third, the only class with confirmed TPs, integer arithmetic, saw FP counts increase from 34 to 50 (invulnerable) and 11 to 12 (vulnerable). The net TP gain is one, so the phrase 'without compromising detection of true vulnerabilities' is untested. Fourth, the novelty claim is overstated: Clairvoyance, RA, and GPTScan already prune alerts via path feasibility and state effects. Finally, no code or data release, so the numbers can't be independently checked.\n\nWho's this for? Practitioners who want to reduce alert noise in Mythril will find useful starting points. For the research claim, the paper needs a held-out benchmark, released code, and a deeper analysis of the integer overflow rule. I'd send it to peer review—a good referee could push it toward a usable evaluation—but it's not ready as-is.","headline":"The FP-reduction numbers are real but in-sample: the rules are fit to the same benchmark and 'ground truth' is treated as complete, so the 'without compromising true positives' claim is untested.","tokens_in":14511,"tokens_out":3718,"would_cite":false,"duration_ms":37923,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Adding vulnerability-specific rules to Mythril cuts false positives by up to 89 percent while preserving true detections.","keywords":["smart contract security","symbolic execution","false positive reduction","Mythril","rule-based analysis","Ethereum","Gigahorse benchmark","vulnerability detection"],"falsifier":"Have independent smart-contract auditors manually review a randomized sample of the alerts that the rules suppressed (the 51 invulnerable-set and 14 vulnerable-set remaining false positives, plus the alerts removed by each rule): if a substantial share are actually exploitable vulnerabilities omitted from the benchmark labels, the claim that true detection was not compromised fails; if the suppressed alerts are genuinely infeasible or guarded paths, the claim is supported.","tokens_in":13545,"feed_emoji":"🛡️","tokens_out":7560,"duration_ms":62930,"temperature":0.7,"pith_summary":"The paper argues that the large volume of false positives produced by symbolic execution tools for Ethereum smart contracts is a reliability problem that can be attacked directly with lightweight, vulnerability-specific rules. The authors patch six such rules into Mythril, a widely used symbolic execution analysis tool, and evaluate the patched version on the Gigahorse benchmark. False positives fall from 102 to 51 on the invulnerable set and from 130 to 14 on the vulnerable set, while true positives rise from 12 to 13 and the F1-score increases from 0.152 to 0.605. A sympathetic reader would take the paper to establish that targeted rule-based filtering can substantially improve precision of symbolic execution tools without sacrificing detection of actual vulnerabilities.","feed_headline":"Rule-based patches cut Mythril false positives by up to 89%","feed_subtitle":"Six targeted rules lift the F1 score from 0.152 to 0.605 on Gigahorse while keeping true detections.","key_machinery":"The mechanism is a set of six vulnerability-specific rules patched into Mythril's analysis code, mostly in its analyze_state functions and arithmetic helper. Each rule acts as an additional constraint or feasibility check that suppresses an alert unless a concrete exploitable path is shown to exist: state access after an external call is reported only when no reentrancy guard constrains the path; assertion violations are reported only when the previous opcode is REVERT and the assertion is always false; predictable-environment dependence is reported only when a tainted value actually influences world-state constraints and a satisfying transaction sequence exists; external calls to user-supplied addresses are reported only when an SSTORE follows the call and a valid transaction sequence is found; integer overflow or underflow is reported only when the Z3 solver confirms the wrap; and multiple calls in a single transaction are reported only when at least two external calls occur and the previous call succeeded. The rules therefore convert broad syntactic alarms into path-sensitive findings.","core_discovery":"The paper's central claim is that a rule-based filtering layer, implemented directly inside a symbolic execution engine, can remove a large share of false vulnerability alerts while keeping, and even slightly improving, the detection of real ones. On the Gigahorse ground truth, the patched Mythril reduces false positives by 50.0 percent on the invulnerable contracts and by 89.2 percent on the vulnerable contracts, increases true positives from 12 to 13, raises recall from 75.0 percent to 81.2 percent, and lifts the F1-score from 0.152 to 0.605. The authors attribute the gains to rules that check path feasibility, require state changes or successful previous calls before reporting reentrancy, skip constructor calls, inspect taint and predictable environment variables, and use the Z3 solver to confirm overflow or underflow conditions.","pith_inferences":["If the same rules were ported to other symbolic execution engines, the size of the gain would likely depend on how many of their baseline alerts already survive a basic feasibility check; tools with different over-approximation patterns may need additional rules tuned to their own false-positive modes.","The concentration of remaining false positives in integer arithmetic suggests that a semantic treatment of wraparound, tied to the actual path constraints rather than to a syntactic overflow pattern, may be a more direct route to closing the gap than further per-vulnerability rules.","Because the evaluation counts any Mythril finding absent from the benchmark labels as a false positive, the magnitude of the reported improvement would change if a different, independently audited label set were used; a testable extension is to rerun the patched tool on a second labeled corpus and compare the false-positive reduction.","For practitioners, the practical value may be larger than the F1 improvement suggests, since the cost of investigating a false alarm is not linear in the alert count: removing the most obviously infeasible paths first removes the cheapest categories of false alarms."],"forward_implications":["Mythril users would see a substantially smaller triage burden, since the number of alerts that must be manually inspected drops by half on clean contracts and by nearly ninety percent on vulnerable contracts.","Precision becomes a designable property of symbolic execution tools rather than an afterthought, because each fix is a small, localized enforcement of feasibility and state-effect checks.","The filtering layer is described as portable: any analyzer offering path feasibility queries, taint tracking, call-type classification, and state-effect detection could adopt the same rules, so the precision gains are not presented as exclusive to Mythril.","The remaining false positives concentrate almost entirely in integer arithmetic overflow and underflow, identifying that vulnerability class as the next target for more sophisticated rules.","Because recall also rose from 75.0 to 81.2 percent, the rules did not merely delete alarms; one true vulnerability missed by vanilla Mythril was recovered."],"supporting_citations":[{"why":"Mythril is the symbolic execution tool whose implementation receives the six rule patches.","marker":"[1]"},{"why":"Gigahorse Benchmarks supply the 100 vulnerable and 40 invulnerable labeled contracts used as ground truth.","marker":"[2]"},{"why":"Z3 is the SMT solver used to check satisfiability of overflow constraints and transaction sequences.","marker":"[28]"},{"why":"Prior bug-injection evaluation that demonstrated analysis tools such as Mythril report many false positives, motivating the problem.","marker":"[3]"},{"why":"Earlier reentrancy study reporting that most static-analysis findings on real contracts are false positives, providing context for the fix.","marker":"[18]"}],"fun_headline_variants":["Six rule filters cut Mythril false positives by up to 89%","Rule-based Mythril: 89% fewer false positives, F1 up to 0.605","Mythril's six new rules drop false alerts by 89% on vulnerable contracts","Symbolic-execution false alarms cut 89% with Mythril rule fixes","Six targeted rules raise Mythril F1 from 0.152 to 0.605"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The evaluation treats the Gigahorse benchmark labels as complete and authoritative ground truth, so every Mythril report that does not match a label is counted as a false positive; if those labels miss real vulnerabilities or classify severity differently, the headline reductions could reflect label coverage rather than genuine false alarms.","fun_headline_variants_meta":{"raw":{"variants":["Six rule filters cut Mythril false positives by up to 89%","Rule-based Mythril: 89% fewer false positives, F1 up to 0.605","Mythril's six new rules drop false alerts by 89% on vulnerable contracts","Symbolic-execution false alarms cut 89% with Mythril rule fixes","Six targeted rules raise Mythril F1 from 0.152 to 0.605"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001024,"raw_usage":{"total_tokens":4335,"prompt_tokens":977,"completion_tokens":3358,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":593,"completion_tokens_details":{"reasoning_tokens":3248}},"tokens_in":593,"tokens_out":3358,"duration_ms":21973,"temperature":1.0,"reasoning_tokens":3248,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:10:04.634800+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Have independent smart-contract auditors manually review a randomized sample of the alerts that the rules suppressed (the 51 invulnerable-set and 14 vulnerable-set remaining false positives, plus the alerts removed by each rule): if a substantial share are actually exploitable vulnerabilities omitted from the benchmark labels, the claim that true detection was not compromised fails; if the suppressed alerts are genuinely infeasible or guarded paths, the claim is supported.","supporting_citations":[{"cited_title":"Mythril,","cited_arxiv_id":null,"evidence_quote":"Mythril is the symbolic execution tool whose implementation receives the six rule patches."},{"cited_title":"Gigahorse-benchmarks,","cited_arxiv_id":null,"evidence_quote":"Gigahorse Benchmarks supply the 100 vulnerable and 40 invulnerable labeled contracts used as ground truth."},{"cited_title":"Z3: An efficient smt solver,","cited_arxiv_id":null,"evidence_quote":"Z3 is the SMT solver used to check satisfiability of overflow constraints and transaction sequences."},{"cited_title":"How Effective are Smart Contract Analysis Tools? Evaluating Smart Contract Static Analysis Tools Using Bug Injection","cited_arxiv_id":"2005.11613","evidence_quote":"Prior bug-injection evaluation that demonstrated analysis tools such as Mythril report many false positives, motivating the problem."},{"cited_title":"Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart con- tracts,","cited_arxiv_id":null,"evidence_quote":"Earlier reentrancy study reporting that most static-analysis findings on real contracts are false positives, providing context for the fix."}],"review_version":1}