PLC-Defuser: Detecting hidden Ladder Logic Bombs in PLCs via Control Flow Graph and model checking

Industrial Control Systems (ICS) are responsible for the operations of critical industrial infrastructures such as water treatment facilities and nuclear plants. To control sensors and actuators, ICSs rely on Programmable Logic Controllers (PLCs), which have become the target of an increasing number of cyberattacks, particularly since the appearance of Stuxnet. In response, numerous anomaly detection methods have been proposed in the literature to identify stealthy attacks targeting ICS sensors and actuators. However, no existing method specifically addresses the detection of Ladder Logic Bombs (LLBs), a class of attacks designed to disrupt the normal operation of PLCs. In this work, we introduce PLC-Defuser, an automated framework specifically tailored to the task of LLB detection. PLC-Defuser first employs static analysis through Control Flow Graphs (CFG) to identify possible LLB triggers within the PLC control logic. It then performs model checking to formally verify whether the identified suspicious triggers activate malicious LLBs. We evaluate PLC-Defuser considering a simplified version of the Secure Water Treatment System (SWaT), for which we built a dataset of PLC programs containing 150 malicious and 150 legitimate samples. Our results demonstrate that PLC-Defuser effectively protects industrial plants without producing false positives and achieves an average execution time of less than 0.5 s.