@inproceedings{karrenberg-wdsa-2022,
author = {Cade Karrenberg and Juan Benavides and Emily Berglund and
  Eunsuk Kang and John Baugh},
title = {Identifying cyber-physical vulnerabilities of water distribution
  systems using finite state processes},
booktitle = {2nd International Joint Conference on Water Distribution
  System Analysis \& Computing and Control in the Water Industry,
  {WDSA CCWI 2022}},
year = {2022},
location = {Universitat Politècnica de València Valencia (Spain)},
number = {14838},
OPTdoi = {not-posted-yet},
url_pdf = {papers/karrenberg-wdsa-2022.pdf},
OPTpublisher = {not-sure},
keywords = {cyber-security, formal methods, water distribution system,
  cyberphysical system, finite state processes},
abstract = {
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.}
}

{"_id":"SaxjgvnmQKZzHFMrR","bibbaseid":"karrenberg-benavides-berglund-kang-baugh-identifyingcyberphysicalvulnerabilitiesofwaterdistributionsystemsusingfinitestateprocesses-2022","author_short":["Karrenberg, C.","Benavides, J.","Berglund, E.","Kang, E.","Baugh, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Cade"],"propositions":[],"lastnames":["Karrenberg"],"suffixes":[]},{"firstnames":["Juan"],"propositions":[],"lastnames":["Benavides"],"suffixes":[]},{"firstnames":["Emily"],"propositions":[],"lastnames":["Berglund"],"suffixes":[]},{"firstnames":["Eunsuk"],"propositions":[],"lastnames":["Kang"],"suffixes":[]},{"firstnames":["John"],"propositions":[],"lastnames":["Baugh"],"suffixes":[]}],"title":"Identifying cyber-physical vulnerabilities of water distribution systems using finite state processes","booktitle":"2nd International Joint Conference on Water Distribution System Analysis & Computing and Control in the Water Industry, WDSA CCWI 2022","year":"2022","location":"Universitat Politècnica de València Valencia (Spain)","number":"14838","optdoi":"not-posted-yet","url_pdf":"papers/karrenberg-wdsa-2022.pdf","optpublisher":"not-sure","keywords":"cyber-security, formal methods, water distribution system, cyberphysical system, finite state processes","abstract":"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.","bibtex":"@inproceedings{karrenberg-wdsa-2022,\nauthor = {Cade Karrenberg and Juan Benavides and Emily Berglund and\n Eunsuk Kang and John Baugh},\ntitle = {Identifying cyber-physical vulnerabilities of water distribution\n systems using finite state processes},\nbooktitle = {2nd International Joint Conference on Water Distribution\n System Analysis \\& Computing and Control in the Water Industry,\n {WDSA CCWI 2022}},\nyear = {2022},\nlocation = {Universitat Politècnica de València Valencia (Spain)},\nnumber = {14838},\nOPTdoi = {not-posted-yet},\nurl_pdf = {papers/karrenberg-wdsa-2022.pdf},\nOPTpublisher = {not-sure},\nkeywords = {cyber-security, formal methods, water distribution system,\n cyberphysical system, finite state processes},\nabstract = {\nModern water distribution systems (WDS) comprise not only physical\ninfrastructure, but also use smart meters, sensors, automated control\nsystems and wireless communication links to manage hydraulic processes\nand water quality. Networked devices create new vulnerabilities to\ncyber-attacks, in which an attacker infiltrates connected devices\nthrough internet and network connections with potentially severe\nconsequences, such as creating water supply interruptions and\ncompromising water quality. Attention to cyber-attacks comes at a time\nof notable intrusions into the computer systems that monitor and\ncontrol infrastructure, including the recent attack on a water\ntreatment plant in Oldsmar, Florida. This paper describes an approach\nfor probing a system's vulnerabilities and finding attack scenarios\nthat may cause a disruption, for example, by lowering the pressure in\nwater mains and exposing a system to harmful contaminants. Our\nmodelling framework uses a process calculus called Finite State\nProcesses (FSP), which is a formal notation that also includes a\nsupporting tool, Labelled Transition System Analyzer (LTSA), for\nautomatically checking safety and other desirable properties of\ncomputer systems. Applying formal methods tools, most-often used in\nthe design and testing of hardware and software systems, to WDSs\nallows us to augment traditional simulation approaches with the\nexhaustive model-checking capabilities of tools such as LTSA. This\nframework couples FSP with epanetCPA, which is an open-source toolbox\nthat can simulate attacks on a system's computer and network\ncomponents to evaluate the resulting hydraulic response. Within this\nframework, we treat WDSs as a bounded state control problem to ensure,\nfor instance, that water levels of an elevated storage tank are always\nwithin an acceptable range. Attacker capabilities are broadly defined\nand modelled to allow communication links to be compromised through\neavesdropping and packet injection attacks. Feasible attack scenarios\nare automatically identified and produced by LTSA, which generates\ncounterexamples to a safety property. To incorporate the physics of\nWDSs into FSP, we discretize and quantize systems and calibrate\nobservable behaviors using Python scripts, including the package Water\nNetwork Tool for Resilience (WNTR). Attack scenarios are simulated\nwith epanetCPA for purposes of validation.}\n}\n\n","author_short":["Karrenberg, C.","Benavides, J.","Berglund, E.","Kang, E.","Baugh, J."],"key":"karrenberg-wdsa-2022","id":"karrenberg-wdsa-2022","bibbaseid":"karrenberg-benavides-berglund-kang-baugh-identifyingcyberphysicalvulnerabilitiesofwaterdistributionsystemsusingfinitestateprocesses-2022","role":"author","urls":{" pdf":"https://jwbaugh.github.io/papers/karrenberg-wdsa-2022.pdf"},"keyword":["cyber-security","formal methods","water distribution system","cyberphysical system","finite state processes"],"metadata":{"authorlinks":{}},"downloads":5,"html":""},"bibtype":"inproceedings","biburl":"https://jwbaugh.github.io/jwb.bib","dataSources":["pewK2DSYXKNLH3TTe"],"keywords":["cyber-security","formal methods","water distribution system","cyberphysical system","finite state processes"],"search_terms":["identifying","cyber","physical","vulnerabilities","water","distribution","systems","using","finite","state","processes","karrenberg","benavides","berglund","kang","baugh"],"title":"Identifying cyber-physical vulnerabilities of water distribution systems using finite state processes","year":2022,"downloads":5}