Cybersecurity is a growing concern in water distribution systems design and management. As our water systems incorporate digital technologies they can become more vulnerable to cyber attacks. Read more about my research that explores these issues.
Cyber water distribution systems (CWDS) include both physical and cyber components, such as smart meters, sensors, automated control systems, and wireless communication links that manage hydraulic processes and water quality. Their addition creates new possibilities as well as vulnerabilities to attacks, since intruders may seek to infiltrate and disrupt systems through network-connected devices. This paper shows how formal methods can be used to identify vulnerabilities in CWDSs. The approach is based on model checking, an automatic verification technique for finite state systems. We describe two different model checking tools, LTSA and nuXmv, and show how they can be used to model small representative CWDSs, check safety properties, and identify vulnerabilities to eavesdropping, packet injection, and other attacks. Our results indicate that model checking tools can be utilized to model CWDS and successfully identify violations in safety properties and other system vulnerabilities including physical violations and communication breaches