Abstract
The paper presents work in progress on formal development of an operating system security model for the purpose of its deductive verification. We consider two approaches to formalize the security model. The first one is to build a monolithic model, another one is to build a hierarchical model using the refinement technique. The main criteria for comparison are costs of development, simplicity of maintenance and confidence in the quality of the formal model. The results are twofold. On the one hand, refinement helped us to deal with complexity of the formal model, to improve its readability and to simplify automatic proofs. However, deep understanding of the security model details and careful planning were absolutely necessary to build a reasonable hierarchical model. The monolithic approach allowed to quickly start formalization and helped to study the details of the security model, but the resulting formal model became hard to maintain and explore.
The research was supported by the Ministry of Education and Science of the Russian Federation (unique project identifier RFMEFI60414X0051).
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.
- 2.
- 3.
These examples are provided with permission of RPA RusBITech.
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamentae Informatica 77(1,2), 1–28 (2007)
Damchoom, K.: An incremental refinement approach to a development of a flash-based file system in Event-B. Ph.D. thesis, University of Southampton, School of Electronics and Computer Science (2010)
Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., Shchepetkov, I.V.: Formal verification of OS security model with alloy and Event-B. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 309–313. Springer, Heidelberg (2014)
Devyanin, P.N.: Security models of computer systems: access control and information flows (in Russian). Hot line - Telecom (2013)
Huynh, N., Frappier, M., Mammar, A., Laleau, R., Desharnais, J.: Validating the RBAC ANSI 2012 standard using B. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 255–270. Springer, Heidelberg (2014)
Wirth, N.: Program development by stepwise refinement. CACM Commun. ACM 14, 221–227 (1971)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 1–39 (2009)
Yeganefard, S., Butler, M., Rezazadeh, A.: Evaluation of a guideline by formal modelling of cruise control system in Event-B. In: NFM 2010, pp. 182–191 (2010)
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
Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., Shchepetkov, I.V. (2016). Using Refinement in Formal Development of OS Security Model. In: Mazzara, M., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science(), vol 9609. Springer, Cham. https://doi.org/10.1007/978-3-319-41579-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-41579-6_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41578-9
Online ISBN: 978-3-319-41579-6
eBook Packages: Computer ScienceComputer Science (R0)