research-article

Model-based security analysis of a water treatment system

Authors:

Daniel Jackson,

Aditya P. MathurAuthors Info & Claims

SEsCPS '16: Proceedings of the 2nd International Workshop on Software Engineering for Smart Cyber-Physical Systems

Pages 22 - 28

https://doi.org/10.1145/2897035.2897041

Published: 14 May 2016 Publication History

Abstract

An approach to analyzing the security of a cyber-physical system (CPS) is proposed, where the behavior of a physical plant and its controller are captured in approximate models, and their interaction is rigorously checked to discover potential attacks that involve a varying number of compromised sensors and actuators. As a preliminary study, this approach has been applied to a fully functional water treatment testbed constructed at the Singapore University of Technology and Design. The analysis revealed previously unknown attacks that were confirmed to pose serious threats to the safety of the testbed, and suggests a number of research challenges and opportunities for applying a similar type of formal analysis to cyber-physical security.

References

[1]

SWaT: Secure Water Treatment Testbed, 2015. https://itrust.sutd.edu.sg/wp-content/uploads/sites/3/2015/11/Brief-Introduction-to-SWaT_181115.pdf.

[2]

Alloy language and analyzer. http://alloy.mit.edu.

[3]

Daniel Jackson. Software Abstractions: logic, language, and analysis. MIT Press, Second edition, 2012.

Digital Library

[4]

Emina Torlak and Daniel Jackson. Kodkod: A relational model finder. In Tools and Algorithms for the Construction and Analysis of Systems TACAS Portugal, 2007., pages 632--647, 2007.

Digital Library

[5]

Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238--252. ACM, 1977.

Digital Library

[6]

David. Urbina, Jairo. Giraldo, Nils Ole. Tippenhauer, and Alvaro Cardenas. Attacking fieldbus communications in ics: Applications to the swat testbed. In Proc. Singapore Cyber-Security Conference (SG-CRC), pages 75--89, 2016.

[7]

André Platzer. Logical analysis of hybrid systems: proving theorems for complex dynamics. Springer Science & Business Media, 2010.

Digital Library

[8]

Sicun Gao, Soonho Kong, and Edmund M Clarke. dreal: An SMT solver for nonlinear theories over the reals. In Automated Deduction--CADE-24, pages 208--214. Springer, 2013.

Digital Library

[9]

Alessandro Cimatti, Sergio Mover, and Stefano Tonetta. SMT-based verification of hybrid systems. In AAAI, 2012.

Digital Library

[10]

Mathworks. Matlab. http://www.mathworks.com/products/matlab/.

[11]

Mathworks. Simulink. http://www.mathworks.com/products/simulink/.

[12]

Ravi Akella and Bruce M McMillin. Model-checking bndc properties in cyber-physical systems. In Computer Software and Applications Conference, 2009. COMPSAC'09. 33rd Annual IEEE International, volume 1, pages 660--663. IEEE, 2009.

Digital Library

[13]

Chih-Hong Cheng, Natarajan Shankar, Harald Ruess, and Saddek Bensalem. EFSMT: A logical framework for cyber-physical systems. arXiv preprint arXiv:1306.3456, 2013.

[14]

Edmund M Clarke and Paolo Zuliani. Statistical model checking for cyber-physical systems. In Automated Technology for Verification and Analysis, pages 1--12. Springer, 2011.

Digital Library

[15]

Dean H Stamatis. Failure mode and effect analysis: FMEA from theory to execution. ASQ Quality Press, 2003.

[16]

William E Vesely, Francine F Goldberg, Norman H Roberts, and David F Haasl. Fault tree handbook. Technical report, DTIC Document, 1981.

[17]

X. Zheng, C. Julien, M. Kim, and S. Khurshid. Perceptions on the state of the art in verification and validation in cyber-physical systems. Systems Journal, IEEE, PP(99):1--14, 2015.

[18]

Sridhar Adepu, Aditya Mathur, Jagadeesh Gunda, and Sasa Djokic. An agent-based framework for simulating and analysing attacks on cyber physical systems. In Algorithms and Architectures for Parallel Processing, pages 785--798. Springer, 2015.

[19]

S. Adepu and A. Mathur. An investigation into the response of a water treatment system to cyber attacks. In Proceedings of the 17th IEEE High Assurance Systems Engineering Symposium, Orlando, January 2016.

Digital Library

Cited By

Li NZhang MLi JAdepu SKang EJin Z(2024)A Game-Theoretical Self-Adaptation Framework for Securing Software-Intensive SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/365294919:2(1-49)Online publication date: 20-Apr-2024
https://dl.acm.org/doi/10.1145/3652949
Moradi FAbbaspour Asadollah SPourvatan BMoezkarimi ZSirjani M(2024)CRYSTAL Framework: Cybersecurity Assurance for Cyber-Physical SystemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100965(100965)Online publication date: Mar-2024
https://doi.org/10.1016/j.jlamp.2024.100965
Ahmad FChaudhry MJamal MSohail MGavilanes DVergara MAshraf I(2023)Formal modeling and analysis of security schemes of RPL protocol using colored Petri netsPLOS ONE10.1371/journal.pone.028570018:8(e0285700)Online publication date: 17-Aug-2023
https://doi.org/10.1371/journal.pone.0285700
Show More Cited By

