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

Jul 16, 2026

A Ladder Logic Bomb (LLB) is malicious control logic inserted into a Programmable Logic Controller (PLC) program that remains dormant until a trigger fires a payload manipulating actuators, forging sensor readings, or denying operator control. The work observes that real LLBs often hide inside function-block bodies, making them indistinguishable for existing Ladder Diagram verifiers. ESBMC-LLB repurposes ESBMCPLC+ by adding a modeling layer that exposes function-block-resident logic to the prover, enabling k-induction unbounded bomb-absence proofs and BMC counterexamples as automatic trigger synthesis. Evaluations show full detection on a public dataset and strong semantic model checking on SWaT, with complementary trade-offs versus CFG-triage detectors.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages14

Reading Time35 min

AccessFree to download

Introduction

ESBMC-LLB: Formal verification view of LLB detection

Payload-to-property reduction and guarantees

Trigger synthesis via bounded counterexamples

DETECTING LADDER LOGIC BOMBS IN IEC 61131-3 PLC PROGRAMS USING ESBMC-PLC+: A FORMAL VERIFICATION APPROACH WITH TRIGGER SYNTHESIS PREPRINT Pierre Dantas* Department of Computer Science The University of Manchester Manchester, UK [pierre.dantas@manchester.ac.uk](pierre.dantas@manchester.ac.uk)[ ](pierre.dantas@manchester.ac.uk)[ORCID: 0000-0001-6390-9340](ORCID: 0000-0001-6390-9340) Lucas Cordeiro* Department of Computer Science The University of Manchester Manchester, UK [lucas.cordeiro@manchester.ac.uk](lucas.cordeiro@manchester.ac.uk)[ ](lucas.cordeiro@manchester.ac.uk)[ORCID: 0000-0002-6235-4272](ORCID: 0000-0002-6235-4272) arXiv :2607 .084 17v 1 [ cs .CL] 9 Jul 2026 Waldir Junior* Electrical Engineering Federal University of Amazonas (UFAM) Manaus, AM, Brazil [waldirjr@ufam.edu.br](waldirjr@ufam.edu.br) ORCID: 0000-0003-3095-0042 July 2026 ABSTRACT A Ladder Logic Bombs (LLB) is malicious control logic inserted into a Programmable Logic Controller (PLC) program that lies dormant until a trigger fires a payload which manipulates actuators, forges sensor readings, or denies operator control. We make a structural observation about real LLB datasets: the malicious logic hides inside function-block bodies, which existing Ladder Diagram (LD) verifiers drop from their Intermediate Representation (IR), rendering the malicious and benign programs indistinguishable to the prover. We present ESBMC-LLB, a method that uses ESBMCPLC+ (an existing IEC 61131-3 verifier) as its verification engine, adding a modeling layer that exposes the function-block-resident logic to the prover and recasts LLB detection as formal verification: a scan-watchdog exposes denial-of-control (non-termination) payloads and output wiring exposes actuator-forgery payloads as checkable safety violations. k-induction yields an unbounded proof of bomb-absence across all scan cycles, and the bounded model checker returns a counterexample that is the detonation trigger – two guarantees that signature-, anomaly-, and Control Flow Graph (CFG)-triage detectors do not provide. On the public Iacobelli et al. [12] dataset, ESBMCLLB detects all 30 bombs and recovers every trigger; because it reasons over program semantics rather than syntactic patterns, it also detects adaptive triggers (computed, opaque-arithmetic, multiscan) that evade a CFG-triage heuristic. We further report the first evaluation of a semantic model checker on the state-of-the-art’s real analog benchmark (PLC-Defuser’s SWaT corpus): our analog modeling extension makes the full corpus parseable for the first time and, on the archived v1.0.0 release, detects 149/150 bombs (99%) with zero false positives, recovering each trigger; on a later corpus version that adds nonlinear non-termination bombs, detection drops to 49% as the Satisfiability Modulo Theories (SMT) backend times out. We conclude that semantic model checking and CFG-triage are complementary – the former adds unbounded bomb-absence proofs and adaptivetrigger robustness and handles Boolean/integer and linear analog logic, the latter leads on nonlinear analog non-termination – and we delineate exactly where each wins. ∗ The authors contributed equally to this research. Corresponding author: [pierre.dantas@manchester.ac.uk](pierre.dantas@manchester.ac.uk). Keywords Ladder Logic Bombs · PLC · IEC 61131-3 · Industrial Control Systems security · ESBMC · BMC · k-induction · SMT · trigger synthesis · formal verification · LD · PLCopen XML 1 Introduction Programmable Logic Controllers (PLCs) run the control logic of safety-critical Industrial Control Systems (ICS): water treatment, power, chemical, and manufacturing plants. An attacker who gains write access to a PLC – through the engineering workstation, a compromised project file, or the supply chain – can insert a Ladder Logic Bombs (LLB): a fragment of control logic that remains dormant until a trigger fires, then executes a payload that sabotagesthe physica

FAQs

What problem does this paper address in IEC 61131-3 PLC programs?

It targets Ladder Logic Bombs (LLBs), malicious control logic that stays dormant until a trigger fires and then sabotages the physical process by manipulating actuators, sensor readings, or operator control.

Why can existing Ladder Diagram verifiers miss real LLBs?

Because LLBs can hide inside function-block bodies, and existing verifiers drop that content from their intermediate representation, making malicious and benign programs indistinguishable to the prover.

How does ESBMC-LLB detect bombs and recover the trigger?

It models function-block-resident logic so verification can check safety/integrity properties. k-induction provides an unbounded bomb-absence proof, while bounded model checking returns a counterexample trace whose triggering input/cycle sequence is treated as the detonation trigger.

Jul 16, 2026

Upload by Theodore