Using Refinement in Formal Development of OS Security Model.
Using Refinement in Formal Development of OS Security Model.
Авторы
Аннотация
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.
Полный текст статьи в формате pdf (на английском)Издание
Proceedings of PSI 2015.
Научная группа
Все публикации за 2015 год
Все публикации