An Approach for Formal Analysis of the Security of a Water Treatment Testbed

摘要

An increase in the number of attacks on cyberphysical systems (CPS) has raised concerns over the vulnerability of critical infrastructure such as water treatment, oil, gas plants, against cyber attacks. Such systems are controlled by an Industrial Control System (ICS) that includes controllers communicating with each other, and with physical sensors and actuators, using a communications network. This paper focuses on a Multiple Security Domain Nondeducibility (MSDND) model to identify the vulnerable points of attack on the system that hide critical information rather than steal it, such as in the STUXNET virus. It is shown how MSDND analysis, conducted on a realistic multi-stage water treatment testbed, is useful in enhancing the security of a water treatment plant. Based on the MSDND analysis, this work offers a thorough documentation on the vulnerable points of attack, invariants used for removing the vulnerabilities, and suggested design decisions that help in developing invariants to mitigate attacks.