{"id":"7388a658-57ff-49f0-b857-7a4080b800ab","arxiv_id":"2607.08417","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"low","formal_verification":"none","parameter_count":2,"one_line_summary":"ESBMC-LLB exposes function-block-hidden ladder logic bombs as safety violations, proves bomb-absence unboundedly, and synthesizes detonation triggers on public PLC benchmarks.","lead":"This paper turns a PLC safety verifier into a detector for dormant malicious ladder logic, recovering the exact trigger that would fire a bomb. It matters because industrial controllers run critical infrastructure and existing scanners miss bombs hidden inside function blocks.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified beyond the paper's own scope limits.","rationale":"The paper's central reduction—FB-body translation makes resident bombs reachable, scan-watchdog and output wiring turn the two dominant payload families into checkable safety violations, BMC synthesizes the trigger, k-induction certifies absence—is internally consistent and multi-corpus supported. The reader already identified the load-bearing scope assumption (modeled classes + supplied properties) and the residual caveats (proxy adaptive comparison, k-induction incompleteness, analog over-approx FP, nonlinear SMT timeout). Those are correctly treated as reasons for CONDITIONAL, not REJECT. No additional load-bearing attack lands: the evaluation includes third-party data, a real SWaT head-to-head with an honest negative result, and explicit complementarity rather than over-claim. Therefore the reader's verdict and confidence need no adjustment.","tokens_in":16122,"tokens_out":526,"duration_ms":5492,"concrete_test":"Reproduce RQ2 and RQ4 from the artifact: run the sound Boolean/integer configuration on all 60 Iacobelli programs and the five adaptive EQ_0 variants; confirm 30/30 malicious VIOLATION with recovered triggers, 29/30 benign SAFE (1 UNKNOWN), 0 FP, and 5/5 adaptive detections. If any of those fail, the strongest claim weakens; if they hold, the CONDITIONAL verdict stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest assumption correctly names the paper's explicit completeness boundary (§4.1, §7): detection is sound only for non-termination and property-violating forgery payloads, and only modulo defender-supplied properties and a trusted toolchain (§3). That is a real scope limit, not a hidden flaw in the argument. The strongest claim is carefully scoped to the modeled classes and the reported corpora (Iacobelli 30/30, SWaT v1.0.0 149/150, adaptive variants 5/5, Boolean/integer 155/155). The paper already reports the nonlinear SWaT drop to 49%, the single UNKNOWN under k-induction, the measured false positive under the analog over-approximation, and that the adaptive comparison uses a CFG-triage proxy rather than released PLC-Defuser. Those residual issues justify CONDITIONAL rather than unconditional ACCEPT, but they do not undermine the central Boolean/integer and linear-analog claims or the complementary positioning versus CFG triage. No stronger internal inconsistency or unsupported leap is present.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper presents ESBMC-LLB, a modeling layer atop the existing ESBMC-PLC+ verifier that recasts Ladder Logic Bomb (LLB) detection as formal property checking. The central observation is that real LLBs hide inside function-block bodies that prior LD frontends drop from the IR; a ~240-line FB-body translation, a scan-watchdog for non-termination payloads, and FB-output wiring for forgery payloads make those bombs checkable. k-induction yields unbounded bomb-absence proofs; incremental BMC recovers the detonation trigger. Evaluation covers the public Iacobelli et al. dataset (30/30 malicious, 0 FP among conclusive benign cases), five adaptive-trigger variants that evade a CFG-triage proxy (5/5), a 310-program Boolean/integer taxonomy corpus (100% recall, 0 FP, median 70 ms), and the first semantic model-checker run on PLC-Defuser’s SWaT corpus (149/150 on archived v1.0.0 linear bombs; 73/150 on a later nonlinear-arithmetic snapshot). The authors position semantic model checking and CFG triage as complementary rather than competing.","tokens_in":16421,"tokens_out":952,"duration_ms":13684,"significance":"If the reported results hold, the work is a clear advance for offline PLC security verification. It supplies two guarantees that signature, anomaly, and CFG-triage detectors lack—unbounded bomb-absence certificates and automatic trigger synthesis—while remaining honest about where SMT-based checking loses (nonlinear analog non-termination). Strengths include: use of public third-party corpora (Iacobelli, PLC-Defuser SWaT) rather than only self-authored data; explicit reporting of the unfavorable nonlinear tier (49%) alongside the favorable linear tier (99%); a reproducible artifact with pinned corpus versions and a sound-mode flag; and a carefully scoped complementary framing versus CFG triage. These make the paper useful both as a detector and as a map of the semantic-vs-structural trade-off for the community.","major_comments":[{"comment":"§6.6 / Table 5: The adaptive-adversary claim is load-bearing for Contribution 3 and the “CFG-triage is structurally incomplete” positioning, yet the comparison is against a transparent CFG-triage proxy, not the released PLC-Defuser tool. The paper states this limitation, but the abstract and §1 still read as if the result is a head-to-head against CFG-triage detectors. Either (a) run the released PLC-Defuser tool on the five variants and report the outcome, or (b) rephrase abstract/intro claims to “evades a CFG-triage proxy modeling syntactic triage” so the contribution is not overstated relative to the evidence.","section":null},{"comment":"§3, §4.1, §7: Detection completeness is explicitly modulo defender-supplied safety/integrity properties and the two modeled payload classes (non-termination, property-violating forgery). For a security detector this is a real operational boundary: an attacker who forges values that never violate the stated property set, or who uses a payload outside those two classes, is out of scope. The paper acknowledges this, but the threat-model and conclusion sections should state more sharply what the defender must supply (and what happens if the property set is incomplete) so that the “unbounded bomb-absence” guarantee is not read as absolute absence of all malicious logic.","section":null},{"comment":"§6.8 / Table 6 and §7: The analog-extended configuration is reported to introduce one false positive on the Iacobelli benign set when applied outside RQ6, and the sound Boolean/integer configuration covers only 75/150 of the SWaT v1.0.0 bombs. The paper correctly separates the two configurations, but the abstract’s “149/150 … with zero false positives” line does not flag that this figure is from the over-approximating analog mode. A one-sentence qualification in the abstract (and a clearer callout in Table 6) would prevent readers from attributing full soundness to the 99% figure.","section":null}],"minor_comments":[],"recommendation":"minor_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The useful part of this paper is not a new solver. It is the observation that real ladder bombs hide inside function-block bodies that prior LD frontends drop, plus a small modeling layer (FB-body translation, scan-watchdog, output wiring) that makes those bombs reachable as ordinary safety violations. Once that is in place, k-induction gives unbounded bomb-absence proofs and BMC returns the concrete trigger. That combination is what signature, anomaly, and CFG-triage tools do not give you.\n\nThey earn the claim. On the public Iacobelli set they get 30/30 detection and full trigger recovery, with zero false positives among the conclusive benign cases. The 310-program Boolean/integer taxonomy is clean (100% recall, 0 FP, median 70 ms). The adaptive variants (computed, opaque arithmetic, multi-scan) beat a CFG-triage proxy for the right reason: they check semantics, not patterns. The SWaT evaluation is the first semantic model-checker run on that corpus; they make it parseable, hit 149/150 on the linear v1.0.0 release with zero FPs, and then report the drop to 49% on the nonlinear non-termination bombs instead of burying it. That honesty is rare and useful.\n\nSoft spots are real but already scoped by the authors. Completeness is only for non-termination and property-violating forgery, and only modulo the defender’s property set and a trusted toolchain. The adaptive comparison is against a proxy, not the released PLC-Defuser tool. k-induction leaves one benign program UNKNOWN. The analog over-approximation introduces a measured false positive on Iacobelli, which is why they correctly keep the sound Boolean/integer configuration separate. None of these break the central Boolean/integer and linear-analog results or the complementary positioning versus CFG triage.\n\nThis is for people who care about offline ICS verification and PLC tooling. The math is standard BMC/k-induction; the data and citation pattern look solid; the artifact story is concrete. I would send it to referees. Engage with it if you work in this area.","headline":"Solid, honest PLC-security paper: FB-body modeling turns an existing verifier into a real LLB detector with trigger synthesis and unbounded absence proofs, and they report the nonlinear failure instead of hiding it.","tokens_in":17006,"tokens_out":528,"would_cite":true,"duration_ms":6372,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Formal model checking of PLC ladder programs can expose hidden logic bombs and recover their detonation triggers, with unbounded proofs that pattern scanners lack.","keywords":["Ladder Logic Bombs","PLC","IEC 61131-3","formal verification","bounded model checking","k-induction","trigger synthesis","industrial control systems"],"falsifier":"A planted ladder bomb whose payload always terminates and never violates any of the supplied safety or integrity properties, yet still produces a harmful physical effect that an operator would care about, would show the method is incomplete for real plant risk.","tokens_in":17016,"feed_emoji":"⚙️","tokens_out":644,"duration_ms":8784,"temperature":0.7,"pith_summary":"Ladder Logic Bombs are ordinary-looking PLC control code that stay dormant until a trigger fires a payload that forges sensors, moves actuators, or hangs the controller. The paper shows that real bombs hide inside function-block bodies that ordinary ladder verifiers simply drop from their intermediate form, so the malicious and benign programs look identical to a prover. ESBMC-LLB restores those bodies, then turns bomb detection into ordinary safety checking: a scan-watchdog makes non-terminating denial-of-control payloads into assertion failures, and output wiring makes actuator-forgery payloads violate mutual-exclusion or integrity properties. Bounded model checking returns the concrete input sequence that is the trigger; k-induction can certify that no bomb of the modeled class exists across all scan cycles. On a public 60-program dataset the method finds every bomb and recovers every trigger; it also catches adaptive triggers that hide from control-flow triage, and on a real analog plant corpus it reaches 99 percent detection for linear cases while openly failing on nonlinear loops that time out the SMT solver.","feed_headline":"Model checking finds hidden PLC bombs and their triggers","feed_subtitle":"Function-block translation plus safety properties catch dormant logic that pattern scanners miss","key_machinery":"ESBMC-LLB modeling layer: function-block-body translation that re-injects the dropped logic into the prover, plus a scan-watchdog assertion and function-block output wiring that convert the two dominant payload families into reachable safety violations whose counterexamples are the triggers.","core_discovery":"Real ladder-logic bombs hide inside function-block bodies that prior ladder verifiers drop from the IR; once those bodies are restored and two lightweight mechanisms (scan-watchdog for non-termination, output wiring for forgery) are added, bomb detection reduces to ordinary safety verification. Bounded model checking synthesizes the detonation trigger as a counterexample, and k-induction supplies an unbounded certificate of bomb absence for the modeled classes.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Model checking finds hidden PLC ladder bombs via function blocks","Formal verification recovers PLC bomb triggers as counterexamples","ESBMC exposes dormant ladder bombs that CFG scanners miss","k-induction proves bomb absence; BMC synthesizes the trigger","Restored function blocks turn PLC bomb hunt into safety checks"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The method only catches bombs whose payloads either fail to terminate or violate a safety property the defender actually wrote down; a bomb that always finishes and never breaks a stated property stays invisible.","fun_headline_variants_meta":{"raw":{"variants":["Model checking finds hidden PLC ladder bombs via function blocks","Formal verification recovers PLC bomb triggers as counterexamples","ESBMC exposes dormant ladder bombs that CFG scanners miss","k-induction proves bomb absence; BMC synthesizes the trigger","Restored function blocks turn PLC bomb hunt into safety checks"]},"model":"grok-4.5","effort":"low","cost_usd":0.005002,"raw_usage":{"total_tokens":1505,"prompt_tokens":911,"num_sources_used":0,"completion_tokens":61,"cost_in_usd_ticks":50020000,"prompt_tokens_details":{"text_tokens":911,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":533,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":911,"tokens_out":61,"duration_ms":5221,"temperature":1.0,"reasoning_tokens":533,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-10T07:46:17.521795+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"A planted ladder bomb whose payload always terminates and never violates any of the supplied safety or integrity properties, yet still produces a harmful physical effect that an operator would care about, would show the method is incomplete for real plant risk.","supporting_citations":[],"review_version":1}