О результатах формирования иерархического представления МРОСЛ ДП-модели | ПДМ. Приложение. 2016. № 9.

О результатах формирования иерархического представления МРОСЛ ДП-модели

«Монолитное» представление мандатной сущностно-ролевой ДП-модели, являющееся основой механизма управления доступом в отечественной защищённой операционной системе специального назначения (ОССН) Astra Linux Special Edition, ввиду своего значительного объёма и сложности стало неудобно как для научного анализа, верификации и дальнейшего развития самой модели, так и для непосредственного применения в ОССН. По этой причине предлагается полностью переработанное иерархическое представление модели, описывающее её по уровням. В текущем таком представлении заданы четыре иерархически упорядоченных уровня, соответствующих: 1) ролевому управлению доступом; 2) мандатному контролю целостности; 3) мандатному управлению доступом с информационными потоками по памяти и 4) по времени. В дальнейшем возможно добавление новых, в том числе «боковых» уровней, например 3') для модели гипервизора.

About results of designing hierarchical representation of mrosl DP-model.pdf Разработанная автором мандатная сущностно-ролевая ДП-модель (МРОСЛ ДП-модель) [1, 2] является частью комплексного научно-обоснованного решения [3] по разработке отечественной защищенной ОССН Astra Linux Special Edition [4, 5]. Для получения гарантий адекватности реализации МРОСЛ ДП-модели в ОССН Институтом системного программирования РАН [6, 7] она была сначала переведена в формализованную нотацию Event-B (Rodin Platform), которая позволила верифицировать описание модели и осуществить дедуктивные доказательства её свойств. Затем на основе формализованного представления модели с использованием инструмента дедуктивной верификации кода Why (в среде разработки Frama-С) были заданы и проверено выполнение спецификаций (предусловий и постусловий) функций механизма управления доступом ОССН, что позволило обосновать адекватность реализации модели в программном коде. В то же время существующее описание МРОСЛ ДП-модели имеет значительный объём и является «монолитным», т. е. в нём элементы модели приводятся в порядке, принятом несколько лет назад в начале формирования модели. Первыми делаются предположения о базовых свойствах задаваемой в рамках модели абстрактной системы, потом даются определения элементов состояний системы, далее описываются требования к реализации в системе мандатного и ролевого управления доступом и мандатного контроля целостности, затем приводятся правила преобразования состояний системы, и в заключение формулируются и обосновываются условия безопасности системы, а также рассматриваются подходы к применению модели в ОССН. В итоге по мере получения новых теоретических результатов и всё большей адаптации модели к условиям функционирования ОССН модель становится всё труднее корректировать, так как каждое изменение в каком-либо её элементе требует учёта во всех других связанных с ним элементах модели, а также проверки справедливости большинства обоснованных в модели утверждений. Кроме того, из-за большого объёма и «монолитности» модели, невозможности в таком виде её поэтапной реализации затрудняется использование модели разработчиками ОССН, а также создание на её основе новых моделей (например, модели гипервизора для ОССН). В связи с этим автором реализуется переход от «монолитного» описания модели к иерархическому, позволяющему представить модель по уровням (слоям). При этом каждый нижний уровень модели представляет абстрактную систему, элементы которой не зависят от новых элементов, принадлежащих более высокому уровню, который, в свою очередь, наследует, а при необходимости корректирует или дополняет элементы нижнего уровня. Таким образом, при иерархическом описании МРОСЛ ДП-модели в настоящее время задаются следующие уровни (рис. 1): - первый уровень - модель системы ролевого управление доступом; - второй уровень - модель системы ролевого управление доступом и мандатного контроля целостности; - третий уровень - модель системы ролевого управление доступом, мандатного контроля целостности и мандатного управления доступом только с информационными потоками по памяти; - четвёртый уровень - модель системы ролевого управление доступом, мандатного контроля целостности и мандатного управления доступом с информационными потоками по памяти и по времени. Рис. 1. Иерархическое представление МРОСЛ ДП-модели и его возможные расширения Этот подход позволяет постепенно усложнять формулировки определений и утверждений модели по мере включения в неё соответствующих очередному рассматриваемому уровню элементов. Например, на третьем уровне (мандатного управления доступом с информационными потоками по памяти) с использованием обозначений из [1] даётся следующая формулировка определения безопасного начального состояния системы. При этом идентификаторы определения и его условий дополнительно показывают последовательность их формирования при переходе от уровня к уровню (Ц - второй уровень, КП - третий уровень). Определение О.Ц.06.КП. Начальное состояние Go системы S(G*,OP,G0) назовём безопасным, если оно удовлетворяет следующим условиям. Условие Ц.1.КП. Для каждых субъект-сессий x,y G S0, таких, что y G de_facto-_own0(x), верно fs0(y) = fs0(x) и is0(y) ^ is0(x) (по сравнению со вторым уровнем добавляется требование равенства текущих уровней доступа субъект-сессий x и y, одна из которых де-факто владеет другой). Условие Ц.2.КП. Для каждых недоверенной субъект-сессии x Е Ns0 , субъект-сессии у Е S0 и сущности e Е E0, таких, что либо (e Е [у] и (x,e,writem) Е F0), либо (e Е]у[ и либо (e,x,writem) Е F0, либо (x,e,read„) Е A0), верно fso(у) ^ fso(x) и iso(у) ^ iso(x) (по сравнению со вторым уровнем добавляется требование, чтобы текущий уровень доступа к сущностям, параметрически или функционально ассоциированным с сущностью у, недоверенной субъект-сессии x был не ниже текущего уровня доступа этой субъект-сессии у и субъект-сессия x либо имела информационные потоки по памяти, либо обладала доступом на чтение). Условие Ц.3. (На третьем уровне в это условие не дополняется новых требований.) Условие Ц.4.КП. Для каждого информационного потока (x^writem) Е F0 справедливо fxo(x) ^ fyo(у), где fxo и fyo - соответствующие функции feo или fso, и справедливо ixo (x) ^ iyo (у), где ixo и iyo - соответствующие функции ieo или iso (по сравнению со вторым уровнем добавляется требование, чтобы при наличии информационного потока по памяти уровень конфиденциальности источника x был не выше уровня конфиденциальности приемника у). Условие КП.5. Для доверенных субъект-сессий x^ ^ LSo, таких, что у Е de_facto_own0(x), (у, downgrade_admin_ro/e, reada) Е AA0, верно (x,down-grade_admin_ro/e, reada) Е AA0 (новое условие, добавленное на третьем уровне, заключающееся в запрете получения через де-факто владение специальной административной роли downgrade_admin_ro/e, позволяющей нарушать правила мандатного управления доступом). Аналогично задаются 34 де-юре и 10 де-факто правил преобразования состояний, когда на каждом очередном уровне добавляются, корректируются или остаются без изменений условия и результаты их применения. При таком иерархическом описании модель гипервизора для ОССН (рис. 1) рассматривается как альтернативный (дополнительный) третий уровень (модель системы ролевого управления доступом, мандатного контроля целостности и гипервизо-ра), так как можно предположить, что гипервизор для ОССН должен обеспечивать корректность функционирования её мандатного контроля целостности, а мандатное управление доступом в ОССН не должно реализовываться средствами гипервизора. Аналогично модель ролевого управления доступом в компьютерной сети целесообразно считать альтернативной четвёртому уровню представления МРОСЛ ДП-модели, так как в этой модели существенным является мандатный контроль целостности и мандатное управление доступом только с информационными потоками по памяти. Таким образом, переход от «монолитного» к иерархическому представлению МРОСЛ ДП-модели за счёт более ясного, структурированного её изложения способствует развитию самой модели, улучшению результатов её верификации при переводе модели в формализованную нотацию Event-B, а также позволяет повысить качество реализации модели непосредственно в ОССН.

