DETECTING LADDER LOGIC BOMBS IN IEC 61131-3 PLC PROGRAMS USING ESBMC-PLC+: A FORMAL VERIFICATION APPROACH WITH TRIGGER SYNTHESIS

Programmable Logic Controllers (PLCs) are critical for industrial infrastructure, yet they are vulnerable to Ladder Logic Bombs (LLBs)—malicious code fragments that remain dormant during standard testing and detonate only under specific conditions. Existing verification tools often fail to detect these because they ignore logic hidden inside function-block bodies. The authors introduce ESBMC-LLB, which extends the ESBMC-PLC+ verification engine to include function-block-resident logic. By recasting bomb detection as a formal verification problem, the tool uses k-induction to provide unbounded proofs of bomb-absence and bounded model checking (BMC) to synthesize the exact trigger sequence that detonates a bomb.

The approach relies on two primary mechanisms to expose malicious behavior. First, a scan-watchdog monitors for non-terminating loops, treating them as safety violations. Second, output wiring propagates forged function-block outputs into the main program, where they trigger safety property violations (such as mutual exclusion errors). Because the tool reasons over program semantics rather than syntactic patterns, it can identify complex, adaptive triggers—such as those involving opaque arithmetic or multi-scan dependencies—that evade traditional Control Flow Graph (CFG) triage methods.

ESBMC-LLB demonstrates high efficacy across diverse datasets. It successfully detected all 30 bombs in the third-party Iacobelli et al. dataset and achieved 99% detection accuracy on the PLC-Defuser SWaT corpus (v1.0.0) with zero false positives. The tool is particularly robust against adaptive adversaries, successfully identifying triggers that syntactic detectors miss. However, the authors note a clear performance boundary: while the tool excels at Boolean, integer, and linear analog logic, its detection rate falls to 49% on newer versions of the SWaT corpus containing nonlinear non-termination bombs, as the underlying SMT solver struggles with the increased complexity.