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

Существующие модели мандатного контроля целостности в операционных системах накладывают ограничения на доступы активных компонент системы к пассивным и представляют эти доступы непосредственно. Такое представление можно использовать в случае операционных систем с монолитной архитектурой, где части системы, обеспечивающие доступ к ресурсам, входят в доверенную вычислительную базу. Однако эти части являются нетривиальными компонентами со сложной реализацией, в связи с чем доказательство отсутствия в них ошибок (уязвимостей) и, следовательно, соответствия модели реальной системе - чрезвычайно трудная задача, которая на практике, как правило, полностью не решается. В данной статье представлена модель мандатного контроля целостности для микроядерной операционной системы KasperskyOS. Базирование системы на микроядре предполагает минимизацию доверенной вычислительной базы. При таком подходе доступ к ресурсам предоставляется с помощью компонент, не входящих в доверенную вычислительную базу. Это создает предпосылки для гарантии соответствия системы определенным свойствам безопасности даже в случае некорректного функционирования этих компонент. В модели для представления частей системы, обеспечивающих доступ к ресурсам, введено понятие драйвера объектов, и операции получения доступа активных компонент (сущностей) к пассивным компонентам (объектам) выполняются посредством драйверов объектов. В статье определены требования, которым должны удовлетворять драйверы объектов и некоторые другие сущности. В модель также добавлены элементы, позволяющие провести ее анализ в случае нарушения данных требований. Сформулирована и доказана теорема о постоянном нахождении модели в целостном состоянии (об отсутствии в модели информационных потоков от менее целостных компонентов к более целостным либо несравнимым) в случае удовлетворения всеми сущностями сформулированных требований, а также об ограниченном характере распространения эффекта от нарушения целостности системы в случае наличия в системе компонентов, нарушающих требования. Корректная реализация модели гарантирует, что если компрометирована часть системы, уровень целостности компонентов которой ограничен некоторыми уровнями целостности, то это не приведет к компрометации части системы с более высокими или несравнимыми уровнями целостности. Описан язык спецификации политик мандатного контроля целостности, разработанный в соответствии с правилами модели, и приведен пример использования языка для задания политики безопасности системы, работающей под управлением KasperskyOS. Целью политики является обеспечение безопасности процесса обновления системы.