Ключевые слова

компьютерная безопасность, формальная модель, иерархическое представление, Linux, computer security, formal model, hierarchical description, Linux

Авторы

ФИООрганизацияДополнительноE-mail
Девянин Петр НиколаевичУМС ФУМО ВО ИБдоктор технических наук, доцент, председательpeter_devyanin@hotmail.com
Всего: 1

Ссылки

Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 2-е изд., испр. и доп. М.: Горячая линия - Телеком, 2013. 338 с.
Девянин П. Н. Необходимые условия нарушения безопасности информационных потоков по времени в рамках МРОСЛ ДП-модели // Прикладная дискретная математика. Приложение. 2015. №8. С. 81-83.
Девянин П. Н., Куликов Г. В., Хорошилов А. В. Комплексное научно-обоснованное решение по разработке отечественной защищенной ОССН Astra Linux Special Edition // Методы и технические средства обеспечения безопасности информации: Материалы 23-й науч.-технич. конф. 30 июня-03 июля 2014г. СПб.: Изд-во Политехи. ун-та, 2014. С.29-33.
Операционные системы Astra Linux. http://www. astra-linux.ru/
Astra Linux. https://ru.wikipedia.org/wiki/AstraX_Linux
Девянин П. Н., Кулямин В. В., Петренко А. К. и др. О представлении МРОСЛ ДП-модели в формализованной нотации Event-B // Проблемы информационной безопасности. Компьютерные системы. 2014. №3. С. 7-15.
Devyanin P., Khoroshilov A, Kuliamin V., et al. Formal verification of OS security model with Alloy and Event-B // LNCS. 2014. V.8477. P. 309-313.
 О результатах формирования иерархического представления МРОСЛ ДП-модели | ПДМ. Приложение. 2016. № 9.

О результатах формирования иерархического представления МРОСЛ ДП-модели | ПДМ. Приложение. 2016. № 9.