Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis

• URL: http://arxiv.org/abs/2607.08417v1
• Date: Thu, 09 Jul 2026 12:42:20 GMT
• Title: Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
• Abstract summary: A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators, forge sensor readings, or deny operator control.<n>We present ESBMC-LLB, which uses ESBMC-PLC+ as its verification engine and adds a modeling layer that exposes function-block logic and recasts bomb detection as a formal verification problem.<n>On the public Iacobelli 2024 dataset, ESBMC-LLB detects all 30 bombs and recovers every trigger; it also detects adaptive triggers that evade CFG-triage.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators, forge sensor readings, or deny operator control. We observe that real malicious logic hides inside function-block bodies, which existing ladder-diagram verifiers drop from their intermediate representation (IR), making bombs invisible to provers. We present ESBMC-LLB, which uses ESBMC-PLC+ as its verification engine and adds a modeling layer that exposes function-block logic and recasts bomb detection as a formal verification problem: a scan-watchdog exposes non-termination payloads, and output wiring exposes actuator-forgery payloads as safety violations. k-induction gives an unbounded proof of bomb-absence across all scans, and the bounded model checker returns a counterexample that is the trigger - guarantees that signature, anomaly, and CFG-triage detectors lack. On the public Iacobelli 2024 dataset, ESBMC-LLB detects all 30 bombs and recovers every trigger; it also detects adaptive triggers (computed, opaque-arithmetic, multi-scan) that evade CFG-triage. We also report the first semantic model-checker evaluation on PLC-Defuser's SWaT corpus: our analog extension makes the full corpus parseable; on v1.0.0, it detects 149/150 bombs (99%) with zero false positives, recovering each trigger; on a later version with nonlinear non-termination bombs, detection drops to 49% as the SMT solver times out. We conclude that semantic model checking and CFG-triage are complementary - the former gives unbounded proofs, adaptive-trigger robustness, and handles Boolean/integer and linear analog logic; the latter leads to nonlinear analog non-termination, and we delineate where each wins.

Related papers

• CyberLLM: A Multi-Agent LLM Framework for Autonomous Detection and Guarded Response in Automotive Cybersecurity [22.68559728326395]
  CyberLLM is a framework that autonomously detects vulnerabilities and executes remediations under a formal, runtime safety guard.<n>Decision agents aggregates findings, tags them with a human-centric asset taxonomy, and selects a tiered response.<n>A symmetric attack pipeline generates and replays exploits so both sides can be exercised on the same scenarios.
  arXiv  Detail & Related papers  (2026-08-06T23:39:13Z)
• Cybersecurity Detection Classification with Reasoning-enabled Language Models [50.72675435043546]
  A major issue in Security Operations Centers (SOCs) is alert fatigue.<n>Prior work prompts or fine-tunes large language models (LLMs) to emit a triage label directly, but does not train them to reason about whether a detection is a genuine threat.<n>We train a chain-of-thought (CoT) reasoning-enabled triage classifier on real, human-labeled Windows endpoint detections.
  arXiv  Detail & Related papers  (2026-07-30T16:22:13Z)
• From Detection to Action: Using LLM Agents for Fault-Tolerant Control [0.21313236831585222]
  We propose an agentic Large Language Model (LLM) framework for Fault-Tolerant Control (FTC)<n>It transforms fault detection outputs into constraint-aware recovery actions grounded in plant-specific knowledge.<n>We show that semantically grounded agents can derive valid recovery decisions within latency budgets compatible with the respective process dynamics.
  arXiv  Detail & Related papers  (2026-06-26T12:13:58Z)
• CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
  We introduce textbfCIAware-Bench, a benchmark for measuring textbfcontrol textbfintervention (CI) awareness across frontier models.<n>CIAware-Bench tests whether models can distinguish their own trajectories from those modified by a control intervention.
  arXiv  Detail & Related papers  (2026-06-09T16:24:16Z)
• From Attack Simulation to SIEM Rule: Deterministic Detection-as-Code Synthesis with Probe-Level Traceability [51.56484100374058]
  Security teams simulate attacks against their own systems to check whether their monitoring would catch a real intruder.<n>A human bridges that gap by hand, reading each finding and writing the corresponding Sigma rule.<n>We show this translation can be partially automated when probes are drawn from a locked corpus.
  arXiv  Detail & Related papers  (2026-06-03T14:26:25Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• Explainability-Guided Adversarial Attacks on Transformer-Based Malware Detectors Using Control Flow Graphs [0.19116784879310025]
  This paper examines the vulnerability of a RoBERTa-based malware detector that linearizes control flow graphs into sequences of function calls.<n>By evaluating evasion strategies within this graph-to-sequence framework, we provide insight into the practical robustness of transformer-based malware detectors beyond aggregate detection accuracy.
  arXiv  Detail & Related papers  (2026-04-04T19:50:04Z)
• From Passive Monitoring to Active Defence: Resilient Control of Manipulators Under Cyberattacks [42.72791770760975]
  False data injection attacks (FDIAs) can induce substantial end-effector deviations without triggering alarms.<n>This paper studies the resilience of redundant manipulators to stealthy FDIAs and advances the architecture from passive monitoring to active defence.
  arXiv  Detail & Related papers  (2026-03-13T14:08:41Z)
• Beyond Reward Suppression: Reshaping Steganographic Communication Protocols in MARL via Dynamic Representational Circuit Breaking [0.0]
  steganographic collusion, where agents develop private protocols to evade monitoring, presents a critical AI safety threat.<n>Existing defenses, limited to behavioral or reward layers, fail to detect coordination in latent communication channels.<n>We introduce the Dynamic Representational Circuit Breaker (DRCB), an architectural defense operating at the optimization substrate.
  arXiv  Detail & Related papers  (2026-03-07T04:14:38Z)
• A multi-layered embedded intrusion detection framework for programmable logic controllers [0.0]
  This research presents an embedded intrusion detection system that runs inside the controller and uses header-level telemetry to detect and respond to network attacks.<n>The proposed architecture provides a multi-layer embedded security that meets the real-time requirements of an industrial system.
  arXiv  Detail & Related papers  (2025-10-08T16:12:02Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.