Ivannikov Institute for System Programming of the RAS

Using Refinement in Formal Development of OS Security Model.


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


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


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


Proceedings of PSI 2015.

Research Group

Software Engineering

All publications during 2015 All publications