Search papers, labs, and topics across Lattice.
This paper introduces ESBMC-LLB, a formal verification tool designed to detect Ladder Logic Bombs (LLBs) in PLC programs by addressing the limitations of existing verifiers that overlook function-block logic. By employing a modeling layer that exposes hidden malicious logic and utilizing k-induction for unbounded proof of bomb absence, the method successfully identifies all 30 bombs in the Iacobelli 2024 dataset while recovering every trigger. The results demonstrate the tool's effectiveness, achieving 99% detection accuracy on the SWaT corpus with zero false positives, although performance decreases with more complex nonlinear bombs.
Uncovering hidden malicious logic in PLC programs, ESBMC-LLB achieves 99% detection accuracy of Ladder Logic Bombs without any false positives.
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.
