Формальная верификация модели мандатного контроля целостности в операционной системе KasperskyOS

Модели мандатного контроля целостности в операционных системах, как правило, накладывают ограничения на доступы активных компонент системы к пассивным и представляют эти доступы непосредственно. Такое представление можно использовать в случае операционных систем с монолитной архитектурой, где части системы, обеспечивающие доступ к ресурсам, входят в доверенную вычислительную базу. Однако доказательство отсутствия ошибок в таких компонентах и, следовательно, соответствия такой модели реальной системе является чрезвычайно трудной задачей. KasperskyOS – операционная система, основанная на микроядре и позволяющая организовать доступ к ресурсам с помощью компонентов, не обязательно входящих в доверенную вычислительную базу. Для KasperskyOS была разработана и реализована модель мандатного контроля целостности, учитывающая наличие таких компонентов и возможность их некорректного функционирования. В данной статье представлен процесс формализации этой модели и автоматизированного доказательства свойств, обеспечиваемых моделью. Описана разработка модели на языке Event-B и отражен опыт ее верификации с использованием платформы Rodin.