Results of realization conditions analysis for information flows by memory in ROSL DP-model.pdf В докладе в рамках ролевой ДП-модели управления доступом и информационнымипотоками в операционных системах семейства Linux [1] (РОСЛ ДП-модели) рассматри-ваются достаточные условия реализации информационного потока по памяти. Дадимопределения.Определение 1. Назовем траекторию функционирования системы S(G*, OP)траекторией без информационных потоков по времени и кооперации доверенных инедоверенных субъект-сессий для передачи прав доступа, если при ее реализациииспользуются только монотонные правила преобразования состояний и доверенныесубъект-сессии не берут роли во множество де-факто текущих ролей; не дают другимролям права доступа к сущностям; не изменяют атрибутов сущностей-контейнеров ине переименовывают сущности; не инициируют создание сущностей, субъект-сессийи жёстких ссылок на сущности, получение доступов к сущностям или де-факто вла-дения к субъект-сессиями; не используют де-факто владение субъект-сессиями длявыполнения от их имени правил преобразования состояний системы; не создают ин-формационный поток по памяти к сущности i_entity в случае, когда правила преоб-разования состояний инициируются недоверенными субъект-сессиями; не реализуютинформационные потоки по памяти к сущностям, функционально ассоциированнымс доверенными субъектами, или от сущностей, параметрически ассоциированных с до-веренными субъектами.Определение 2. Пусть Go - состояние системы E(G*, OP), в котором существу-ют сущности x , y . E, x = y. Определим предикат can_write_memory(x, y, G0), ис-тинный тогда и только тогда, когда существуют состояния G1 , . . . , Gn и правила пре-образования состояний o p i , . . . , opN, такие, что Go ^opx Gi ^op2 . . . ^~OPN Gn, где N ^ 0,является траекторией без информационных потоков по времени и кооперации дове-ренных и недоверенных субъект-сессий для передачи прав доступа, и выполняетсяусловие (x,y,writem) . FN.Определение 3. Пусть G - состояние системы E(G*,OP), в котором существу-ют сущности x, y . E, x = y. Определим предикат direct/y_can_write_memory(x, y, G),истинный тогда и только тогда, когда существует последовательность сущностейe 1 , . . . , e m . E, где e1 = x, em = y, m ^ 2, и либо m =2 и (x,y,writem) . F, либодля каждого i = 1 , . . . , m - 1 выполняется одно из условий 1-4:1) 6j . LS П S и либо [(ej, ei + 1 , writem) . F], либо [(ej,ei+1, writea) . A и не су-ществует доверенной субъект-сессии ej+1 . Ls П S, такой, что ei + 1 . [ej+1] и (ej,ej) .. (ej+1)/(E)].2) ei . Ns П S и выполняется одно из условий:- (ei,ei+1,writem) . F;- существует ei . S, такая, что ei . de_facto_own(ei ) и или (ei, ei+1, writem) . F,или ei+1 . E \ S и (ei, ei+1, writea) . A;- ei+1 . E \ S и существует ei . S, такая, что ei . de_facto_own(ei), execute_container(ei,ei+1) = true, ie(ei+1) ^ is(ei), [если ie(ei+1) = i_high, то существуетei' Е S, такая, что ei' Е de_facto_own(ei ) , (ei', i_entity, writea) Е A], и возможенодин из двух случаев: (ei + 1,writer ) Е PA(roles(ei)); существует r Е UA(user(ei)), такая, что (ei + 1,writer ) Е PA(r), [для e Е]Г[либо (ei,e,reada) Е A, либо (ei, e, writea) Е A], ir(r) ^ is(ei), [если ir(r) == i_high, то существует (ei', i_entity, writea) Е A], Constraint^(roles') = true,где [roles'(ei) = roles(ei) U { r } и для e' = ei справедливо roles'(e') = roles(e')];- ei + 1 Е E \ S и существуют ei Е S, r Е can_manage_rights(roles(ei) П AR) ПHroles(ei), такие, что ei Е de_facto_own(ei ) , ie(ei+1) ^ ir(r) ^ is(ei), [еслиie(ei+1) = i_high, то существует ei' Е S, такая, что (ei', i_entity, writea) Е A],ConstraintP(PA') = true, где [PA'(r) = PA(r) U {(ei + 1 , writer )} и для r' = rсправедливо PA'(r') = PA(r')] и либо [(ei,ei + 1,owna) Е A], либо [(ei + 1,ownr ) ЕЕ PA(roles(ei)) и execute_container(ei, ei + 1 ) = true].3) ei + 1 Е Ls П S, (ei+1, ei , reada) Е A, и либо не существует доверенной субъект-сессии ei+1 Е LS П S, такой, что ei + 1 Е [ei+1] и (ei+1,ei ) Е (ei+ 1)/(E), либо не существуетдоверенной субъект-сессии ei Е LS П S, такой, что ei E]ei[ и (ei + 1 , e i + 1 ) Е (ei)P(E).4) ei + 1 Е NS П S, ei E E \ S и существует ei+1 E S, такая, что ei+1 E de_facto_own(ei + 1 ) и выполняется одно из следующих условий:- (ei+1,ei, reada) Е A;- execute_container(ei+1, ei ) = true и возможен один из двух случаев: (ei,readr ) Е PA(roles(ei+1)); существует r Е UA(user(ei+1)), такая, что (ei,readr ) Е PA(r), [для e E]r[ либо(ei+1, e, reada) E A, либо (ei+1, e, writea) E A], ir(r) ^ is(ei+1), [если ir(r) == i_high, то существует (ei'+1, i_entity, writea) E A], Constraint^(roles') == true, где [roles'(ei+1) = roles(ei+1) U { r } и для e' = ei+1 справедливоroles'(e' ) = roles(e')];- существует r E can_manage_rights(roles(ei+1) П AR) П roles(ei+1), такая, чтоei+1 E de_facto_own(ei+1 ) , ie(ei ) ^ ir(r) ^ is(ei+1), если ie(ei ) = i_high, то су-ществует ei'+1 E S, такая, что (ei'+1, i_entity, writea) E A, ConstraintP(PA') == true, где [PA'(r) = PA(r) U { ( e i,readr ) } и для r' = r справедливо PA'(r') == PA(r')], и либо [(ei+1, ei , owna) E A], либо [(ei,ownr ) E PA(roles(ei+1)) иexecute_container(ei+1, ei ) = true].Справедливо следующее утверждение о достаточных условиях истинности преди-ката can_write_memory(x, y, G0).Утверждение 1. Пусть G0 - состояние системы E(G*, OP), в котором существу-ют сущности x , y Е E0 , x = y. Если истинен предикат directly_can_write_memory(x,y,G0 ) , то истинен предикат can_write_memory(x, y, G0).В дальнейшем планируется развитие РОСЛ ДП-модели по следующим направ-лениям: расширение достаточных условий реализации информационных потоков попамяти, анализ условий получения недоверенной субъект-сессией контроля над дове-ренной субъект-сессией, а также включение в модель элементов, позволяющих задатьв ней мандатное управление доступом.

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