Waldir Junior

Pierre Dantas, Lucas Cordeiro, Waldir Junior

OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) security research. Existing open-source verifiers for IEC 61131-3, including ESBMC-PLC, prove safety over an abstract scan-cycle model with idealized unbounded integers. The board artifact runs on a resource-constrained microcontroller unit (MCU) with 16-bit words (8-bit AVR Arduinos), and sensors are read via a finite-resolution analog-to-digital converter (ADC). We show this deployment gap makes naive width-aware verification unsound: across 123 real programs, checking 16-bit overflow without a hardware input model yields 44% false alarms (54/123) and finds no genuine defects, because it explores sensor values no ADC can produce. Since the gap lies where computation meets the physical process - a bounded sensor reading scaled by finite-width arithmetic into an actuation command - an overflow can silently suppress a safety action, such as a high-level alarm. An unbounded input model fabricates alarms that no environment can trigger. We present hardware-faithful verification for IEC 61131-3 on open hardware: a declarative hardware abstraction layer (HAL) descriptor (width, ADC/PWM resolution, I/O binding) and a sound lowering that interprets arithmetic at target width and constrains inputs to hardware-realizable ranges. We instantiate it for Arduino as ArduinoTool, deriving HAL parameters from official cores and realizing the input-range model in the ESBMC Ladder Diagram (LD) frontend. On the 123-program corpus, the HAL annotator eliminates all 54 false alarms while preserving robustness proofs, and a controlled corpus demonstrates the rare width-dependent defects it detects with realizable witnesses.

Pierre Dantas, Lucas Cordeiro, Waldir Junior

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.