Using Refinement in Formal Development of OS Security Model

Autor:	Alexey Khoroshilov, Alexander K. Petrenko, Ilya V. Shchepetkov, Victor V. Kuliamin, Petr N. Devyanin
Rok vydání:	2016
Předmět:	business.industry Computer science media_common.quotation_subject Work in process Computer security model Mathematical proof Hierarchical database model Development (topology) Quality (business) Simplicity Software engineering business Formal verification media_common
Zdroj:	Lecture Notes in Computer Science ISBN: 9783319415789 Ershov Memorial Conference
DOI:	10.1007/978-3-319-41579-6_9
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::029c20d9f49fa6aeb026218fd6cbebd2 https://doi.org/10.1007/978-3-319-41579-6_9 Zobrazit plný text záznamu