journal article
Feb 05, 2020
A Formal Approach to Physics-based Attacks in Cyber-physical Systems
ACM Transactions on Privacy and Security
Vol. 23
No. 1
pp. 1-41
·
Association for Computing Machinery (ACM)
Abstract
We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1) We define a hybrid process calculus to model both CPSs and physics-based attacks. (2) We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands to drive a CPS into an undesired state; we group these attacks into classes and provide the means to assess attack tolerance/vulnerability with respect to a given class of attacks, based on a proper notion of most powerful physics-based attack. (3) We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. (4) We illustrate our definitions and results by formalising a non-trivial running example in U
PPAAL
SMC, the statistical extension of the U
PPAAL
model checker; we use U
PPAAL
SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.
PPAAL
SMC, the statistical extension of the U
PPAAL
model checker; we use U
PPAAL
SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.
Topics
No keywords indexed for this article. Browse by subject →
References
65
[4]
Ezio Bartocci , Jyotirmoy Deshmukh , Alexandre Donzé , Georgios Fainekos , Oded Maler , Dejan Ničković , and Sriram Sankaranarayanan . 2018. Specification-based monitoring of cyber-physical systems: A survey on theory, tools, and applications . In Lectures on Runtime Verification—Introductory and Advanced Topics . Springer , 135--175. DOI:https://doi.org/10.1007/978-3-319-75632-5_5 10.1007/978-3-319-75632-5_5 Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, and Sriram Sankaranarayanan. 2018. Specification-based monitoring of cyber-physical systems: A survey on theory, tools, and applications. In Lectures on Runtime Verification—Introductory and Advanced Topics. Springer, 135--175. DOI:https://doi.org/10.1007/978-3-319-75632-5_5
[5]
Gerd Behrmann , Alexandre David , and Kim G . Larsen . 2004 . A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems (SFM-RT’04) (Lecture Notes in Computer Science), Vol. 3185 . Springer , 200--236. DOI:https://doi.org/10.1007/978-3-540-30080-9_7 10.1007/978-3-540-30080-9_7 Gerd Behrmann, Alexandre David, and Kim G. Larsen. 2004. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems (SFM-RT’04) (Lecture Notes in Computer Science), Vol. 3185. Springer, 200--236. DOI:https://doi.org/10.1007/978-3-540-30080-9_7
[6]
Gerd Behrmann , Alexandre David , Kim G. Larsen , John Håkansson , Paul Pettersson , Wang Yi , and Martijn Hendriks . 2006. UPPAAL 4.0. In Quantitative Evaluation of Systems . IEEE Computer Society , 125--126. DOI:https://doi.org/10.1109/QEST.2006.59 10.1109/QEST.2006.59 Gerd Behrmann, Alexandre David, Kim G. Larsen, John Håkansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. 2006. UPPAAL 4.0. In Quantitative Evaluation of Systems. IEEE Computer Society, 125--126. DOI:https://doi.org/10.1109/QEST.2006.59
[8]
Chiara Bodei Stefano Chessa and Letterio Galletta. 2019. Measuring security in IoT communications. Theoret. Comput. Sci. (2019) 100--124. DOI:https://doi.org/10.1016/j.tcs.2018.12.002 10.1016/j.tcs.2018.12.002
10.1016/j.tcs.2018.12.002
[9]
Chiara Bodei Stefano Chessa and Letterio Galletta. 2019. Measuring security in IoT communications. Theoret. Comput. Sci. (2019) 100--124. DOI:https://doi.org/10.1016/j.tcs.2018.12.002
10.1016/j.tcs.2018.12.002
[10]
Chiara Bodei , Pierpaolo Degano , Gian-Luigi Ferrari , and Letterio Galletta . 2019 . Tracing where IoT data are collected and aggregated . Log. Meth. Comput. Sci. 13 , 3:5 (2019), 1 -- 38 . DOI:https://doi.org/10.23638/LMCS-13(3:5)2017 10.23638/LMCS-13(3:5)2017 Chiara Bodei, Pierpaolo Degano, Gian-Luigi Ferrari, and Letterio Galletta. 2019. Tracing where IoT data are collected and aggregated. Log. Meth. Comput. Sci. 13, 3:5 (2019), 1--38. DOI:https://doi.org/10.23638/LMCS-13(3:5)2017
[18]
Riccardo Focardi and Fabio Martinelli . 1999. A uniform approach for the definition of security properties . In Formal Methods (Lecture Notes in Computer Science) , Vol. 1708 . Springer , 794--813. DOI:https://doi.org/10.1007/3-540-48119-2_44 10.1007/3-540-48119-2_44 Riccardo Focardi and Fabio Martinelli. 1999. A uniform approach for the definition of security properties. In Formal Methods (Lecture Notes in Computer Science), Vol. 1708. Springer, 794--813. DOI:https://doi.org/10.1007/3-540-48119-2_44
[24]
Jairo Giraldo , David I. Urbina , Alvaro A. Cárdenas , Junia Valente , Mustafa Faisal , Justin Ruths , Niels O. Tippenhauer , Henrik Sandberg , and Richard Candell . 2018. A survey of physics-based attack detection in cyber-physical systems. ACM Comput. Surv. 51, 4 ( 2018 ), 76:1--76:36. DOI:https://doi.org/10.1145/3203245 10.1145/3203245 Jairo Giraldo, David I. Urbina, Alvaro A. Cárdenas, Junia Valente, Mustafa Faisal, Justin Ruths, Niels O. Tippenhauer, Henrik Sandberg, and Richard Candell. 2018. A survey of physics-based attack detection in cyber-physical systems. ACM Comput. Surv. 51, 4 (2018), 76:1--76:36. DOI:https://doi.org/10.1145/3203245
[26]
Dieter Gollmann and Marina Krotofil . 2016. Cyber-physical systems security . In The New Codebreakers—Essays Dedicated to David Kahn on the Occasion of His 85th Birthday (Lecture Notes in Computer Science) , Vol. 9100 . Springer , 195--204. DOI:https://doi.org/10.1007/978-3-662-49301-4_14 10.1007/978-3-662-49301-4_14 Dieter Gollmann and Marina Krotofil. 2016. Cyber-physical systems security. In The New Codebreakers—Essays Dedicated to David Kahn on the Occasion of His 85th Birthday (Lecture Notes in Computer Science), Vol. 9100. Springer, 195--204. DOI:https://doi.org/10.1007/978-3-662-49301-4_14
[32]
ICS-CERT. 2015. Cyber-Attack against Ukrainian Critical Infrastructure. (2015). Retrieved from https://ics-cert.us-cert.gov/alerts/IR-ALERT-H-16-056-01. ICS-CERT. 2015. Cyber-Attack against Ukrainian Critical Infrastructure. (2015). Retrieved from https://ics-cert.us-cert.gov/alerts/IR-ALERT-H-16-056-01.
[34]
Marina Krotofil and Alvaro A. Cárdenas . 2013. Resilience of process control systems to cyber-physical attacks . In Proceedings of the Nordic Conference on Secure IT Systems (NordSec 2013) (Lecture Notes in Computer Science) , Vol. 8208 . Springer, 166--182. DOI:https://doi.org/10.1007/978-3-642-41488-6_12 10.1007/978-3-642-41488-6_12 Marina Krotofil and Alvaro A. Cárdenas. 2013. Resilience of process control systems to cyber-physical attacks. In Proceedings of the Nordic Conference on Secure IT Systems (NordSec 2013) (Lecture Notes in Computer Science), Vol. 8208. Springer, 166--182. DOI:https://doi.org/10.1007/978-3-642-41488-6_12
[40]
Ruggero Lanotte , Massimo Merro , Andrei Munteanu , and Luca Viganò . 2019. A formal approach to physics-based attacks in cyber-physical systems (extended version). Retrieved from CoRR abs/1902.04572 ( 2019 ). Ruggero Lanotte, Massimo Merro, Andrei Munteanu, and Luca Viganò. 2019. A formal approach to physics-based attacks in cyber-physical systems (extended version). Retrieved from CoRR abs/1902.04572 (2019).
[41]
[43]
Ruggero Lanotte , Massimo Merro , and Simone Tini . 2020. A probabilistic calculus of cyber-physical systems. Information and Computation ( 2020 ). To appear. Ruggero Lanotte, Massimo Merro, and Simone Tini. 2020. A probabilistic calculus of cyber-physical systems. Information and Computation (2020). To appear.
[48]
Peter Csaba Ölveczky and José Meseguer . 2007 . Semantics and pragmatics of real-time maude . Higher-Ord. Symb. Comput. 20 , 1 -- 2 (2007), 161--196. DOI:https://doi.org/10.1007/s10990-007-9001-5 10.1007/s10990-007-9001-5 Peter Csaba Ölveczky and José Meseguer. 2007. Semantics and pragmatics of real-time maude. Higher-Ord. Symb. Comput. 20, 1--2 (2007), 161--196. DOI:https://doi.org/10.1007/s10990-007-9001-5
[49]
André Platzer . 2018. Logical Foundations of Cyber-Physical Systems . Springer . DOI:https://doi.org/10.1007/978-3-319-63588-0 10.1007/978-3-319-63588-0 André Platzer. 2018. Logical Foundations of Cyber-Physical Systems. Springer. DOI:https://doi.org/10.1007/978-3-319-63588-0
Showing 50 of 65 references
Cited By
43
Generating resilience curves in availability and integrity through cyberattack modeling using timed colored Petri nets
SICE Journal of Control, Measuremen...
Daisuke Tsuji, Junya Fujita · 2025
Metrics
43
Citations
65
References
Details
- Published
- Feb 05, 2020
- Vol/Issue
- 23(1)
- Pages
- 1-41
- License
- View
Authors
Funding
Italian Ministry of Education
Universities and Research
Cite This Article
Ruggero Lanotte, Massimo Merro, Andrei Munteanu, et al. (2020). A Formal Approach to Physics-based Attacks in Cyber-physical Systems. ACM Transactions on Privacy and Security, 23(1), 1-41. https://doi.org/10.1145/3373270
Related
You May Also Like
A General Framework for Adversarial Examples with Objectives
Mahmood Sharif, Sruti Bhagavatula · 2019
147 citations
Deepfake Detection Model Combining Texture Differences and Frequency Domain Information
Shuaijv Fang, Zhiyong Zhang · 2025
12 citations
Multi-Stage Enhanced Zero Trust Intrusion Detection System for Unknown Attack Detection in Internet of Things and Traditional Networks
Malek Al-Zewairi, Sufyan Almajali · 2025
9 citations