Detection of Ladder Logic Bombs in PLC Control Programs: an Architecture based on Formal Verification

Industrial Control Systems (ICS) are responsible for the operations of production plants and critical infrastructures such as nuclear plants and smart grids. Since failures in such systems may harm people, damage properties, and affect the environment, security (in addition to safety) concerns are of paramount importance. In this work, we present a formal verification architecture for the detection of Ladder Logic Bombs, a class of attacks aimed at disrupting the normal operation of Programmable Logic controllers (PLCs). We built a dataset of PLC programs modeling the control logic of a physical system, containing thirty malicious and thirty legitimate samples, then we tested the proposed framework showing that it is able to detect LLBs with very high values of accuracy and precision.