Abstract
Modern industrial control systems become increasingly interconnected and rely on external networks to provide their services. Hence they become vulnerable to security attacks that might directly jeopardise their safety. The growing understanding that if the system is not secure then it is not safe calls for novel development and verification techniques weaving security consideration into the safety-driven design. In this paper, we demonstrate how to make explicit the relationships between safety and security in the formal system development by refinement. The proposed approach allows the designers to identify at early design states mutual interdependencies between the mechanisms ensuring safety and security and build robust system architecture.
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
Notes
- 1.
Due to a lack of space we present a simple model of communication. A more elaborated model similar to [5] can also be used.
References
Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)
Brunel, J., Rioux, L., Paul, S., Faucogney, A., Vallée, F.: Formal safety and security assessment of an avionic architecture with alloy. In: ESSS 2014, EPTCS, vol. 150, pp. 8–19 (2014)
Cimatti, A., DeLong, R., Marcantonio, D., Tonetta, S.: Combining MILS with contract-based design for safety and security requirements. In: Koornnee, F., van Gulijk, C. (eds.) SAFECOMP 2015 Workshops. LNCS, vol. 9338, pp. 264–276. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24249-1_23
Fovino, I.N., Masera, M., Cian, A.D.: Integrating cyber attacks within fault trees. Reliab. Eng. Syst. Safety 94(9), 1394–1402 (2009)
Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A.: Formal derivation of a distributed program in Event B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 420–436. Springer, Heidelberg (2011)
Kelly, T.P.: Arguing safety - a systematic approach to managing safety cases. Ph.D. thesis (1998)
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, Heidelberg (2014)
Rodin: Event-B platform. http://www.event-b.org/
Schmittner, C., Gruber, T., Puschner, P., Schoitsch, E.: Security application of failure mode and effect analysis (FMEA). In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 310–325. Springer, Heidelberg (2014)
Young, W., Leveson, N.G.: An integrated approach to safety and security based on systems theory. Commun. ACM 57(2), 31–35 (2014)
Acknowledgements
This work is partially funded by the TEKES project Cyber Trust.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Troubitsyna, E., Laibinis, L., Pereverzeva, I., Kuismin, T., Ilic, D., Latvala, T. (2016). Towards Security-Explicit Formal Modelling of Safety-Critical Systems. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2016. Lecture Notes in Computer Science(), vol 9922. Springer, Cham. https://doi.org/10.1007/978-3-319-45477-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-45477-1_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-45476-4
Online ISBN: 978-3-319-45477-1
eBook Packages: Computer ScienceComputer Science (R0)