Библиография
Аннотация
В работе подробно рассматривается, как в операционных системах на базе MILS можно проверять механизмы мандатного контроля целостности, чтобы гарантировать корректное поведение. На примере KasperskyOS работа продолжает и развивает ранее представленную модель мандатного контроля целостности, разработанную с учётом микроядерной архитектуры системы и использования непривилегированных компонентов для управления доступом к ресурсам. Если в предыдущей статье модель была введена и описана на математическом и естественном языках, то в данной работе основной акцент сделан на ее строгой формализации и доказательстве корректности заявленных свойств безопасности.
Эта модель формализуется на языке Event-B как математическая конструкция с четкой структурой состояний, переходов и инвариантов. Отдельная часть работы посвящена автоматизированной верификации модели на платформе Rodin: демонстрируется, какие свойства безопасности удалось доказать, насколько глубоко автоматизация помогает в анализе и какие ограничения остаются. Показано, что формальный подход позволяет выявить несогласованности в исходном описании модели и повысить ее надежность ещё до внедрения механизмов в реальную ОС.
Исследование адресовано специалистам по операционным системам, разработчикам защитных механизмов, экспертам по формальным методам и инженерам, которые создают или анализируют архитектуры повышенной надежности. Оно дает целостное представление о том, как формальная верификация помогает проектировать модели безопасности в операционных системах, и чем KasperskyOS интересна в этом контексте.