Abstract
In this work, we present an actor-based approach for security analysis of Cyber-Physical Systems at the design phase. We use Timed Rebeca, an actor-based modeling language, to model the behavior of components and potential attacks, and verify the security properties using Rebeca model checking tool. We employ STRIDE model as a reference for classifying the attacks. To demonstrate the applicability of our approach, we use a Secure Water Treatment (SWaT) system as a case study. We analyze the architecture of the SWaT system using three different attack schemes in which various parts of the system network and physical devices are compromised. In the end, we identify single and combined attack scenarios that violate security properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The acronym STRIDE stands for Spoofing, Tampering, Reputation, Information Disclosure, Denial of Service, and Elevation of Privilege.
References
Lanotte, R., Merro, M., Muradore, R., Viganò, L.: A formal approach to cyber-physical attacks. In: IEEE 30th Computer Security Foundations Symposium (CSF), pp. 436–450. IEEE (2017)
Adepu, S., Mathur, A., Gunda, J., Djokic, S.: An agent-based framework for simulating and analysing attacks on cyber physical systems. In: Wang, G., Zomaya, A., Perez, G.M., Li, K. (eds.) ICA3PP 2015. LNCS, vol. 9530, pp. 785–798. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27137-8_57
The industrial control systems cyber emergency response team. https://www.us-cert.gov/ics. Accessed 23 Apr 2020
Stallings, W., Brown, L., Bauer, M.D., Bhattacharjee, A.K.: Computer Security: Principles and Practice. Pearson Education, London (2012)
Gollmann, D., Gurikov, P., Isakov, A., Krotofil, M., Larsen, J., Winnicki, A.: Cyber-physical systems security: experimental analysis of a vinyl acetate monomer plant. In: Proceedings of Cyber-Physical System Security, pp. 1–12. ACM (2015)
Kang, E., Adepu, S., Jackson, D., Mathur, A.P.: Model-based security analysis of a water treatment system. In: Proceedings of Software Engineering for Smart Cyber-Physical Systems, pp. 22–28. ACM (2016)
Taormina, R., Galelli, S., Tippenhauer, N.O., Salomons, E., Ostfeld, A.: Characterizing cyber-physical attacks on water distribution systems. J. Water Resour. Plann. Manage. 143(5), 04017009 (2017)
Lanotte, R., Merro, M., Munteanu, A., Viganò, L.: A formal approach to physics-based attacks in cyber-physical systems. ACM Trans. Priv. Secur. (TOPS) 23(1), 1–41 (2020)
Reynisson, A.H., et al.: Modelling and simulation of asynchronous real-time systems using timed Rebeca. Sci. Comput. Program. 89, 41–68 (2014)
Sirjani, M., Khamespanah, E.: On time actors. In: Ábrahám, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 373–392. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30734-3_25
Khamespanah, E., Sirjani, M., Sabahi-Kaviani, Z., Khosravi, R., Izadi, M.: Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci. Comput. Program. 98, 184–204 (2015)
Shostack, A.: Threat Modeling: Designing for Security. Wiley, Hoboken (2014)
Sirjani, M., Movaghar, A., Shali, A., De Boer, F.S.: Modeling and verification of reactive systems using Rebeca. Fundamenta Informaticae 63(4), 385–410 (2004)
Sirjani, M.: Rebeca: theory, applications, and tools. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 102–126. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74792-5_5
Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Formal Modeling: Actors, Open Systems, Biological Systems - Essays, pp. 20–56 (2011)
Afra: an integrated environment for modeling and verifying Rebeca family designs (2019). https://rebeca-lang.org/alltools/Afra. Accessed 09 Nov 2019
Sirjani, M., Khamespanah, E., Lee, E.: Model checking software in cyberphysical systems. In: COMPSAC 2020 (2020)
Giraldo, J., et al.: A survey of physics-based attack detection in cyber-physical systems. ACM Comput. Surv. (CSUR) 51(4), 1–36 (2018)
Choi, S., Yun, J.-H., Kim, S.-K.: A comparison of ICS datasets for security research based on attack paths. In: Luiijf, E., Žutautaitė, I., Hämmerli, B.M. (eds.) CRITIS 2018. LNCS, vol. 11260, pp. 154–166. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-05849-4_12
Flaus, J.-M.: Cybersecurity of Industrial Systems. Wiley, Hoboken (2019)
Mathur, A.P., Tippenhauer, N.O.: SWaT: a water treatment testbed for research and training on ICS security. In: Cyber-physical Systems for Smart Water Networks (CySWater), pp. 31–36. IEEE (2016)
Sirjani, M.: Power is overrated, go for friendliness! Expressiveness, faithfulness, and usability in modeling: the actor experience. In: Principles of Modeling - Essays Dedicated to Edward A. Lee, pp. 423–448 (2018)
Rebeca (2019). http://rebeca-lang.org/Rebeca. Accessed 03 June 2019
Khamespanah, E., Sirjani, M., Mechitov, K., Agha, G.: Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking. Int. J. Softw. Tools Technol. Transfer. 20(5), 547–561 (2017). https://doi.org/10.1007/s10009-017-0480-3
Sharifi, M., Mosaffa, Z., Mohammadi, S., Sirjani, M.: Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. In: ECEASST, vol. 66 (2013)
Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. Formal Aspects Comput. 29(6), 1051–1086 (2017). https://doi.org/10.1007/s00165-017-0429-z
Sirjani, M., Lee, E., Khamespanah, E.: Model checking cyberphysical systems. Mathematics 8(7), 1067 (2020)
Sirjani, M., Provenzano, L., Asadollah, S.A., Moghadam, M.H.: From requirements to verifiable executable models using Rebeca. In: International Workshop on Automated and verifiable Software sYstem DEvelopment, November 2019
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27–30 July 1996, pp. 278–292. IEEE Computer Society (1996)
Samonas, S., Coss, D.: The CIA strikes back: redefining confidentiality, integrity and availability in security. J. Inf. Syst. Secur. 10(3), 21–45 (2014)
iTrust: Secure water treatment (SWaT) dataset (2019). https://itrust.sutd.edu.sg/itrust-labs_datasets/dataset_info/. Accessed 17 Sept 2019
Rebeca (2020). http://rebeca-lang.org/allprojects/CRYSTAL
Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4), 401–424 (1994)
Wasicek, A., Derler, P., Lee, E.A.: Aspect-oriented modeling of attacks in automotive cyber-physical systems. In: ACM/EDAC/IEEE Design Automation Conference (DAC) (2014)
Buck, J., Ha, S., Lee, E.A., Messerschmitt, D.G.: Ptolemy: a framework for simulating and prototyping heterogeneous systems. In: Readings in Hardware/software Co-Design, pp. 527–543 (2001)
Rocchetto, M., Tippenhauer, N.O.: Towards formal security analysis of industrial control systems. In: ACM Asia Conference on Computer and Communications Security, pp. 114–126. ACM (2017)
Fritz, R., Zhang, P.: Modeling and detection of cyber attacks on discrete event systems. IFAC-PapersOnLine 51(7), 285–290 (2018)
Jahandideh, I., Ghassemi, F., Sirjani, M.: Hybrid Rebeca: modeling and analyzing of cyber-physical systems. In: Chamberlain, R., Taha, W., Törngren, M. (eds.) CyPhy/WESE - 2018. LNCS, vol. 11615, pp. 3–27. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-23703-5_1
Acknowledgment
This research is partly supported by Swedish Foundation for Strategic Research (SSF) via the Serendipity project, and KKS SACSys Synergy project (Safe and Secure Adaptive Collaborative Systems).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Moradi, F., Abbaspour Asadollah, S., Sedaghatbaf, A., Čaušević, A., Sirjani, M., Talcott, C. (2020). An Actor-Based Approach for Security Analysis of Cyber-Physical Systems. In: ter Beek, M.H., Ničković, D. (eds) Formal Methods for Industrial Critical Systems. FMICS 2020. Lecture Notes in Computer Science(), vol 12327. Springer, Cham. https://doi.org/10.1007/978-3-030-58298-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-58298-2_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-58297-5
Online ISBN: 978-3-030-58298-2
eBook Packages: Computer ScienceComputer Science (R0)