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.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abrial, J.R.: Modeling in Event-B. Cambridge University Press, New York (2010)
Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds.): Rigorous Development of Complex Fault-Tolerant Systems. LNCS, vol. 4157. Springer, Heidelberg (2006)
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
Fovino, I.N., Masera, M., Cian, A.D.: Integrating cyber attacks within fault trees. Rel. Eng. Sys. Safety 94(9), 1394–1402 (2009)
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
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)
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
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)
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
Sere, K., Troubitsyna, E.A.: Probabilities in action systems. In: Proceedings of the 8th Nordic Workshop on Programming Theory, pp. 373–387 (1996)
Kelly, T.P., Weaver, R.A.: The goal structuring notation - a safety argument notation. In: DSN 2004, Workshop on Assurance Cases (2004)
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
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)
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
Laibinis, L., Troubitsyna, E.: Fault tolerance in use-case modeling. In: Proceedings of RHAS 2005 (2005)
Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Boston (1995)
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)
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)
Paul, S., Rioux, L.: Over 20 years of research into cybersecurity and safety engineering: a short bibliography. Saf. Secur. Eng. VI 151, 335 (2015)
Pereverzeva, I., Troubitsyna, E., Laibinis, L.: Formal development of critical multi-agent systems: a refinement approach. In: EDCC 2012, pp. 156–161 (2012)
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
Prokhorova, Y., Laibinis, L., Troubitsyna, E.: Facilitating construction of safety cases from formal models in Event-B. Inform. Softw. Technol. 60, 51–76 (2015)
Rodin: Event-B platform. http://www.event-b.org/
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
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
Sere, K., Troubitsyna, E.: Hazard analysis in formal specification. In: Proceedings of the 18th International Conference, SAFECOMP 1999, pp. 350–360 (1999)
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
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
Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Integrating stochastic reasoning into Event-B development. Formal Asp. Comput. 27(1), 53–77 (2015)
Troubitsyna, E.: Enhancing dependability via parameterized refinement. In: PRDC 1999, Hong Kong, p. 120. IEEE Computer Society (1999)
Troubitsyna, E.: Stepwise Development of Dependable Systems. Technical report (2000)
Troubitsyna, E.: Elicitation and specification of safety requirements. In: ICONS 2008, Cancun, Mexico, pp. 202–207. IEEE Computer Society (2008)
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
Young, W., Leveson, N.G.: An integrated approach to safety and security based on systems theory. Commun. ACM 57(2), 31–35 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)