Аннотация доклада.

Традиционно механизм управления доступом рассматривается как основа обеспечения безопасности компьютерных систем, в особенности защищенных операционных систем (ОС) с мандатным управлением доступом. Для научного исследования свойств этого механизма за более чем 40 лет построены десятки теоретических моделей. Однако большинство отечественных разработчиков защищенных ОС используют (как правило, только формально) для реализации механизма управления доступом устаревшие, неадекватные условиям функционирования современных ОС модели (например, классическую модель Белла-ЛаПадулы), что не позволяет повысить доверие к безопасности получаемого решения. В связи с этим может оказаться полезным анализ результатов построения механизма управления доступом в отечественной защищенной ОС Astra Linux Special Edition на основе новой мандатной сущностно-ролевой ДП-модели (сокращенно, МРОСЛ ДП-модели), в которой обеспечивается сочетание мандатного управления доступом, мандатного контроля целостности с перспективным ролевым управлением доступом. В МРОСЛ ДП-модели применен новый подход, когда роли и административные роли представляются как аналоги сущностей-контейнеров, что позволяет задать в ОС иерархию ролей в виде виртуальной файловой системы. Все вносимые в модель элементы рассматриваются, во-первых, с точки зрения их реализации в ОС, во-вторых, с учетом перспектив дальнейшего строгого теоретического обоснования свойств моделируемой ОС (формулирования алгоритмически проверяемых условий безопасности). Кроме того, модель разрабатывается с учетом обеспечения возможности с использованием методик верификации кода программ осуществить вывод и формальное обоснование корректности реализации модели непосредственно в программном коде механизма управления доступом защищенной ОС Astra Linux Special Edition.