Role-based security model of SELinux computer system.pdf В настоящее время наиболее рапространенным методом реализации безопасногоуправления доступом и информационными потоками в операционных системах (ОС)семейства GNU/Linux является применение программного средства SELinux, в свя-зи с чем возникает задача разработки формальной модели его безопасности. В даннойработе решается задача анализа безопасности управления доступом и информацион-ными потоками в компьютерной системе (КС) SELinux, предлагаются ролевая модельбезопасности данной КС, алгоритм проверки возможности получения права доступаи реализации информационного потока, а также метод применения данной модели напрактике для анализа безопасности рассматриваемой КС.Будем использовать основные понятия и обозначения теории ДП-моделей, считая,что моделируемая КС представляется системой, каждое состояние в которой зада-ётся набором объектов, а каждый переход из состояния в состояние осуществляетсяв результате применения одного из правил преобразования состояний. Определим но-вые элементы ДП-модели, необходимые для адекватного анализа безопасности КСSELinux:T - множество типов сущностей;M - множество известных классов сущностей;Rm - множество прав доступа, допустимых для известных классов сущностей;label : E ^ U х R х T - функция, сопоставляющая сущности контекст безопасности(метку);user : E ^ U, role : E ^ R, type : E ^ T - такие функции, что если e G E иlabel(e) = (u,r, t), то user(e) = u, role(e) = r, type(e) = t;class : E ^ M - функция, сопоставляющая каждой сущности известный класс;allow_role : R ^ 2R - функция, сопоставляющая каждой роли множество ролей,которые она может занять;role_types : R ^ 2T - функция, сопоставляющая каждой роли множество типовсубъектов, к которым ей разрешено получать доступ;user_roles : U ^ 2R - функция, сопоставляющая каждому пользователю множе-ство ролей, на которые он может быть авторизован;class_perms : M ^ 2RM -функция, сопоставляющая каждому известному классусущностей набор прав доступа, к нему применимый;Rr = {(c,p) : c G M,p G class_perms(c)} -множество видов прав доступа;P С S х E х (Rr U {ownr}) -множество текущих прав доступа субъектов к сущно-стям;функции fa : U х E ^ 2Е, fp : U х E ^ 2Е, ft : S х E х Rr ^ 2Е, type_rights :T х T ^ 2Rr, role_transition : R х T ^ R, type_transition : T х T х M ^ 2T,login : R х T ^ 2RxT, constrain : Rr х (U х R х T)2 ^ {0,1}, validatetrans :M х (U х R х T)3 ^ {0,1}.Определение 1. Иерархия известных классов сущностей - это заданное на мно-жестве M отношение частичного порядка ^м, такое, чтоVmi,m2 G M (mi m2 ^ class_perms(mi) D class_perms(m2)).Определение 2. Совокупность объектов G = (U, UL, R, E, S, LS, T, F, M, Rm, P,label, allow_role, role_types, user_roles, class_perms, type_rights, role_transition,type_transition, , login, constrain, validatetrans, ) будем называть состояниемсистемы.В модели определены 19 правил преобразования состояний, образующих множе-ство OP.Используем следующие обозначения:.(G*, OP) -система, где G* -множество всех возможных состояний; OP - мно-жество правил преобразования состояний;G hop G' - переход системы из состояния G в состояние G' с использованием пра-вила преобразования состояний op G OP.Предположение 1. В рамках модели КС SELinux на траекториях функциони-рования системы доверенные пользователи не создают новых субъектов, доверенныесубъекты не участвуют в передаче прав доступа, не реализуют информационных пото-ков по времени, не создают субъектов, не используют права доступа владения к другимсубъектам.Предположение 2. В рамках модели КС SELinux на траекториях функциони-рования системы не изменяются множества U, Ul , Ls, R, T, M, Rm, отношение ^м намножестве M, функции allow_role, role_types, user_roles, class_perms, type_rights,role_transition, type_transition, login, предикаты constrain, validatetrans.Ввиду предположения 2 состояние системы будем записывать как G = (S, E, P, F,, class).Определение 3. Система .(G*,OP) с множеством правил преобразования со-стояний OP называется ДП-моделью КС SELinux, если её состояния подчиняютсяопределению 2 и удовлетворяют предположениям 1 и 2.Для формализации возможности получения права доступа и реализации инфор-мационного потока сформулируем определения предикатов безопасности ДП-моделиКС SELinux.Определение 4. Пусть G0 = (S0,E0, P0, F0,HE0,class0) -состояние системы.(G*, OP), в котором существуют пользователь u G U, право доступа ar G Rr и сущ-ность e G E0. Определим предикат can_share(u, e, ar, G0), который будет истинным то-гда и только тогда, когда существуют состояния Gi , . . . , GN = (SN, EN, PN, FN, HEN,classN) и правила преобразования состояний opi ,... , opN, такие, что G0 hopi Gi h^... hopN GN и существует субъект x G SN, такой, что user(x) = u, и (x, e, ar ) G PN, гдеN ^ 0.Определение 5. Пусть G0 = (S0,E0, P0,F0,HE0,class0) -состояние системы.(G*, OP), в котором существуют сущности x, y G E0. Определим предикат can_write_-memory(x, y, G0), который будет истинным тогда и только тогда, когда существуютсостояния Gi , . . . , Gn = (SN, En, PN, Fn, HEN,classN) и правила преобразования со-стояний opi ,... ,opN, такие, что G0 hopi Gi h^ ... hop. GN и (x,y,writem) G FN, гдеN ^ 0.Определение 6. Пусть Go = (So,Eo, Po,F0,HEo,c/asso) -состояние системыE(G*, OP), в котором существуют сущности x, y Е Eo. Определим предикат can_write_-time(x, y, Go), который будет истинным тогда и только тогда, когда существуют состо-яния G1 , . . . , Gn = (Sn, En , PN, Fn , HEN, c/assN) и правила преобразования состоянийop1,..., opN, такие, что Go bop1 G1 bop2 ... bopN GN и (x, y, writet) Е FN, где N ^ 0.Замечание 1. Заметим, что для проверки истинности предикатов can_share(u,e,ar, Go), can_write_mem,ory(x, y, Go) и can_write_time(x, y, Go) в соответствиис определением требуется учесть все траектории функционирования КС, что не осу-ществимо на практике.В связи с замечанием 1 представляется целесообразным сформулировать и обос-новать алгоритмы проверки истинности предикатов can_share, can_write_m,em,ory иcan_write_tim,e. Такие алгоритмы реализуют преобразование начального состоянияКС в его замыкание и позволяют проверить истинность предикатов для всех поль-зователей, сущностей и прав доступа одновременно. В работе вводятся определениязамыканий ДП-модели КС SELinux (time-замыкания и memory-замыкания), предла-гаются и обосновываются алгоритмы их построения.Предлагается также метод применения построенной модели на практике для про-верки возможности получения права доступа и реализации информационного потокав КС SELinux. Метод состоит из двух основных этапов. Первый этап - это построе-ние начального состояния предложенной ДП-модели КС SELinux по набору конфи-гурационных файлов КС. Второй этап - это построение time-замыкания полученногосостояния и интерпретация полученных результатов с точки зрения КС SELinux. Навходе метод имеет весь набор необходимых конфигурационных файлов КС SELinux,а на выходе - ответ на вопрос, возможны ли получение заданного права доступа илиреализация заданного информационного потока.

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