nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation

verfasst von : Yuqi Chen, Christopher M. Poskitt, Jun Sun

Erschienen in: FM 2016: Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Cyber-physical systems (CPS), which integrate algorithmic control with physical processes, often consist of physically distributed components communicating over a network. A malfunctioning or compromised component in such a CPS can lead to costly consequences, especially in the context of public infrastructure. In this short paper, we argue for the importance of constructing invariants (or models) of the physical behaviour exhibited by CPS, motivated by their applications to the control, monitoring, and attestation of components. To achieve this despite the inherent complexity of CPS, we propose a new technique for learning invariants that combines machine learning with ideas from mutation testing. We present a preliminary study on a water treatment system that suggests the efficacy of this approach, propose strategies for establishing confidence in the correctness of invariants, then summarise some research questions and the steps we are taking to investigate them.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Validated Simulation-Based Verification of Delayed Differential Dynamics

Nächstes Kapitel From Electrical Switched Networks to Hybrid Automata

Secure Water Treatment (SWaT). http://itrust.sutd.edu.sg/research/testbeds/secure-water-treatment-swat/. Accessed Sep 2016

Supplementary material. http://sav.sutd.edu.sg/?page_id=3258

Adepu, S., Mathur, A.: Distributed detection of single-stage multipoint cyber attacks in a water treatment plant. In: Proceedings of ACM Asia Conference on Computer and Communications Security (AsiaCCS 2016), pp. 449–460. ACM (2016)

Adepu, S., Mathur, A.: Using process invariants to detect cyber attacks on a water treatment system. In: Hoepman, J.-H., Katzenbeisser, S. (eds.) Proceedings of International Conference on ICT Systems Security and Privacy Protection (SEC 2016). IFIP AICT, vol. 471, pp. 91–104. Springer, New York (2016)CrossRef

Alves, T., Felton, D.: TrustZone: integrated hardware and software security. ARM white paper (2004)

Anati, I., Gueron, S., Johnson, S.P., Scarlata, V.R.: Innovative technology for CPU based attestation and sealing. Intel white paper (2013)

Cárdenas, A.A., Amin, S., Sastry, S.: Research challenges for the security of control systems. In: Proceedings of USENIX Workshop on Hot Topics in Security (HotSec 2008). USENIX Association (2008)

Castelluccia, C., Francillon, A., Perito, D., Soriente, C.: On the difficulty of software-based attestation of embedded devices. In: Proceedings of ACM Conference on Computer and Communications Security (CCS 2009), pp. 400–409. ACM (2009)

Choudhari, A., Ramaprasad, H., Paul, T., Kimball, J.W., Zawodniok, M.J., McMillin, B.M., Chellappan, S.: Stability of a cyber-physical smart grid system using cooperating invariants. In: Proceedings of IEEE Computer Software and Applications Conference (COMPSAC 2013), pp. 760–769. IEEE (2013)

10.

Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1–12. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_1 CrossRef

11.

Frehse, G., Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30 CrossRef

12.

Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_14 CrossRef

13.

Hasuo, I., Suenaga, K.: Exercises in nonstandard static analysis of hybrid systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 462–478. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_34 CrossRef

14.

Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649–678 (2011)CrossRef

15.

Kang, E., Adepu, S., Jackson, D., Mathur, A.P.: Model-based security analysis of a water treatment system. In: Proceedings of International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS 2016), pp. 22–28. ACM (2016)

16.

Khaitan, S.K., McCalley, J.D.: Design techniques and applications of cyberphysical systems: a survey. IEEE Syst. J. 9(2), 350–365 (2015)CrossRef

17.

Kong, P., Li, Y., Chen, X., Sun, J., Sun, M., Wang, J.: Towards concolic testing for hybrid systems. In: Fitzgerald, J., et al. (eds.) FM 2016. LNCS-FM, vol. 9995, pp. 460–478. Springer, Heidelberg (2016)CrossRef

18.

Lee, E.A.: Cyber physical systems: design challenges. In: Proceedings of International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), pp. 363–369. IEEE (2008)

19.

Maier, A.: Online passive learning of timed automata for cyber-physical production systems. In: Proceedings of IEEE International Conference on Industrial Informatics (INDIN 2014), pp. 60–66. IEEE (2014)

20.

Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 199–214. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11164-3_17

21.

Offutt, A.J., Lee, A., Rothermel, G., Untch, R.H., Zapf, C.: An experimental determination of sufficient mutant operators. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(2), 99–118 (1996)CrossRef

22.

Paul, T., Kimball, J.W., Zawodniok, M.J., Roth, T.P., McMillin, B.M., Chellappan, S.: Unified invariants for cyber-physical switched system stability. IEEE Trans. Smart Grid 5(1), 112–120 (2014)CrossRef

23.

Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71070-7_15 CrossRef

24.

Quesel, J., Mitsch, S., Loos, S.M., Arechiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transf. 18(1), 67–91 (2016)CrossRef

25.

Roth, T., McMillin, B.: Physical attestation of cyber processes in the smart grid. In: Luiijf, E., Hartel, P. (eds.) CRITIS 2013. LNCS, vol. 8328, pp. 96–107. Springer, Heidelberg (2013). doi:10.1007/978-3-319-03964-0_9 CrossRef

26.

Seshadri, A., Perrig, A., van Doorn, L., Khosla, P.K.: SWATT: software-based ATTestation for embedded devices. In: Proceedings of IEEE Symposium on Security and Privacy (S&P 2004), p. 272. IEEE (2004)

27.

Valente, J., Barreto, C., Cárdenas, A.A.: Cyber-physical systems attestation. In: Proceedings of IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS 2014), pp. 354–357. IEEE (2014)

28.

Vodencarevic, A., Kleine Büning, H., Niggemann, O., Maier, A.: Identifying behavior models for process plants. In: Proceedings of IEEE Conference on Emerging Technologies & Factory Automation (ETFA 2011), pp. 1–8. IEEE (2011)

29.

Wang, J., Sun, J., Yuan, Q., Pang, J.: Should we learn probabilistic models for model checking? a new approach and an empirical study. CoRR abs/1605.08278 (2016). http://arxiv.org/abs/1605.08278

30.

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

Titel: Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
verfasst von: Yuqi Chen
Christopher M. Poskitt
Jun Sun
Verlag: Springer International Publishing
Buch: FM 2016: Formal Methods
Print ISBN: 978-3-319-48988-9

Electronic ISBN: 978-3-319-48989-6

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-48989-6_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"