Cyber-Physical Systems Security Verification Utilising SAT-based Model Checking

CPS integration into critical infrastructures makes it necessary to guarantee security, thereby making security in CPS paramount. This project incorporates the application of model checking, more specifically SAT-based model checking as a form of formal verification to increase CPS security. After mapping CPS security properties into a Boolean satisfiability problem, SAT solvers can conveniently search for malicious behaviour through the state space. This approach enables the rigorous checking of complex systems to ensure that no single component or sub system has inherent security flaws or has not met given security requirements. Model checking by means of SAT-based identification supports accurate analysis of counterexamples for any violations, thus enabling efficient diagnosis of security breaches. This methodology provides a strategic and feasible approach to perform a confirmation of the authentication, access control, data integrity, confidentiality and intrusion in CPS. Analysing the proposed approach, it is noted that there are substantial enhancements in the detection accuracy as well as the verification within the system, leading towards the qualitative security assurance for the critical systems. This project is in line with the goal of providing improvements in the reliability and robustness of CPS which can be achieved by using the abilities of SAT solvers in the formal verification.