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, а также позволяет повысить качество реализации модели непосредственно в ОССН.

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