Ivannikov Institute for System Programming of the RAS


Using Refinement in Formal Development of OS Security Model.

Authors

P. N. Devyanin, A. V. Khoroshilov, V. V. Kuliamin, A. K. Petrenko, and I. V. Shchepetkov.

Abstract

The paper presents work in progress on formal development of an operating system security model. The main goal is to measure our confidence in the quality of the model. Additional goal is to simplify its maintenance. We formalized and verified the model using formal method Event-B in two ways - with and without use of the refinement technique - in order to compare them and figure out what approach meets our goals better. Refinement is technique that helped us deal with complexity of the model, improve readability and simplify automatic proofs. However, deep understanding of the security model details and careful planning were absolutely necessary to achieve this. The approach without use of the refinement technique 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.

Full text of the paper in pdf

Keywords

security model; formal veri cation; re nement; Event-B.

Edition

Proceedings of PSI 2015.

Research Group

Software Engineering

All publications during 2015 All publications