Abstract
We propose a method to detect attacks on sensors and controllers in cyber-physical systems. We develop a monitor that uses an abstract digital twin, Tiny Twin, to detect false sensor data and faulty control commands. The Tiny Twin is a state transition system that represents the observable behavior of the system from the monitor point of view. At runtime, the monitor observes the sensor data and the control commands, and checks whether the observed data and commands are consistent with the state transitions in the Tiny Twin. The monitor produces an alarm when an inconsistency is detected. We model the components of the system and the physical processes in the Rebeca modeling language and use its model checker to generate the state space. The Tiny Twin is built automatically by reducing the state space, keeping the observable behavior of the system, and preserving the trace equivalence. We demonstrate the method and evaluate it in detecting attacks using a temperature control system.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Afra: An integrated environment for modeling and verifying Rebeca family designs (2021). https://rebeca-lang.org/alltools/Afra. Accessed 09 July 2021
Abera, T., et al.: C-FLAT: control-flow attestation for embedded systems software. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 743–754 (2016)
Bagheri, M., et al.: Coordinated actor model of self-adaptive track-based traffic control systems. J. Syst. Softw. 143, 116–139 (2018)
Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_9
Carvalho, L.K., Wu, Y.C., Kwong, R., Lafortune, S.: Detection and mitigation of classes of attacks in supervisory control systems. Automatica 97, 121–133 (2018)
Cheng, B.H.C., et al.: Using models at runtime to address assurance for self-adaptive systems. In: Bencomo, N., France, R., Cheng, B.H.C., Aßmann, U. (eds.) Models@run.time. LNCS, vol. 8378, pp. 101–136. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08915-7_4
Cheng, L., Tian, K., Yao, D., Sha, L., Beyah, R.A.: Checking is believing: event-aware program anomaly detection in cyber-physical systems. IEEE Trans. Dependable Secure Comput. 18(2), 825–842 (2019)
Corbett, J.C., et al.: Spanner: Google’s globally distributed database. ACM Trans. Comput. Syst. 31(3), 1–22 (2013)
Dureuil, L., Petiot, G., Potet, M.-L., Le, T.-H., Crohen, A., de Choudens, P.: FISSC: a fault injection and simulation secure collection. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 3–11. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45477-1_1
Eckhart, M., Ekelhart, A.: A specification-based state replication approach for digital twins. In: Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and Privacy, pp. 36–47 (2018)
Gao, C., Seatzu, C., Li, Z., Giua, A.: Multiple attacks detection on discrete event systems. In: 2019 IEEE International Conference on Systems, Man and Cybernetics (SMC), pp. 2352–2357. IEEE (2019)
Hewitt, C.: Viewing control structures as patterns of passing messages. Artif. Intell. 8(3), 323–364 (1977)
Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In: TACAS 2020. LNCS, vol. 12079, pp. 3–20. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_1
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)
Kassem, A., Falcone, Y.: Detecting fault injection attacks with runtime verification. In: Proceedings of the 3rd ACM Workshop on Software Protection, pp. 65–76 (2019)
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)
Křikava, F., Collet, P., France, R.B.: Actor-based runtime model of adaptable feedback control loops. In: Proceedings of the 7th Workshop on Models@ run. time, pp. 39–44 (2012)
Lanotte, R., Merro, M., Munteanu, A.: A process calculus approach to detection and mitigation of PLC malware. Theoret. Comput. Sci. 890, 125–146 (2021)
Lee, E., Seo, Y.D., Kim, Y.G.: A cache-based model abstraction and runtime verification for the internet-of-things applications. IEEE Internet Things J. 7(9), 8886–8901 (2020)
Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1), 2–16 (2005)
Lima, P.M., Alves, M.V., Carvalho, L.K., Moreira, M.V.: Security against network attacks in supervisory control systems. IFAC-PapersOnLine 50(1), 12333–12338 (2017)
Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a Lingua Franca for deterministic concurrent systems. ACM Trans. Embed. Comput. Syst. 20(4), 1–27 (2021)
Lohstroh, M., Menard, C., Schulz-Rosengarten, A., Weber, M., Castrillon, J., Lee, E.A.: A language for deterministic coordination across multiple timelines. In: 2020 Forum for Specification and Design Languages (FDL), pp. 1–8. IEEE (2020)
Lohstroh, M., et al.: Reactors: a deterministic model for composable reactive systems. In: Chamberlain, R., Edin Grimheden, M., Taha, W. (eds.) CyPhy/WESE - 2019. LNCS, vol. 11971, pp. 59–85. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-41131-2_4
Loulou, H., Saudrais, S., Soubra, H., Larouci, C.: Adapting security policy at runtime for connected autonomous vehicles. In: 2016 IEEE 25th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 26–31. IEEE (2016)
Mitchell, R., Chen, I.R.: A survey of intrusion detection techniques for cyber-physical systems. ACM Comput. Surv. 46(4), 1–29 (2014)
Mohan, S., Bak, S., Betti, E., Yun, H., Sha, L., Caccamo, M.: S3a: secure system simplex architecture for enhanced security and robustness of cyber-physical systems. In: Proceedings of the 2nd ACM International Conference on High Confidence Networked Systems, pp. 65–74 (2013)
Moradi, F., Abbaspour Asadollah, S., Sedaghatbaf, A., Čaušević, A., Sirjani, M., Talcott, C.: An actor-based approach for security analysis of cyber-physical systems. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 130–147. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_5
Ptolemaeus, C.: System design, modeling, and simulation: using Ptolemy II, vol. 1. Ptolemy. org Berkeley (2014)
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., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20–56. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24933-4_3
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
Sirjani, M., Lee, E.A., Khamespanah, E.: Verification of cyberphysical systems. Mathematics 8(7), 1068 (2020)
Zhang, Q., Li, Z., Seatzu, C., Giua, A.: Stealthy attacks for partially-observed discrete event systems. In: 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), vol. 1, pp. 1161–1164. IEEE (2018)
Zhao, Y., Liu, J., Lee, E.A.: A programming model for time-synchronized distributed real-time systems. In: 13th IEEE Real Time and Embedded Technology and Applications Symposium (RTAS 2007), pp. 259–268. IEEE (2007)
Acknowledgment
The work of a subset of authors is partly supported by SSF Serendipity project, KKS DPAC Project (Dependable Platforms for Autonomous Systems and Control), 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
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Moradi, F., Bagheri, M., Rahmati, H., Yazdi, H., Asadollah, S.A., Sirjani, M. (2022). Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-Attacks. In: Legunsen, O., Rosu, G. (eds) Model Checking Software. SPIN 2022. Lecture Notes in Computer Science, vol 13255. Springer, Cham. https://doi.org/10.1007/978-3-031-15077-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-031-15077-7_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-15076-0
Online ISBN: 978-3-031-15077-7
eBook Packages: Computer ScienceComputer Science (R0)