Identifying cyber-physical vulnerabilities of water distribution systems using finite state processes. Karrenberg, C., Benavides, J., Berglund, E., Kang, E., & Baugh, J. In 2nd International Joint Conference on Water Distribution System Analysis & Computing and Control in the Water Industry, WDSA CCWI 2022, 2022.
Identifying cyber-physical vulnerabilities of water distribution systems using finite state processes [pdf]Pdf  abstract   bibtex   
Modern water distribution systems (WDS) comprise not only physical infrastructure, but also use smart meters, sensors, automated control systems and wireless communication links to manage hydraulic processes and water quality. Networked devices create new vulnerabilities to cyber-attacks, in which an attacker infiltrates connected devices through internet and network connections with potentially severe consequences, such as creating water supply interruptions and compromising water quality. Attention to cyber-attacks comes at a time of notable intrusions into the computer systems that monitor and control infrastructure, including the recent attack on a water treatment plant in Oldsmar, Florida. This paper describes an approach for probing a system's vulnerabilities and finding attack scenarios that may cause a disruption, for example, by lowering the pressure in water mains and exposing a system to harmful contaminants. Our modelling framework uses a process calculus called Finite State Processes (FSP), which is a formal notation that also includes a supporting tool, Labelled Transition System Analyzer (LTSA), for automatically checking safety and other desirable properties of computer systems. Applying formal methods tools, most-often used in the design and testing of hardware and software systems, to WDSs allows us to augment traditional simulation approaches with the exhaustive model-checking capabilities of tools such as LTSA. This framework couples FSP with epanetCPA, which is an open-source toolbox that can simulate attacks on a system's computer and network components to evaluate the resulting hydraulic response. Within this framework, we treat WDSs as a bounded state control problem to ensure, for instance, that water levels of an elevated storage tank are always within an acceptable range. Attacker capabilities are broadly defined and modelled to allow communication links to be compromised through eavesdropping and packet injection attacks. Feasible attack scenarios are automatically identified and produced by LTSA, which generates counterexamples to a safety property. To incorporate the physics of WDSs into FSP, we discretize and quantize systems and calibrate observable behaviors using Python scripts, including the package Water Network Tool for Resilience (WNTR). Attack scenarios are simulated with epanetCPA for purposes of validation.

Downloads: 0