Корректность правил преобразования состояний системы в рамках мандатной сущностно-ролевой ДП-модели оС семейства Linux

УДК 004.94

КОРРЕКТНОСТЬ ПРАВИЛ ПРЕОБРАЗОВАНИЯ СОСТОЯНИЙ СИСТЕМЫ В РАМКАХ МАНДАТНОЙ СУЩНОСТНО-РОЛЕВОЙ ДП-МОДЕЛИ ОС СЕМЕЙСТВА LINUX

П. Н. Девянин

Рассматриваются де-юре и де-факто правила преобразования состояний системы мандатной сущностно-ролевой ДП-модели управления доступом и информационными потоками в операционных системах (ОС) семейства Linux и формулируется утверждение об их корректности относительно заданных в рамках модели требований к реализации мандатного контроля целостности, мандатного и ролевого управления доступом.

Ключевые слова: компьютерная безопасность, формальная модель, управление доступом.

Для строгого формального обоснования безопасности защищённой операционной системы Astra Linux Special Edition [1] автором разрабатывается мандатная сущностно-ролевая ДП-модель управления доступом и информационными потоками в ОС семейства Linux [2, 3] (МРОСЛ ДП-модель). В рамках модели описываются требования к реализации механизмов мандатного контроля целостности, мандатного и ролевого управления доступом, в том числе:

— для уровней доступа и целостности учётной записи пользователя;

— для текущих уровней доступа и целостности субъект-сессии;

— для уровней конфиденциальности и целостности сущности, входящей в состав сущности-контейнера;

— для уровней конфиденциальности и целостности роли или административной роли;

— для уровней конфиденциальности и целостности сущностей, параметрически ассоциированных с учётной записью пользователя, ролью или административной ролью;

— для доступов субъект-сессии к сущности с учётом атрибутов конфиденциальности и целостности сущностей-контейнеров CCR и CCRI, для создания, удаления сущности или «жёсткой» ссылки на сущность, для сущностей-«дырок», в которых данные «не сохраняются», для доступов субъект-сессии на владение к субъект-сессии, на активизацию из сущности субъект-сессии;

— для специальных сущностей, используемых для получения доступа к сущностям с высоким уровнем целостности;

— для доступов субъект-сессии к роли или административной роли;

— для индивидуальных ролей и административных ролей учётной записи пользователя;

— для изменения атрибутов CCR, CCRI, переименования роли, административной роли или сущности-контейнера;

— для получения субъект-сессией данных о числе «жёстких» ссылок к сущности;

— для предоставления имён сущностей, ролей или административных ролей;

— для возможности нарушения отдельных условий мандатного управления доступом (при администрировании защищённой ОС).

После этого задаются 20 де-юре и 10 де-факто правил преобразования состояний системы, для каждого из которых детально описываются условия и результаты применения. В таблице приведены примеры задания де-юре правила grant_rights(x, X,

г, {(у, аГ]): 1 ^ і ^ к}), позволяющего субъект-сессии х при кооперации с субъект-сессией х' дать роли г права доступа к сущности у, и де-факто правила соиЬго1(х, у, г), при реализации которого субъект-сессия х получает фактическое владение субъект-сессией у, используя сущность г, функционально ассоциированную с у.

Примеры задания правил преобразования состояний

Правило Исходное состояние G =

grant rights

control(x, y, z) x € Ns П S, y € S, x = y, z € [y] и или x = z, или (x, z,writem) € F, или [z € S и z € de facto own(x)] S' = S, E' = E, PA' = PA, A' = A, AA' = AA, user' = user, H'e = He , de facto own'(x) = = de facto own(x) U {y}, F' = = FU{(x, y, writet), (y, x, writet)}

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

Утверждение 1. Пусть Go — состояние системы Tj(G*,OP), удовлетворяющее требованиям к реализации мандатного контроля целостности, мандатного и ролевого управления доступом. Тогда для любой траектории Go —opi G1 -op2 ... -opN Gn, где N ^ 1, эти требования выполняются в состоянии Gn и при переходе Gn-1 -0pN Gn .

Таким образом, обеспечивается основа для дальнейшего теоретического исследования и обоснования в рамках МРОСЛ ДП-модели свойств рассматриваемых защищённых ОС семейства Linux.

ЛИТЕРАТУРА

1. Операционные системы Astra Linux jj http://www.astra-linux.ru/.

2. Девянин П. Н. О разработке мандатной сущностно-ролевой ДП-модели управления доступом и информационными потоками в операционных системах семейства Linux jj Методы и технические средства обеспечения безопасности информации: Материалы 21-й науч.-технич. конф. 24-29 июня 2012 г. СПб.: Изд-во Политехн. ун-та, 2012. С. 91-94.

3. Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 2-е изд., испр. и доп. М.: Горячая линия-Телеком, 2013. 338 с.