Skip to main content
SpringerLink
Log in

Co-engineering Safety and Security in Industrial Control Systems: A Formal Outlook

  • Conference paper
  • First Online:
Software Engineering for Resilient Systems (SERENE 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10479))

Included in the following conference series:

Abstract

An increasing openness and interconnectedness of safety-critical industrial control systems makes them vulnerable to security attacks. Hence, we should establish the integrated approaches enabling safety-security co-engineering. Such approaches should support an analysis of interdependencies between the mechanisms required for safety and security assurance. In this paper, we demonstrate how formal modelling can facilitate reasoning about the impact of certain security solutions on safety and vise versa. We rely on modelling and refinement in Event-B to systematically uncover mutual interdependencies and the constraints that should be imposed on the system to guarantee its safety even in the presence of security attacks. The approach is illustrated by a case study – a battery charging system of an electric car.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abrial, J.R.: Modeling in Event-B. Cambridge University Press, New York (2010)

    Book  MATH  Google Scholar 

  2. Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157. Springer, Heidelberg (2006)

    Google Scholar 

  3. Cimatti, A., DeLong, R., Marcantonio, D., Tonetta, S.: Combining MILS with contract-based design for safety and security requirements. In: Koornneef, F., Gulijk, C. (eds.) SAFECOMP 2015. LNCS, vol. 9338, pp. 264–276. Springer, Cham (2015). doi:10.1007/978-3-319-24249-1_23

    Chapter  Google Scholar 

  4. Fovino, I.N., Masera, M., Cian, A.D.: Integrating cyber attacks within fault trees. Rel. Eng. Sys. Safety 94(9), 1394–1402 (2009)

    Article  Google Scholar 

  5. Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Supporting reuse in Event-B development: modularisation approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 174–188. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11811-1_14

    Chapter  Google Scholar 

  6. Iliasov, A., Romanovsky, A., Laibinis, L., Troubitsyna, E., Latvala, T.: Augmenting Event-B modelling with real-time verification. In: Proceedings of the FormSERA 2012, pp. 51–57. IEEE (2012)

    Google Scholar 

  7. Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A.: Patterns for refinement automation. In: Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 70–88. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17071-3_4

    Chapter  Google Scholar 

  8. Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Developing mode-rich satellite software by refinement in event-B. Sci. Comput. Program. 78(7), 884–905 (2013)

    Article  Google Scholar 

  9. Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Väisänen, P., Ilic, D., Latvala, T.: Verifying mode consistency for on-board satellite software. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 126–141. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15651-9_10

    Chapter  Google Scholar 

  10. Sere, K., Troubitsyna, E.A.: Probabilities in action systems. In: Proceedings of the 8th Nordic Workshop on Programming Theory, pp. 373–387 (1996)

    Google Scholar 

  11. Kelly, T.P., Weaver, R.A.: The goal structuring notation - a safety argument notation. In: DSN 2004, Workshop on Assurance Cases (2004)

    Google Scholar 

  12. Kriaa, S., Bouissou, M., Colin, F., Halgand, Y., Pietre-Cambacedes, L.: Safety and security interactions modeling using the BDMP formalism: case study of a pipeline. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 326–341. Springer, Cham (2014). doi:10.1007/978-3-319-10506-2_22

    Google Scholar 

  13. Laibinis, L., Troubitsyna, E.: Fault tolerance in a layered architecture: a general specification pattern in B. In: SEFM 2004, Beijing, China, pp. 346–355. IEEE Computer Society (2004)

    Google Scholar 

  14. Laibinis, L., Troubitsyna, E.: Refinement of fault tolerant control systems in B. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 254–268. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30138-7_22

    Chapter  Google Scholar 

  15. Laibinis, L., Troubitsyna, E.: Fault tolerance in use-case modeling. In: Proceedings of RHAS 2005 (2005)

    Google Scholar 

  16. Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Boston (1995)

    Google Scholar 

  17. Lopatkin, I., Iliasov, A., Romanovsky, A., Prokhorova, Y., Troubitsyna, E.: Patterns for representing FMEA in formal specification of control systems. In: HASE 2011, Boca Raton, FL, USA, pp. 146–151. IEEE Computer Society (2011)

    Google Scholar 

  18. McIver, A., Morgan, C., Troubitsyna, E.: The probabilistic steam boiler: a case study in probabilistic data refinement. In: Proceedings of the International Refinement Workshop, Canberra, Australia, pp. 250–265. Springer (1998)

    Google Scholar 

  19. Paul, S., Rioux, L.: Over 20 years of research into cybersecurity and safety engineering: a short bibliography. Saf. Secur. Eng. VI 151, 335 (2015)

    Article  Google Scholar 

  20. Pereverzeva, I., Troubitsyna, E., Laibinis, L.: Formal development of critical multi-agent systems: a refinement approach. In: EDCC 2012, pp. 156–161 (2012)

    Google Scholar 

  21. Ponsard, C., Dallons, G., Massonet, P.: Goal-oriented co-engineering of security and safety requirements in cyber-physical systems. In: Skavhaug, A., Guiochet, J., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9923, pp. 334–345. Springer, Cham (2016). doi:10.1007/978-3-319-45480-1_27

    Chapter  Google Scholar 

  22. Prokhorova, Y., Laibinis, L., Troubitsyna, E.: Facilitating construction of safety cases from formal models in Event-B. Inform. Softw. Technol. 60, 51–76 (2015)

    Article  Google Scholar 

  23. Rodin: Event-B platform. http://www.event-b.org/

  24. Schmittner, C., Ma, Z., Puschner, P.: Limitation and improvement of STPA-Sec for safety and security co-analysis. In: Skavhaug, A., Guiochet, J., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9923, pp. 195–209. Springer, Cham (2016). doi:10.1007/978-3-319-45480-1_16

    Chapter  Google Scholar 

  25. Schmittner, C., Ma, Z., Smith, P.: FMVEA for safety and security analysis of intelligent and cooperative vehicles. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds.) SAFECOMP 2014. LNCS, vol. 8696, pp. 282–288. Springer, Cham (2014). doi:10.1007/978-3-319-10557-4_31

    Google Scholar 

  26. Sere, K., Troubitsyna, E.: Hazard analysis in formal specification. In: Proceedings of the 18th International Conference, SAFECOMP 1999, pp. 350–360 (1999)

    Google Scholar 

  27. Tarasyuk, A., Pereverzeva, I., Troubitsyna, E., Latvala, T., Nummila, L.: Formal development and assessment of a reconfigurable on-board satellite system. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012. LNCS, vol. 7612, pp. 210–222. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33678-2_18

    Chapter  Google Scholar 

  28. Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Quantitative verification of system safety in Event-B. In: Troubitsyna, E.A. (ed.) SERENE 2011. LNCS, vol. 6968, pp. 24–39. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24124-6_3

    Chapter  Google Scholar 

  29. Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Integrating stochastic reasoning into Event-B development. Formal Asp. Comput. 27(1), 53–77 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  30. Troubitsyna, E.: Enhancing dependability via parameterized refinement. In: PRDC 1999, Hong Kong, p. 120. IEEE Computer Society (1999)

    Google Scholar 

  31. Troubitsyna, E.: Stepwise Development of Dependable Systems. Technical report (2000)

    Google Scholar 

  32. Troubitsyna, E.: Elicitation and specification of safety requirements. In: ICONS 2008, Cancun, Mexico, pp. 202–207. IEEE Computer Society (2008)

    Google Scholar 

  33. Troubitsyna, E., Laibinis, L., Pereverzeva, I., Kuismin, T., Ilic, D., Latvala, T.: Towards security-explicit formal modelling of safety-critical systems. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 213–225. Springer, Cham (2016). doi:10.1007/978-3-319-45477-1_17

    Chapter  Google Scholar 

  34. Young, W., Leveson, N.G.: An integrated approach to safety and security based on systems theory. Commun. ACM 57(2), 31–35 (2014)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Åbo Akademi University, Turku, Finland

    Inna Vistbakka & Elena Troubitsyna

  2. Space Systems Finland, Espoo, Finland

    Tuomas Kuismin & Timo Latvala

Authors
  1. Inna Vistbakka
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elena Troubitsyna
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tuomas Kuismin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Timo Latvala
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Inna Vistbakka .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle-upon-Tyne, United Kingdom

    Alexander Romanovsky

  2. Åbo Akademi University, Turku, Finland

    Elena A. Troubitsyna

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Vistbakka, I., Troubitsyna, E., Kuismin, T., Latvala, T. (2017). Co-engineering Safety and Security in Industrial Control Systems: A Formal Outlook. In: Romanovsky, A., Troubitsyna, E. (eds) Software Engineering for Resilient Systems. SERENE 2017. Lecture Notes in Computer Science(), vol 10479. Springer, Cham. https://doi.org/10.1007/978-3-319-65948-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65948-0_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65947-3

  • Online ISBN: 978-3-319-65948-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation