Model Checking of Security Properties in Industrial Control Systems (ICS)

With the increasing inter-connection of operation technology to the IT network, the security threat to the Industrial Control System (ICS) is increasing daily. Therefore, it is critical to utilize formal verification technique such as model checking to mathematically prove the correctness of security and safety requirements in the controller logic before it is deployed on the field. However, model checking requires considerable effort for regular ICS users and control technician to verify properties. This paper, provides a simpler approach to the model checking of temperature process control system by first starting with the control module design without formal verification. Second, identifying possible vulnerabilities in such design. Third, verifying the safety and security properties with a formal method.