Условия безопасности информационных потоков по памяти в рамках МРОСЛ ДП-модели | ПДМ. 2014. № 7 (Приложение).

Условия безопасности информационных потоков по памяти в рамках МРОСЛ ДП-модели

В рамках мандатной сущностно-ролевой ДП-модели, ориентированной на реализацию в отечественной защищённой операционной системе специального назначения Astra Linux Special Edition, анализируются условия безопасности информационных потоков по памяти в смысле Белла - ЛаПадулы и мандатного контроля целостности.

Security conditions for information flows by memory within the mrosl DP-model.pdf Фундаментальным требованием безопасности операционных систем, реализующих мандатное управление доступом, является предотвращение возможности реализации информационных потоков по памяти «сверху вниз» (безопасность в смысле Белла - ЛаПадулы [1]). Кроме того, современную защищённую операционную систему трудно представить без мандатного контроля целостности, основой которой является предотвращение возможности модификации (через создание соответствующих информационных потоков по памяти) сущностей с высоким уровнем целостности субъект-сессиями с низким уровнем целостности. Таким образом, важным этапом при разработке мандатной сущностно-ролевой ДП-модели (МРОСЛ ДП-модели) [1-3], реализуемой в настоящее время в отечественной защищенной операционной системе специального назначения (ОССН) Astra Linus Special Edition [4], стало формулирование и обоснование достаточных условий безопасности в смысле Белла - ЛаПадулы и мандатного контроля целостности. Дополнительно к использованным в перечисленных работах дадим следующие определения и обозначения. Определение 1. Доверенную субъект-сессию у назовем функционально корректной относительно доверенной субъект-сессии у' и сущности или субъект-сессии e, когда у не реализует информационный поток по памяти от e к некоторой сущности e', функционально ассоциированной с у'. Субъект-сессию у назовем абсолютно функционально корректной относительно субъект-сессии y' и сущности или субъект-сессии e, когда у не реализует информационный поток по памяти от e к некоторой сущности e', функционально ассоциированной с у'. При этом используем следующие обозначения: - f _correct : ^ 2LsX(EuS) -функция, задающая для каждой доверенной субъект-сессии множество пар вида (доверенная субъект-сессия, сущность или субъект-сессия), относительно которых она функционально корректна; - af _correct : S ^ 2Sx(EuS) -функция, задающая для каждой субъект-сессии множество пар вида (субъект-сессия, сущность или субъект-сессия), относительно которых она абсолютно функционально корректна. Определение 2. Доверенную субъект-сессию у назовем параметрически корректной относительно доверенной субъект-сессии у' и сущности или субъект-сессии e, когда у не реализует информационный поток по памяти от или к e от или к некоторой сущности e', параметрически ассоциированной с у'. Субъект-сессию у назовем абсолютно параметрически корректной относительно субъект-сессии у' и сущности или субъект-сессии e, когда у не реализует информационный поток по памяти от или к e от или к некоторой сущности e', параметрически ассоциированной с у'. При этом используем следующие обозначения: - p_correct : ^ 2LsX(EuS) -функция, задающая для каждой доверенной субъект-сессии множество пар вида (доверенная субъект-сессия, сущность или субъект-сессия), относительно которых она параметрически корректна; - ap_correct : S ^ 2Sx(EuS) -функция, задающая для каждой субъект-сессии множество пар вида (субъект-сессия, сущность или субъект-сессия), относительно которых она абсолютно параметрически корректна. Определение 3. Назовём траекторию Go ^opx Gi ^op2 ... ^opn Gn системы E(G*, OP, G0), где N ^ 0, на которой доверенные субъект-сессии не инициируют выполнение де-юре правил преобразования состояний, траекторией без кооперации доверенных и недоверенных субъект-сессий. Таким образом, по определению в системе S(G*, OP, G0) на траекториях без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа доверенные субъект-сессии могут инициировать выполнение только де-факто правил вида f/ow_memory_access(x, у, аа), f/ow_time_access(x, у), fin^x^z), pos^x^z) и pas^x^z). Определение 4. Состояние G системы E(G*, OP, G0) назовём безопасным, когда оно удовлетворяет следующим условиям: - для каждых субъект-сессий x, y G S, таких, что y G de_/acto_own(x), выполняется ЛЫ = fs(x) и is(y) ^ is(x); - для каждых недоверенной субъект-сессии x G Ns , субъект-сессии y G S и сущности e G E, таких, что либо (e G [y] и (x,e,writem) G F), либо (e G]y[ и либо (e,x,writem) G F, либо (x,e,reada) G A), верны условия /s(y) ^ /s(x) и is(y) ^ is(x); - для каждой доверенной субъект-сессии y G Ls и каждой сущности c_i_entity G G E_HOLE, где c G LC, верно условие (y, c_i_entity, writea) G A; - для каждого информационного потока (x,y,af) G F, где a/ G {writem, writet}, справедливо /x(x) ^ / (y), где /ж и /у соответствующие функции fe, /г или и, если a/ = writem, то справедливо ix(x) ^ iy(y), где ix и iy - соответствующие функции ie или is. Определение 5. Пусть G0 - безопасное начальное состояние системы E(G*, OP, G0) и существует траектория без кооперации доверенных и недоверенных субъект-сессий G0 hopi G1 hop2 ... hopN Gn, где N ^ 1. Будем говорить, что в состоянии GN произошло нарушение безопасности системы, когда в нём выполняется одно из следующих условий, при этом они не выполняются в состояниях Gj траектории, где 0 ^ i < N: - существуют недоверенная субъект-сессия x G Nsn и доверенная субъект-сессия y G de_/acto_ownN(x) П LSn , такие, что iSN (y) = i_high (нарушение безопасности в смысле мандатного контроля целостности); - существует информационный поток по памяти (x,y,writem) G Fn, такой, что x, y G En и не верно неравенство /eN (x) ^ /eN (y) (нарушение безопасности в смысле Белла - ЛаПадулы); - существует информационный поток по времени (x, y, writet) G Fn, такой, что x, y G G En и не верно неравенство /eN (x) ^ /eN (y) (нарушение безопасности в смысле контроля информационных потоков по времени). В следующей базовой теореме безопасности (БТБ-ДП) сформулированы достаточные условия безопасности системы, заданной в рамках МРОСЛ ДП-модели, в смыслах Белла - ЛаПадулы и мандатного контроля целостности. При этом анализ условий безопасности информационных потоков по времени как существенно более сложный планируется осуществить при проведении дальнейших исследований. Теорема 1. Пусть G0 - безопасное начальное состояние системы E(G*,OP, G0). Пусть на всех траекториях системы без кооперации доверенных или недоверенных субъект-сессий G0 hopi G1 hop2 ... hopN GN, где N ^ 0, и в каждом состоянии GN для каждой субъект-сессии s G Sn и сущности e G En выполняются следующие условия: - если e G [s], то выполняются условия isN (s) ^ ieN (e) и (/sN (s) = /eN (e) или ieN (e) = i_high) (корректность уровней конфиденциальности и целостности сущностей, функционально ассоциированных с субъект-сессиями); - если e g] s [, то выполняется равенство /sN (s) = /eN (e) и для каждой роли или административной роли r G Rn U ARn, такой, что (e,readr) G PAn(r), выполняются условия isN (s) ^ ieN (e) ^ irN (r) (корректность уровней конфиденциальности и целостности, а также прав доступа на чтение к сущностям, параметрически ассоциированным с субъект-сессиями); - для всех доверенных субъект-сессий s G LSn верны равенства /_correctN(s) = = p_correctN (s) = LSn x (En U Sn) (функциональная и параметрическая корректность всех доверенных субъект-сессий относительно всех доверенных субъект-сессий и сущностей); - для всех субъект-сессий s Е SN выполняются равенства {s' Е SN : fSN (s') = = fSN(s)}x(EN U SN) С af_correctN(s) = ap_correctN(s) (абсолютная функциональная и параметрическая корректность субъект-сессии относительно всех сущностей и субъект-сессий с совпадающим уровнем конфиденциальности). Тогда система E(G*, OP, Go) безопасна в смыслах Белла - ЛаПадулы и мандатного контроля целостности. Условия теоремы БТБ-ДП требуют от ОССН функционально и параметрически корректной (абсолютно корректной) реализации всех субъект-сессий и корректного задания соответствующих уровней конфиденциальности и целостности функционально или параметрически ассоциированных с ними сущностей. Если, например, субъект-сессия, имеющая высокий уровень доступа, некорректно обрабатывает данные («заражается») в сущностях с низким уровнем конфиденциальности и это приводит к получению фактического владения над нею субъект-сессией с низким уровнем доступа, то система защиты ОССН не сможет этому воспрепятствовать. Таким образом, условия теоремы БТБ-ДП указывают на необходимость повышения качества разработки прикладного программного обеспечения ОССН.

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

access control, information flow, formal model, computer security, Linux, информационный поток, формальная модель, компьютерная безопасность

Авторы

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

Ссылки

Операционные системы Astra Linux. http://www.astra-linux.ru/.
Девянин П. Н. Администрирование системы в рамках мандатной сущностно-ролевой ДП-модели управления доступом и информационными потоками в ОС семейства Linux // Прикладная дискретная математика. 2013. №4(22). С. 22-40.
Девянин П. Н. Адаптация мандатной сущностно-ролевой ДП-модели к условиям функционирования ОС семейства Linux // Системы высокой доступности. 2013. №3. С. 98-102.
Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 2-е изд., испр. и доп. М.: Горячая линия - Телеком, 2013. 338 с.
 Условия безопасности информационных потоков по памяти в рамках МРОСЛ ДП-модели | ПДМ. 2014. № 7 (Приложение).

Условия безопасности информационных потоков по памяти в рамках МРОСЛ ДП-модели | ПДМ. 2014. № 7 (Приложение).