Recommendations

POSTER: Defense against False Data Injection Attack in a Cyber-Physical System
ASIA CCS '24: Proceedings of the 19th ACM Asia Conference on Computer and Communications Security

Cyber-physical systems (CPSs) are closed-loop feedback systems that efficiently control the physical processes through cyber-systems. Security threats like false data injection (FDI) attacks are increasing in CPSs. FDI attacks disrupt the system's ...
Automatic web security unit testing: XSS vulnerability detection
AST '16: Proceedings of the 11th International Workshop on Automation of Software Test

Integrating security testing into the workflow of software developers not only can save resources for separate security testing but also reduce the cost of fixing security vulnerabilities by detecting them early in the development cycle. We present an ...
Design and Analysis of Security Attacks against Critical Smart Grid Infrastructures
ICECCS '14: Proceedings of the 2014 19th International Conference on Engineering of Complex Computer Systems

Smart grid, the future power grid, is expected to provide better energy efficiency, more customer choices and improved reliability and security. As the smart grid is an integrated system that consists of multiple subsystems, understanding it as a whole ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SEsCPS '16: Proceedings of the 2nd International Workshop on Software Engineering for Smart Cyber-Physical Systems

May 2016

71 pages

ISBN:9781450341714

DOI:10.1145/2897035

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS\DATC: IEEE Computer Society
TCSE: IEEE Computer Society's Tech. Council on Software Engin.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 May 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE '16

Sponsor:

ACM
SIGSOFT
IEEE-CS\DATC
TCSE

ICSE '16: 38th International Conference on Software Engineering

May 14 - 22, 2016

Texas, Austin

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

50
Total Citations
View Citations
409
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)2

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li NZhang MLi JAdepu SKang EJin Z(2024)A Game-Theoretical Self-Adaptation Framework for Securing Software-Intensive SystemsACM Transactions on Autonomous and Adaptive Systems10.1145/365294919:2(1-49)Online publication date: 20-Apr-2024
https://dl.acm.org/doi/10.1145/3652949
Moradi FAbbaspour Asadollah SPourvatan BMoezkarimi ZSirjani M(2024)CRYSTAL Framework: Cybersecurity Assurance for Cyber-Physical SystemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100965(100965)Online publication date: Mar-2024
https://doi.org/10.1016/j.jlamp.2024.100965
Ahmad FChaudhry MJamal MSohail MGavilanes DVergara MAshraf I(2023)Formal modeling and analysis of security schemes of RPL protocol using colored Petri netsPLOS ONE10.1371/journal.pone.028570018:8(e0285700)Online publication date: 17-Aug-2023
https://doi.org/10.1371/journal.pone.0285700
Zhang FWu QXuan BChen YLin WPoskitt CSun JChen B(2023)Constructing Cyber-Physical System Testing Suites Using Active Sensor FuzzingIEEE Transactions on Software Engineering10.1109/TSE.2023.330933049:11(4829-4845)Online publication date: Nov-2023
https://doi.org/10.1109/TSE.2023.3309330
Sobien DYardimci MNguyen MMao WFordham VRahman ADuncan SBatarseh F(2023)AI for Cyberbiosecurity in Water Systems—A SurveyCyberbiosecurity10.1007/978-3-031-26034-6_13(217-263)Online publication date: 11-Jan-2023
https://doi.org/10.1007/978-3-031-26034-6_13
Serru TNguyen NBatteux MRauzy A(2022)Modeling Cyberattack Propagation and Impacts on Cyber-Physical System Safety: An ExperimentElectronics10.3390/electronics1201007712:1(77)Online publication date: 25-Dec-2022
https://doi.org/10.3390/electronics12010077
Shi LKrishnan SWen S(2022)Study Cybersecurity of Cyber Physical System in the Virtual Environment: A Survey and New DirectionProceedings of the 2022 Australasian Computer Science Week10.1145/3511616.3513098(46-55)Online publication date: 14-Feb-2022
https://dl.acm.org/doi/10.1145/3511616.3513098
Asadollah S(2022)Cyberattacks: Modeling, Analysis, and Mitigation2022 6th International Conference on Computer, Software and Modeling (ICCSM)10.1109/ICCSM57214.2022.00021(80-84)Online publication date: Jul-2022
https://doi.org/10.1109/ICCSM57214.2022.00021
Serna JDay NEsmaeilsabzali S(2022)Dash: declarative behavioural modelling in Alloy with control state hierarchySoftware and Systems Modeling10.1007/s10270-022-01012-122:2(733-749)Online publication date: 6-Aug-2022
https://doi.org/10.1007/s10270-022-01012-1
Kittelmann ARunge TBordis TSchaefer I(2022)Runtime Verification of Correct-by-Construction Driving ManeuversLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_15(242-263)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19849-6_15
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents