Automated Security Domain Partitioning with a Formal Method Perspective of a Cyber-Physical Systems

Modern society increasingly relies on the correct functioning of a myriad of interacting Cyber-Physical Systems (CPS) such as water systems, electric power grids, and air traffic control systems. Two critical vulnerabilities pre-sent in these systems are the potential for information leakage and suscep-tibility to deceptive information. The goal of this project is to improve CPS information security by automating the complex task of optimally partition-ing the system into security domains. Automated Theorem Provers are employed to automate testing partition quality. Testing is performed by ex-amining each pairwise connection in a system to determine whether it is Multi-Security Domain Non-Deducibility (MSDND) secure. The performance measure of each partition is then obtained by taking the percentage of con-nections that are MSDND secure. This implies that a higher percentage of secure connections corresponds to a higher performance measure and in turn a better partitioning of a CPS into information flow security domains