Ранее мы разбирали задачу формализации и верификации модели мандатного контроля целостности, реализованного в KasperskyOS. А сегодня читайте обзор статьи наших коллег Владимира Буренкова и Дмитрия Кулагина “Модель мандатного контроля целостности в операционной системе KasperskyOS”.

Один из ключевых показателей кибериммунных систем - размер и сложность доверенной кодовой базы (ДКБ). Естественно, операционная система в большинстве случаев входит в ДКБ, поэтому использование микроядерных операционных систем позволяет при одинаковых затратах на безопасную разработку тщательнее верифицировать такое решение, уменьшить поверхность защиты и снизить эксплуатационные затраты за счёт меньшего количества критических уязвимостей, которые необходимо срочно исправлять.

KasperskyOS является микроядерной операционной системой, в ней реализован мандатный контроль доступа, для которой сформулирована и доказана теорема о постоянном нахождении модели в целостном состоянии. Корректная реализация модели гарантирует, что если компрометирована часть системы, уровень целостности компонентов которой ограничен некоторыми уровнями целостности, то это не приведет к компрометации части системы с более высокими или несравнимыми уровнями целостности.

В статье описывается архитектура операционной системы KasperskyOS, особенности реализации декларации интерфейсов, контроля взаимодействия процессов, контроля доступа к ресурсам, особенности реализации модели мандатного контроля целостности, язык описания политик безопасности.

Рекомендуем к изучению всем, кто интересуется кибериммунной разработкой и хочет досконально разобраться в ключевых аспектах работы KasperskyOS, понять математический аппарат, стоящий за мандатным контролем доступа, реализованным в нашей операционной системе.

💾 ССЫЛКА НА СКАЧИВАНИЕ