System controllers in critical infrastructures

Control systems are at the heart of many critical infrastructures. Malicious attacks on system controllers like SCADA (Supervisory Control And Data Acquisition) systems are serious threats to critical national infrastructures such as smart grids, nuclear power plants, or transportation systems. Analyzing and verifying the security of the control systems has increasingly become an important defense mechanism. This paper presents an approach that facilitates a semi-automated security system verification of control systems by a novel application of model checking, a technique traditionally used for automated software verification. The proposed approach is different from typical model-checking applications in that it has the ability to uncover missing safety and security properties that should be specified to prevent catastrophes caused by malicious acts. We describe the approach by illustrating its use in analyzing a cooling reactor system controller in a nuclear power plant system. The approach is general and applicable to SCADA and other control systems.