Correctness of state transformation rules in MROSL DP-model.pdf Для строгого формального обоснования безопасности защищённой операционной системы Astra Linux Special Edition [1] автором разрабатывается мандатная сущност-но-ролевая ДП-модель управления доступом и информационными потоками в ОС семейства Linux [2, 3] (МРОСЛ ДП-модель). В рамках модели описываются требования к реализации механизмов мандатного контроля целостности, мандатного и ролевого управления доступом, в том числе: — для уровней доступа и целостности учётной записи пользователя; — для текущих уровней доступа и целостности субъект-сессии; — для уровней конфиденциальности и целостности сущности, входящей в состав сущности-контейнера; — для уровней конфиденциальности и целостности роли или административной роли; — для уровней конфиденциальности и целостности сущностей, параметрически ассоциированных с учётной записью пользователя, ролью или административной ролью; — для доступов субъект-сессии к сущности с учётом атрибутов конфиденциальности и целостности сущностей-контейнеров CCR и CCRI, для создания, удаления сущности или «жёсткой» ссылки на сущность, для сущностей-«дырок», в которых данные «не сохраняются», для доступов субъект-сессии на владение к субъект-сессии, на активизацию из сущности субъект-сессии; — для специальных сущностей, используемых для получения доступа к сущностям с высоким уровнем целостности; — для доступов субъект-сессии к роли или административной роли; — для индивидуальных ролей и административных ролей учётной записи пользователя; — для изменения атрибутов CCR, CCRI, переименования роли, административной роли или сущности-контейнера; — для получения субъект-сессией данных о числе «жёстких» ссылок к сущности; — для предоставления имён сущностей, ролей или административных ролей; — для возможности нарушения отдельных условий мандатного управления доступом (при администрировании защищённой ОС). После этого задаются 20 де-юре и 10 де-факто правил преобразования состояний системы, для каждого из которых детально описываются условия и результаты применения. В таблице приведены примеры задания де-юре правила grant_rights(x, x', r, {(y, arj): 1 ^ j ^ k}), позволяющего субъект-сессии x при кооперации с субъект-сессией x' дать роли r права доступа к сущности y, и де-факто правила control (x, y, z), при реализации которого субъект-сессия x получает фактическое владение субъект-сессией y, используя сущность z, функционально ассоциированную с y. Примеры задания правил преобразования состояний Правило Исходное состояние G = (PA, user, A, AA, F, HE) Результирующее состояние G' = (PA', user', A', AA', F', HE) grant rights(x, x', r, {(y, arj): 1 < j < k}) x,x' £ S, y £ E, r £ R u AR, (x, r, writea) £ AA, Constraintpa(PA') = true, (x,y,owna) £ A, [если y £ S, то arj = ownr и is(y) ^ ir(r)], [если y £ E \ S и arj £ £ {ownr,writer}, то ie(y) ^ ir(r)], [если (y £ S и is(y) = i high) или (y £ E \ S и ie(y) = i high), то (x',fs(x) i entity, writea) £ A], где 1 ^ j ^ k S' = S, E' = E, A' = A, AA' = = AA, user' = user, HE = He, F' = F, PA'(r) = PA(r) u u{(y, arj) : 1 < j < k} и для r' £ R \ {r} выполняется равенство PA'(r') = PA(r') 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. Пусть G0 — состояние системы T.(G*,OP), удовлетворяющее требованиям к реализации мандатного контроля целостности, мандатного и ролевого управления доступом. Тогда для любой траектории G0 \opi Gi \ор2 ... \opN GN, где N ^ 1, эти требования выполняются в состоянии Gn и при переходе Gn-i \oPN Gn . Таким образом, обеспечивается основа для дальнейшего теоретического исследования и обоснования в рамках МРОСЛ ДП-модели свойств рассматриваемых защищён-ных ОС семейства Linux.

Скачать электронную версию публикации