Using Refinement in Formal Development of OS Security Model

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.