Развитие семейства ДП-моделей логического управления доступом в компьютерных системах д.т.н., доцент Девянин П.Н. ИКСИ, г. Москва

2 Основные формальные модели управления доступом и информационными потоками Формальные модели Модели дискреционного управления доступом Модели мандатного управления доступом Модели безопасности информационных потоков Модели ролевого управления доступом Субъектно-ориентированная модель изолированной программной среды Модель ХРУ Модель ТМД Модель Take-Grant Базовая модель ролевого управления доступом Автоматная модель Программная модель Вероятностная модель Классическая модель Белла-ЛаПадулы Модель СВС Модель безопасности переходов Модель целостности Биба Модель ролевого администрирования Модели тематического управления доступом Модель мандатного ролевого управления доступом

3 Основные существенные особенности функционирования современных КС Возможность реализации в КС доверенных и недоверенных субъектов с различными условиями функционирования; Возможность реализации в КС доверенных и недоверенных субъектов с различными условиями функционирования; Различие в условиях реализации в КС информационных потоков по памяти и по времени; Различие в условиях реализации в КС информационных потоков по памяти и по времени; Наличие в современных КС иерархической структуры сущностей и возможность ее использования при реализации информационных потоков по времени; Наличие в современных КС иерархической структуры сущностей и возможность ее использования при реализации информационных потоков по времени; Возможность кооперации или, наоборот, противодействия субъектов друг другу при передаче прав доступа и реализации информационных потоков; Возможность кооперации или, наоборот, противодействия субъектов друг другу при передаче прав доступа и реализации информационных потоков; Возможность изменения функциональности субъекта при реализации информационного потока по памяти на функционально ассоциированные с ним сущности. Возможность изменения функциональности субъекта при реализации информационного потока по памяти на функционально ассоциированные с ним сущности.

4 Элементы базовой ДП-модели E = O C множество сущностей, где O множество объектов, C множество контейнеров; S E множество субъектов; R r = {read r, write r, append r, execute r, own r } множество видов прав доступа; R a = {read a, write a, append a } множество видов доступа; R f = {write m, write t } множество видов информационных потоков; R raf = R r R a R f множество видов прав доступа, видов доступа и видов информационных потоков. Определение. Определение. Определим H: E 2 E функцию иерархии сущностей, сопоставляющую каждой сущности c E множество сущностей H(c) E и удовлетворяющую условиям: Условие 1. Условие 1. Если сущность e H(c), то e < c и не существует сущности- контейнера d C, такой, что e < d, d < c. Условие 2. Условие 2. Для любых сущностей e 1, e 2 E, e 1 e 2, по определению выполняются равенство H(e 1 ) H(e 2 ) = и условия: если o O, то выполняется равенство H(o) = ; если e 1 < e 2, то или e 1, e 2 E \ S, или e 1, e 2 S; если e E \ S, то H(e) E \ S; если s S, то H(s) S.

5 Определение. Пусть определены множества S, E, R S E R r, A S E R a, F E E R f и функция иерархии сущностей H. Определим G = (S, E, R A F, H) конечный помеченный ориентированный граф без петель, где элементы множеств S, E являются вершинами графа, элементы множества R A F ребрами графа. Назовем G = (S, E, R A F, H) графом доступов. (G*, OP) система, при этом: каждое состояние системы представляется графом доступов; G* множество всех возможных состояний; OP множество правил преобразования состояний. G op G переход системы (G*, OP) из состояния G в состояние G Определение системы а) б) в)г) r a write m write t

6 Правила преобразования состояний В базовой ДП-модели определены 16 монотонных и немонотонных правил преобразования состояний: take_right( r, x, y, z), grant_right( r, x, y, z), remove_right( r, x, y, z), own_take( r, x, y), own_remove( r, x, y), create_entity(x, y, z), create_subject(x, y, z), delete_entity(x, y, z), rename_entity(x, y, z), access_read(x, y), access_write(x, y), access_append(x, y), flow(x, y, y, z), find(x, y, z), post(x, y, z), pass(x, y, z) G z G z write r write r write t write t x y x y rename_entity(x, y, z) … write t write t … r r s y s y

7 Семейство ДП-моделей ДП-модель без кооперации доверенных и недоверенных субъектов ДП-модель с блокирующими доступами доверенных субъектов ДП-модель с функционально ассоциированными с субъектами сущностями ДП-модель для политики безопасного администрирования Мандатная ДП-модель с отождествлением порожденных субъектов Мандатная ДП-модель для политики строгого мандатного управления доступом Мандатная ДП-модель с блокирующими доступами доверенных субъектов ДП-модель с функционально и параметрически ассоциированными с субъектами сущностями ДП-модель файловой системы Базовая ролевая ДП- модель Базовая дискреционная ДП-модель Мандатная ДП-модель ДП-модель для политики абсолютного разделения административных и пользовательских полномочий

8 ДП-модель с функционально ассоциированными с субъектами сущностями (ФАС ДП-модель) G 0 G 1 own r write m control(x, y, z) x z y x z y Права доступа Информационные потоки по памяти Информационные потоки по времени Доступы

9 ФАС ДП-модель Теорема. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) начальное состояние системы (G*, OP, G 0 ), в котором A 0 = F 0 =, и недоверенный субъект x N S S 0, доверенный субъект y L S S 0. Пусть истинен предикат can_share_own(x, y, G 0, L S ). Тогда существуют недоверенный субъект x N S S 0, доверенный субъект y L S S 0, сущность e [y] такие, что выполняется одно из условий. Условие 1. x = e. Условие 2. (x, e, r ) R 0, где r {own r, write r, append r }. Условие 3. Существует доверенный субъект y L S S 0 такой, что истинен предикат can_write_memory(y, e, G 0, L S ), и выполняется одно из условий: субъект y некорректен относительно сущности x; субъект y некорректен относительно сущности x; право доступа (x, y, r ) R 0, где r {write r, append r }; право доступа (x, y, r ) R 0, где r {write r, append r }; существует сущность e E 0 такая, что право доступа (x, e, r ) R 0, где r {own r, write r, append r }, и субъект y некорректен относительно сущности e. существует сущность e E 0 такая, что право доступа (x, e, r ) R 0, где r {own r, write r, append r }, и субъект y некорректен относительно сущности e. Определение. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) состояние системы (G*, OP) и недоверенный субъект x N S S 0, субъект y S 0, где x y. Определим предикат can_share_own(x, y, G 0, L S ), который будет истинным тогда и только тогда, когда существуют состояния G 1, …, G N и правила преобразования состояний op 1, …, op N, где N 0, такие, что траектория G 0 op1 G 1 op2 … opN G N является траекторией без кооперации доверенных и недоверенных субъектов для передачи прав доступа и реализации информационных потоков, и (x, y, own r ) R N.

10 ДП-модель веб-системы (Назаров И.О.) e f1, e f2, e f3 сущности-функции ядра веб-системы; e kernel сущность-каталог, содержащая функции ядра веб-системы в виде исполняемых модулей; s i доверенный субъект-интерфейс веб-системы; e p сущность-параметр, ассоциированная с субъектом- интерфейсом и используемая им при выборе сущности- функции для активизации; s 1, s 2, s 3 доверенные субъекты-потоки HTTP-сервера, реализующие передачу данных от пользователей к интерфейсу веб-системы и наоборот; e 1, e 2, e 3, e 4, e 5 сущности-порты, используемые субъектами-потоками HTTP-сервера, для записи в них и чтения из них данных при реализации взаимодействия между пользователем и интерфейсом; s a доверенный субъект-пользователь веб-системы; e s сущность-скрипт, функционально ассоциированная с субъектом-пользователем и исполняющаяся в браузере пользователя веб-системы; s u недоверенный субъект-пользователь веб-системы. Утверждение. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) начальное состояние системы 1 (G*, OP, G 0 ), в котором недоверенный субъект s u N S S 0, доверенный субъект s a L S S 0, сущность e s E 0 такие, что e s [s a ], пусть также право доступа владения (s u, s a, own r ) N r, тогда выполняются следующие условия: Условие 1. Предикат can_write_memory(s u, e s, G 0, L S ) является истинным. Условие 2. Предикат can_share_own(s u, s i, G 0, L S ) является истинным и возможно нарушение безопасности системы.

11 e b1, e b2 сущности-«банки данных» СУБД веб-системы; e base сущность-«база данных», содержащая сущности «банки данных»; s d доверенный субъект-драйвер СУБД веб-системы; e q сущность-запрос, функционально ассоциированная с субъектом-драйвером; e r сущность-результат; s i доверенный субъект-интерфейс веб-системы; e p сущность-параметр, ассоциированная с субъектом- интерфейсом; s 1, s 2 доверенные субъекты-потоки, являющиеся потоками ОС, порожденными процессом HTTP-сервера; e 1, e 2, e 3 сущности-порты, используемые субъектами- потоками HTTP-сервера для записи в них и чтения из них данных; s u недоверенный субъект-пользователь веб-системы; e out сущность-устройство вывода данных рабочей станции субъекта-пользователя. Утверждение. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) начальное состояние системы 1 (G*, OP, G 0 ), в котором недоверенный субъект s u N S S 0, доверенный субъект s d L S S 0, сущность e q E 0 такие, что e q [s d ]. Тогда выполняются следующие условия: Условие 1. Предикат can_share_own(s u, s d, G 0, L S ) является истинным. Условие 2. Предикат can_write_memory(e b2, e out, G 0, L S ) является истинным и возможно нарушение безопасности системы. ДП-модель веб-системы на основе СУБД (Назаров И.О.)

12 ДП-модель с функционально и параметрически ассоциированными с субъектами сущностями (ФПАС ДП-модель, Колегов Д.Н.) G 0 G 1 own r write m control(x, y, z) x z [y] y x z [y] y G 0 G 1 own r write m know(x, y) x z ]y[ y x z ]y[ y G 0 z 1 ]y[ G 1 z 1 ]y[ write m write m own r know(x, y) x y x y write m write m z 2 ]y[ z 2 ]y[

13 ФПАС ДП-модель (Колегов Д.Н.) Определение. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) состояние системы (G*, OP) и недоверенный субъект x N S S 0, субъект y S 0, где x y. Определим предикат directly_can_share_own(x, y, G 0, L S ), который будет истинным тогда и только тогда, когда существует последовательность субъектов s 1, …, s m S 0, где s 1 = x, s m = y и m 2, таких, что для каждого i = 1,..., m – 1 справедливо неравенство s i s i + 1 и выполняется одно из условий: s i [s i + 1 ]; s i [s i + 1 ]; истинен предикат can_share(own r, s i, s i + 1, G 0, L S ); истинен предикат can_share(own r, s i, s i + 1, G 0, L S ); существует сущность e [s i + 1 ] такая, что истинен предикат can_write_memory(s i, e, G 0, L S ); существует сущность e [s i + 1 ] такая, что истинен предикат can_write_memory(s i, e, G 0, L S ); для каждой сущности e ]s i + 1 [ истинен предикат can_write_memory(e, s i, G 0, L S ). для каждой сущности e ]s i + 1 [ истинен предикат can_write_memory(e, s i, G 0, L S ). Теорема. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) состояние системы (G*, OP), пусть также право доступа владения (x, y, own r ) N r, x N S S 0, y S 0, где x y. Предикат can_share_own(x, y, G 0, L S ) является истинным тогда и только тогда, когда существует последовательность субъектов s 1, …, s m S 0, где s 1 = x, s m = y и m 2, таких, что выполняется одно из условий. Условие 1. m = 2 и истинен предикат directly_can_share_own(x, y, G 0, L S ). Условие 2. m > 2 и для каждого i = 1,..., m – 2 выполняется одно из условий: s i, s i + 1 N S S 0 и истинны предикаты directly_can_share_own(s i, s i + 1, G 0, L S ), directly_can_share_own(s i + 1, s i + 2, G 0, L S ); s i, s i + 1 N S S 0 и истинны предикаты directly_can_share_own(s i, s i + 1, G 0, L S ), directly_can_share_own(s i + 1, s i + 2, G 0, L S ); i < m – 2, s i, s i + 2 N S S 0 и истинны предикаты directly_can_share_own(s i, s i + 1, G 0, L S ), directly_can_share_own( s i + 2, s i + 1, G 0, L S ); i < m – 2, s i, s i + 2 N S S 0 и истинны предикаты directly_can_share_own(s i, s i + 1, G 0, L S ), directly_can_share_own( s i + 2, s i + 1, G 0, L S ); i < m – 2, s i + 1, s i + 2 N S S 0 и истинны предикаты directly_can_share_own(s i + 1, s i, G 0, L S ), directly_can_share_own(s i + 2, s i + 1, G 0, L S ); i < m – 2, s i + 1, s i + 2 N S S 0 и истинны предикаты directly_can_share_own(s i + 1, s i, G 0, L S ), directly_can_share_own(s i + 2, s i + 1, G 0, L S ); s i + 1 N S S 0 и истинны предикаты directly_can_share_own(s i + 1, s i, G 0, L S ), directly_can_share_own(s i + 1, s i + 2, G 0, L S ). s i + 1 N S S 0 и истинны предикаты directly_can_share_own(s i + 1, s i, G 0, L S ), directly_can_share_own(s i + 1, s i + 2, G 0, L S ).

14 ДП-модель файловых систем (ФС ДП-модель, Буренин П.В.) Предположение. В рамках ФС ДП-модели выполняются следующие условия. Условие 1. Во множестве сущностей выделено подмножество сущностей, защищенных ФС и не являющихся субъектами. Условие 2. Во множестве доверенных субъектов выделено подмножество субъектов, обладающих правами доступа и реализующих доступ к сущностям, защищенным ФС, и кодирование в них данных в случае, когда оно осуществляется ФС. Эти доверенные субъекты реализуют информационные потоки по памяти между каждой сущностью, защищенной ФС, и соответствующей ей сущностью-образом, не являющейся субъектом. Условие 3. Доверенные или недоверенные субъекты, не реализующие доступ к сущностям, защищенным ФС, не обладают правами доступа и не могут получать доступ к этим сущностям. При этом они могут обладать правами доступа или получать доступ к сущностям-образам сущностей, защищенных ФС. Условие 4. В каждом состоянии системы кроме множества субъектов анализируется множество потенциальных доверенных субъектов (доверенных субъектов, которые могут быть созданы в процессе функционирования системы для реализации доступа к сущностям, защищенным ФС). Условие 5. Кроме возможности создания новых субъектов из сущностей недоверенный субъект может создать доверенного субъекта в случае, когда недоверенный субъект реализовал к себе информационные потоки по памяти от всех сущностей, параметрически ассоциированных с потенциальным доверенным субъектом. При этом недоверенный субъект получает контроль над созданным доверенным субъектом. Условие 6. Каждый доверенный субъект не обладает правами доступа ко всем сущностям. Условие 7. Доверенные субъекты, не реализующие доступ к сущностям, защищенным ФС, в процессе функционирования системы не получают новые доступы к сущностям и не участвуют в создание информационных потоков к или от сущностей, защищенных ФС. Условие 8. Не рассматриваются информационные потоки по времени, право доступа и доступ на запись в конец сущности. Условие 9. В начальном состоянии системы недоверенные субъекты не реализуют доступы к сущностям, к ним не имеют доступы другие субъекты, и отсутствуют информационные потоки по памяти с участием недоверенных субъектов. FSE E \ S множество сущностей, защищенных ФС; fs: FSE E \ S инъективная функция, которая ставит в соответствие каждой сущности, защищенной ФС, соответствующую ей сущность-образ; PS множество потенциальных доверенных субъектов, реализующих доступ к сущностям из множества FSE; FSS L S S множество доверенных субъектов, реализующих доступ к сущностям из множества FSE.

15 ФС ДП-модель (Буренин П.В.). Запрещенные информационные потоки Определение. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) начальное состояние системы (G*, OP, G 0 ). Запрещенным информационным потоком по памяти является информационный поток от сущности e FSE, защищенной ФС, к недоверенному субъекту x N S S 0 в случае, когда в начальном состоянии G 0 субъект x не имеет прав доступа read r или own r к сущности-образу fs(e) E, соответствующей сущности e. Определение. В рамках ФС ДП- модели будем говорить, что система (G*, OP, G 0 ) является безопасной в случае, когда невозможен переход системы в состояние, в котором реализуется запрещенный информационный поток по памяти. Определение. Нарушитель в рамках ФС ДП-модели любой недоверенный субъект системы.

16 ФС ДП-модель (Буренин П.В.). Правило potential_subject(x, y, z)

17 ФС ДП-модель (Буренин П.В.). Достаточные условия реализации запрещенного информационного потока Определение. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) состояние системы (G*, OP) и недоверенный субъект x N S S 0, субъект или потенциальный доверенный субъект y S 0 PS, где x y. Определим предикат directly_can_share_own(x, y, G 0 ), который будет истинным тогда и только тогда, когда существует последовательность субъектов s 1, …, s m S 0 PS, где s 1 = x, s m = y и m 2, таких, что для каждого i = 1,..., m – 1 справедливо неравенство s i s i + 1 и выполняется одно из условий: s i + 1 FSS 0 и s i [s i + 1 ] (каждый доверенный субъект из множества FSS 0 является функционально корректным); s i + 1 FSS 0 и s i [s i + 1 ] (каждый доверенный субъект из множества FSS 0 является функционально корректным); истинен предикат simple_can_share(own r, s i, s i + 1, G 0 ); истинен предикат simple_can_share(own r, s i, s i + 1, G 0 ); s i + 1 FSS 0 и существует сущность e [s i + 1 ] такая, что истинен предикат simple_can_write_memory(s i, e, G 0 ) (невозможно получение к доверенному субъекту из множества FSS 0 права доступа владения с использованием реализованного к нему информационного потока по памяти); s i + 1 FSS 0 и существует сущность e [s i + 1 ] такая, что истинен предикат simple_can_write_memory(s i, e, G 0 ) (невозможно получение к доверенному субъекту из множества FSS 0 права доступа владения с использованием реализованного к нему информационного потока по памяти); для каждой сущности e ]s i + 1 [ истинен предикат simple_can_write_memory(s i, e, G 0 ). для каждой сущности e ]s i + 1 [ истинен предикат simple_can_write_memory(s i, e, G 0 ). Теорема. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) состояние системы (G*, OP) и сущности x, y E 0, где x y. Предикат can_write_memory(x, y, G 0 ) является истинным в случае, когда существует последовательность сущностей e 1, …, e m E 0, где e 1 = x, e m = y и m 2, таких, что для каждого i = 1,..., m – 1 выполняется одно из условий. Условие 1. e i L S S 0 и или (e i, e i + 1, write m ) F 0, или (e i, e i + 1, write a ) A 0. Условие 2. e i FSS 0 (N S S 0 ) и или (e i, e i + 1, write m ) F 0, или истинен предикат can_share(write r, e i, e i + 1, G 0 ). Условие 3. e i + 1 L S S 0 и (e i + 1, e i, read a ) A 0. Условие 4. e i + 1 FSS 0 (N S S 0 ) и истинен предикат can_share(read r, e i + 1, e i, G 0 ). Условие 5. e i N S S 0, e i + 1 FSS 0 (N S S 0 ) и истинен предикат can_share_own(e i, e i + 1, G 0 ). Условие 6. e i + 1 N S S 0, e i FSS 0 (N S S 0 ) и истинен предикат can_share_own(e i + 1, e i, G 0 ).

18 Основные ролевые модели семейства RBAC Административные права доступа U R P S ARAP Иерархия ролей Пользователи Сессии Права доступа Роли Административные роли Ограничения Иерархия административных ролей Базовая модель; Модель ролевого администрирования; Модель мандатного ролевого управления доступом.

19 Специфика ролевого управления доступом Наличие статических и, особенно, динамических ограничений на роли пользователей, роли сессий и права доступа ролей; Наличие статических и, особенно, динамических ограничений на роли пользователей, роли сессий и права доступа ролей; Сложный анализ условий передачи прав доступа с учетом наличия прав доступа к сущностям только у ролей (вопрос о фактических ролях, фактических правах доступа сессий, фактических возможных действий); Сложный анализ условий передачи прав доступа с учетом наличия прав доступа к сущностям только у ролей (вопрос о фактических ролях, фактических правах доступа сессий, фактических возможных действий); Необходимость уточнения способов классификации субъектов на доверенные и недоверенные; Необходимость уточнения способов классификации субъектов на доверенные и недоверенные; Каскадное удаление или добавление прав доступа с использованием иерархии ролей; Каскадное удаление или добавление прав доступа с использованием иерархии ролей; Неэффективность использования графов доступов для описания состояний. Неэффективность использования графов доступов для описания состояний.

20 Базовая ролевая ДП-модель Элементы ДП-моделей КС с дискреционным или мандатным управлением доступом: E = O C множество сущностей, где O множество объектов, C множество контейнеров; S E множество субъект-сессий пользователей; L S S множество доверенных субъект-сессий; N S = S \ L S множество недоверенных субъект-сессий; [s] E множество всех сущностей, функционально ассоциированных с субъект-сессией s; R r = {read r, write r, append r, execute r, own r } множество видов прав доступа; R a = {read a, write a, append a, own a } множество видов доступа; R f = {write m, write t } множество видов информационных потоков; H E : E 2 E функция иерархии сущностей.

21 Базовая ролевая ДП-модель Элементы моделей КС с ролевым управлением доступом (RBAC и ARBAC): U множество пользователей; R множество ролей; AR множество административных ролей (AR R = ); P E R r множество прав доступа к сущностям; UA: U 2 R функция авторизованных ролей пользователей; AUA: U 2 AR функция авторизованных административных ролей пользователей; PA: R 2 P функция прав доступа ролей; user: S U функция принадлежности субъект-сессии пользователю; roles: S 2 R 2 AR функция текущих ролей субъект-сессий; H R : R 2 R функция иерархии ролей; H AR : AR 2 AR функция иерархии административных ролей.

22 Базовая ролевая ДП-модель can_manage_rights: AR 2 R функция администрирования прав доступа ролей; A S E R a множество доступов субъект-сессий к сущностям; F E E R f множество информационных потоков; G = (UA, AUA, PA, user, roles, A, F, H R, H AR, H E, L U, L S ) состояние системы; (G*, OP) система, при этом G* множество всех возможных состояний, OP множество правил преобразования состояний, G op G переход системы из состояния G в состояние G с использованием правила преобразования состояний; (G*, OP) система, при этом G* множество всех возможных состояний, OP множество правил преобразования состояний, G op G переход системы из состояния G в состояние G с использованием правила преобразования состояний; (G*, OP, G 0 ) система (G*, OP) с начальным состоянием G 0. (G*, OP, G 0 ) система (G*, OP) с начальным состоянием G 0. Предположение. В рамках БР ДП-модели на траекториях функционирования системы не изменяются: значения множеств U, L U, R, функции UA, AUA, H R, H AR. Предположение. Каждые пользователь или субъект-сессия системы (G*, OP) вне зависимости от имеющихся у них авторизованных ролей являются либо доверенными, либо недоверенными. Доверенные пользователи или субъект- сессии не создают новых субъект-сессий. Каждые недоверенный пользователь или субъект-сессия могут создать только недоверенную субъект-сессию.

23 Фактические роли, права доступа, возможные действия Предположение. Субъект-сессии могут иметь друг другу только доступ владения own a. Роли могут обладать к субъект-сессиям только правом доступа владения own r. Если субъект-сессия s 1 реализовала информационный поток по памяти от себя к сущности, функционально ассоциированной с другой субъект-сессией s 2, то субъект-сессия s 1 получает: доступ владения own a к субъект-сессии s 2 ; доступ владения own a к субъект-сессии s 2 ; возможность использовать роли из множества ролей roles(s 2 ) (при этом субъект-сессия s 1 не может изменить множество текущих ролей roles(s 2 )); возможность использовать роли из множества ролей roles(s 2 ) (при этом субъект-сессия s 1 не может изменить множество текущих ролей roles(s 2 )); возможность получать доступ владения own a к субъект-сессиям, доступом владения к которым обладает субъект-сессия s 2 ; возможность получать доступ владения own a к субъект-сессиям, доступом владения к которым обладает субъект-сессия s 2 ; возможность использовать административные роли субъект-сессии s 2 для осуществления действий над ролями и сущностями, которые позволяют ей изменять права доступа ролей субъект-сессии s 2. возможность использовать административные роли субъект-сессии s 2 для осуществления действий над ролями и сущностями, которые позволяют ей изменять права доступа ролей субъект-сессии s 2. возможность использовать информационные потоки, в реализации которых участвует субъект-сессия s 2. возможность использовать информационные потоки, в реализации которых участвует субъект-сессия s 2. de_facto_roles: S 2 R функция фактических текущих ролей субъект-сессий; de_facto_rights: S 2 P функция фактических текущих прав доступа субъект- сессий. de_facto_actions: S 2 P 2 R функция фактических возможных действий субъект- сессий

24 Примеры задания правил преобразования состояний

25 Монотонные правила Определение. Назовем правило преобразования состояний монотонным, если его применение не приводит к удалению из состояний: ролей из множества текущих ролей субъект-сессии, прав доступа ролей к сущностям, субъект-сессий или сущностей, доступов субъект-сессий к сущностям, информационных потоков. Монотонными правила (17): take_role(x, r), grant_right(x, r, (y, r )), create_entity(x, r, y, z), create_first_session(u, r, y, z), create_session(x, w, r, y, z), rename_entity(x, y, z), control(x, y, z), access_own(x, y), take_access_own(x, y, z), access_read(x, y), access_write(x, y), access_append(x, y), flow(x, y, y, z), find(x, y, z), post(x, y, z), pass(x, y, z), take_flow(x, y). Немонотонными правила (3): remove_role(x, r), remove_right(x, r, (y, r )), delete_entity(x, y, z). Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) начальное состояние системы (G*, OP, G 0 ). Пусть также существуют состояния системы G 1, …, G N и правила преобразования состояний op 1, …, op N такие, что G 0 op1 G 1 op2 … opN G N, где N 0. Тогда существуют состояния G 1, …, G M, где M 0, и монотонные правила преобразования состояний op 1, …, op M такие, что G 0 op1 G 1 op2 … opM G M и выполняются следующие условия. Условие 1. Верно включение S N S M, и для каждого субъект-сессии s S N выполняются условия: user N (s) = user M (s), roles N (s) roles M (s). Условие 2. Верно включение E N E M, и для каждой сущности e E N выполняется условие H EN (e) H EM (e). Условие 3. Для каждой роли r R выполняется условие PA N (r) PA M (r). Условие 4. Верно включение A N A M. Условие 5. Верно включение F N F M.

26 Связь условий и результатов применения правил преобразования состояний в рамках ФАС ДП-модели Права доступа Информационные потоки по памяти Информационные потоки по времени Доступы

27 Зависимость условий и результатов применения правил преобразования состояний БР ДП-модели PA PA F F A P Пользователи (U) Субъект-сессии (S) Роли (R AR) Права доступа own r к субъект- сессиям Права доступа к сущностям Доступы own a к субъект-сессиям Доступы к сущностям Информационные потоки по памяти Информационные потоки по времени user roles de_facto_roles UA, AUA UA, AUA control(x, y, z)

28 Траектории без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа Определение. Назовем траекторию функционирования системы (G*, OP) траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, если при ее реализации используются только монотонные правила преобразования состояний, и доверенные субъект-сессии: не берут роли во множество текущих ролей; не берут роли во множество текущих ролей; не дают другим ролям права доступа к сущностям; не дают другим ролям права доступа к сущностям; не получают доступ владения к субъект-сессиям. не получают доступ владения к субъект-сессиям. В системе (G*, OP) на траекториях без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа доверенные субъект-сессии: не инициируют выполнения следующих правил преобразования состояний: take_role(x, r), grant_right(x, r, (y, r )), create_session(x, w, r, y, z), control(x, y, z), access_own(x, y), take_access_own(x, y, z), take_flow(x, y); не инициируют выполнения следующих правил преобразования состояний: take_role(x, r), grant_right(x, r, (y, r )), create_session(x, w, r, y, z), control(x, y, z), access_own(x, y), take_access_own(x, y, z), take_flow(x, y); могут выполнять монотонные правила преобразования состояний: create_entity(x, r, y, z), rename_entity(x, y, z), access_read(x, y), access_write(x, y), access_append(x, y), flow(x, y, y, z), find(x, y, z), post(x, y, z), pass(x, y, z); могут выполнять монотонные правила преобразования состояний: create_entity(x, r, y, z), rename_entity(x, y, z), access_read(x, y), access_write(x, y), access_append(x, y), flow(x, y, y, z), find(x, y, z), post(x, y, z), pass(x, y, z); недоверенные пользователи могут инициировать выполнение правила create_first_session(u, r, y, z). недоверенные пользователи могут инициировать выполнение правила create_first_session(u, r, y, z).

29 Случай двух субъект-сессий. Предикаты Случай двух субъект-сессий. Предикаты can_share((e, ), x, G 0 ) и directly_grant_right(x, y, G) Определение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют пользователь x U 0 и право доступа к сущности (e, ) P 0. Определим предикат can_share((e, ), x, G 0 ), который будет истинным тогда, и только тогда, когда существуют состояния G 1, …, G N и правила преобразования состояний op 1, …, op N такие, что G 0 op1 G 1 op2 … opN G N является траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существует субъект-сессия s x S N такая, что user N (s x ) = x и право доступа к сущности (e, ) de_facto_rights N (s x ), где N 0. Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором недоверенная субъект-сессия или недоверенный пользователь x N U (N S S), субъект- сессия или недоверенный пользователь y N U S. Определим предикат directly_grant_right(x, y, G), который будет истинным тогда, и только тогда, когда или x = y, или выполняется одно из условий 1-4. Условие 1. Если y N U и x N U, то существует роль r can_manage_rights(AUA(x)) UA(y). Условие 2. Если y N U и x N S S, то существуют роль r can_manage_rights(AUA(user(x))) UA(y). Условие 3. Если y S и x N U, то выполняется одно из условий: y N S S и существуют роль r can_manage_rights(AUA(x)) UA(user(y)); y N S S и существуют роль r can_manage_rights(AUA(x)) UA(user(y)); y L S S и существуют роль r can_manage_rights(AUA(x)) roles(y). y L S S и существуют роль r can_manage_rights(AUA(x)) roles(y). Условие 4. Если y S и x N S S, то выполняется одно из условий: y N S S и существуют роль r can_manage_rights(AUA(user(x))) UA(user(y)); y N S S и существуют роль r can_manage_rights(AUA(user(x))) UA(user(y)); y L S S и существуют роль r can_manage_rights(AUA(user(x))) roles(y). y L S S и существуют роль r can_manage_rights(AUA(user(x))) roles(y).

30 Случай двух субъект-сессий. Случай двух субъект-сессий. Предикат directly_access_own(x, y, G) Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x N U (N S S), субъект-сессия или недоверенный пользователь y N U S. Определим предикат directly_access_own(x, y, G), который будет истинным тогда, и только тогда, когда или x = y, или выполняется одно из условий 1-6. Условие 1. Если y N U и x N U, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и выполняется одно из условий или r y UA(x), или x fa(y, e y ), или существует сущность e E такая, что (e, ) PA(UA(x)), где {write r, append r, own r }, и или e fa(y, e y ), или (e, ) PA(UA(y)), где {read r, own r }. Условие 2. Если y N U и x N S S, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и выполняется одно из условий или r y UA(user(x)), или x fa(y, e y ), или существует сущность e E такая, что (e, ) PA(UA(user(x)), где {write r, append r, own r }, или (x, e, write m ) F, и или e fa(y, e y ), или (e, ) PA(UA(y)), где {read r, own r }. Условие 3. Если y N U и x L S S, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и выполняется одно из условий или r y roles(x), или x fa(y, e y ), или существует сущность e E такая, что (e, ) PA(roles(x)), где {write r, append r }, или (x, e, write m ) F, и или e fa(y, e y ), или (e, ) PA(UA(y)), где {read r, own r }. Условие 4. Если y S и x N U, то выполняется одно из условий или (y, own r ) PA(UA(x)), или x [y], или существует сущность e E такая, что (e, ) PA(UA(x)), где {write r, append r, own r }, и или e [y], или y N S S, (e, ) PA(UA(user(y))), где {read r, own r }, или y L S S, (e, read r ) PA(roles(y)), (y, e) y(E). Условие 5. Если y S и x N S S, то выполняется одно из условий или (y, own r ) PA(UA(user(x))), или x [y], или (x, y, own a ) A, или существует сущность e E такая, что (e, ) PA(UA(user(x)), где {write r, append r, own r }, или (x, e, write m ) F, и или e [y], или y N S S, (e, ) PA(UA(user(y))), где {read r, own r }, или y L S S, (e, read r ) PA(roles(y)), (y, e) y(E). Условие 6. Если y S и x L S S, то выполняется одно из условий или (y, own r ) PA(roles(x)), или x [y], или (x, y, own a ) A, или существует сущность e E такая, что (e, ) PA(roles(x)), где {write r, append r }, или (x, e, write m ) F, и выполняется одно из условий: y N S S и или e [y], или (e, ) PA(UA(user(y))), где {read r, own r }; y N S S и или e [y], или (e, ) PA(UA(user(y))), где {read r, own r }; y L S S и или e [y], (x, x) y(E), или (e, read r ) PA(roles(y)), (y, e) y(E). y L S S и или e [y], (x, x) y(E), или (e, read r ) PA(roles(y)), (y, e) y(E).

31 Случай двух субъект-сессий. Случай двух субъект-сессий. Предикат directly_can_share((e, ), x, G) Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором существует пользователь x N U и право доступа к сущности (e, ) P. Определим предикат directly_can_share((e, ), x, G), который будет истинным тогда, и только тогда, когда существует пользователь y U, и выполняется одно из условий 1-6, где {, own r }. Условие 1. Выполняется одно из условий: пользователь y N U, право доступа (e, ) PA(UA(y)), и истинен предикат directly_access_own(x, y, G); пользователь y N U, право доступа (e, ) PA(UA(y)), и истинен предикат directly_access_own(x, y, G); существует недоверенная субъект-сессия s y N S S такая, что user(s y ) = y, истинен предикат directly_access_own(x, s y, G) и (e, ) PA(UA(user(s y ))). существует недоверенная субъект-сессия s y N S S такая, что user(s y ) = y, истинен предикат directly_access_own(x, s y, G) и (e, ) PA(UA(user(s y ))). Условие 2. Существует недоверенная субъект-сессия s x N S S такая, что user(s x ) = x, и выполняется одно из условий: пользователь y N U, право доступа (e, ) PA(UA(y)) и истинен предикат directly_access_own(s x, y, G); пользователь y N U, право доступа (e, ) PA(UA(y)) и истинен предикат directly_access_own(s x, y, G); существует недоверенная субъект-сессия s y N S S такая, user(s y ) = y, истинен предикат directly_access_own(s x, s y, G), и (e, ) PA(UA(user(s y ))). существует недоверенная субъект-сессия s y N S S такая, user(s y ) = y, истинен предикат directly_access_own(s x, s y, G), и (e, ) PA(UA(user(s y ))). Условие 3. Существует доверенная субъект-сессия s y L S S такая, что user(s y ) = y, право доступа (e, ) PA(roles(s y )), и выполняется одно из условий: истинен предикат directly_access_own(x, s y, G); истинен предикат directly_access_own(x, s y, G); существует недоверенная субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_access_own(s x, s y, G). существует недоверенная субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_access_own(s x, s y, G). Условие 4. Если own r, то существует доверенная субъект-сессия s y L S S такая, что user(s y ) = y, право доступа (e, own r ) PA(roles(s y )), can_manage_rights(roles(s y ) AR) (roles(s y ) UA(x)), и выполняется одно из условий: истинен предикат directly_access_own(x, s y, G); истинен предикат directly_access_own(x, s y, G); существует недоверенная субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_access_own(s x, s y, G). существует недоверенная субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_access_own(s x, s y, G). Условие 5. Пользователь y N U, право доступа (e, own r ) PA(UA(y)), и выполняется одно из условий: пользователь x N U, и истинен предикат directly_grant_right(y, x, G); пользователь x N U, и истинен предикат directly_grant_right(y, x, G); существует субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_grant_right(y, s x, G). существует субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_grant_right(y, s x, G). Условие 6. Существует субъект-сессия s y N S S такая, что user(s y ) = y, право доступа (e, own r ) PA(UA(user(s y ))), и выполняется одно из условий: пользователь x N U, и истинен предикат directly_grant_right(s y, x, G); пользователь x N U, и истинен предикат directly_grant_right(s y, x, G); существует субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_grant_right(s y, s x, G). существует субъект-сессия s x N S S такая, что user(s x ) = x, и истинен предикат directly_grant_right(s y, s x, G).

32 Случай двух субъект-сессий. Условия непосредственного получения прав доступа Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x N U (N S S 0 ), субъект-сессия или недоверенный пользователь y N U S 0 и право доступа к сущности (e, ) P 0. Пусть истинен предикат directly_access_own(x, y, G 0 ) и выполняется одно из условий: если y N U, то (e, ) PA 0 (UA 0 (y)), где {, own r }; если y N U, то (e, ) PA 0 (UA 0 (y)), где {, own r }; если y N S S 0, то (e, ) PA 0 (UA 0 (user 0 (y))), где {, own r }; если y N S S 0, то (e, ) PA 0 (UA 0 (user 0 (y))), где {, own r }; если y L S S 0 и x N U, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (x)) ; если y L S S 0 и x N U, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (x)) ; если y L S S 0 и x N S S 0, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (user 0 (x))). если y L S S 0 и x N S S 0, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (user 0 (x))). Тогда выполняется одно из условий. Условие 1. Если x N U, то истинен предикат can_share((e, ), x, G 0 ). Условие 2. Если x N S S 0, то истинен предикат can_share((e, ), user 0 (x), G 0 ). Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x N U (N S S 0 ), субъект-сессия или недоверенный пользователь y N U S 0 и право доступа к сущности (e, ) P 0. Пусть истинен предикат directly_grant_right(x, y, G 0 ) и выполняется одно из условий: если x N U, то (e, own r ) PA 0 (UA 0 (x)); если x N U, то (e, own r ) PA 0 (UA 0 (x)); если x N S S 0, то (e, own r ) PA 0 (UA 0 (user 0 (x))). если x N S S 0, то (e, own r ) PA 0 (UA 0 (user 0 (x))). Тогда выполняется одно из условий. Условие 1. Если y N U, то истинен предикат can_share((e, ), y, G 0 ). Условие 2. Если y S 0, то истинен предикат can_share((e, ), user 0 (y), G 0 ). Теорема. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором выполняются условия |U 0 | 2, x N U, для каждого пользователя u U 0 верно неравенство |user 0 1 (u)| 1, и существует право доступа к сущности (e, ) P 0. Предикат can_share((e, ), x, G 0 ) является истинным тогда, и только тогда, когда является истинным предикат directly_can_share((e, ), x, G 0 ).

33 Случай двух субъект-сессий. Условия непосредственного получения прав доступа Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x N U (N S S 0 ), субъект-сессия или недоверенный пользователь y N U S 0 и право доступа к сущности (e, ) P 0. Пусть истинен предикат directly_access_own(x, y, G 0 ) и выполняется одно из условий: если y N U, то (e, ) PA 0 (UA 0 (y)), где {, own r }; если y N U, то (e, ) PA 0 (UA 0 (y)), где {, own r }; если y N S S 0, то (e, ) PA 0 (UA 0 (user 0 (y))), где {, own r }; если y N S S 0, то (e, ) PA 0 (UA 0 (user 0 (y))), где {, own r }; если y L S S 0 и x N U, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (x)) ; если y L S S 0 и x N U, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (x)) ; если y L S S 0 и x N S S 0, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (user 0 (x))). если y L S S 0 и x N S S 0, то либо (e, ) PA 0 (roles 0 (y)), либо (e, own r ) PA 0 (roles 0 (y)) и can_manage_rights(roles 0 (y) AR) (roles 0 (y) UA 0 (user 0 (x))). Тогда выполняется одно из условий. Условие 1. Если x N U, то истинен предикат can_share((e, ), x, G 0 ). Условие 2. Если x N S S 0, то истинен предикат can_share((e, ), user 0 (x), G 0 ). Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x N U (N S S 0 ), субъект-сессия или недоверенный пользователь y N U S 0 и право доступа к сущности (e, ) P 0. Пусть истинен предикат directly_grant_right(x, y, G 0 ) и выполняется одно из условий: если x N U, то (e, own r ) PA 0 (UA 0 (x)); если x N U, то (e, own r ) PA 0 (UA 0 (x)); если x N S S 0, то (e, own r ) PA 0 (UA 0 (user 0 (x))). если x N S S 0, то (e, own r ) PA 0 (UA 0 (user 0 (x))). Тогда выполняется одно из условий. Условие 1. Если y N U, то истинен предикат can_share((e, ), y, G 0 ). Условие 2. Если y S 0, то истинен предикат can_share((e, ), user 0 (y), G 0 ). Теорема. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором выполняются условия |U 0 | 2, x N U, для каждого пользователя u U 0 верно неравенство |user 0 1 (u)| 1, и существует право доступа к сущности (e, ) P 0. Предикат can_share((e, ), x, G 0 ) является истинным тогда, и только тогда, когда является истинным предикат directly_can_share((e, ), x, G 0 ).

34 Случай без информационных потоков по памяти PA PA F F A P Пользователи (U) Субъект-сессии (S) Роли (R AR) Права доступа own r к субъект- сессиям Права доступа к сущностям Доступы own a к субъект-сессиям Доступы к сущностям Информационные потоки по памяти Информационные потоки по времени user roles de_facto_roles UA, AUA UA, AUA control(x, y, z)

35 Случай без информационных потоков по памяти. Предикат simple_can_access_own(x, y, G 0 ) Определение. Траекторию без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа G 0 op1 G 1 op2 … opN G N, где N 0, назовем простой в случае, когда при ее реализации для 0 i N каждое правило op i не является правилом вида control(x, y, z), использующим для получения доступа владения субъект-сессией x к субъект-сессии y информационный поток по памяти (x, z, write m ), где z [y]. Определение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь x N U и субъект-сессия или недоверенный пользователь y N U S 0 такие, что x y. Определим предикат simple_can_access_own(x, y, G 0 ), который будет истинным тогда и только тогда, когда существуют состояния G 1, …, G N = (PA N, user N, roles N, A N, F N, H EN ) и правила преобразования состояний op 1, …, op N такие, что G 0 op1 G 1 op2 … opN G N, где N 0, является простой траекторией без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и существуют субъект-сессии s x, s y S N такие, что user N (s x ) = x, или s y = y, или user N (s y ) = y, и выполняется условие (s x, s y, own a ) A N. Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором существуют субъект- сессии или недоверенные пользователи x, y N U S. Определим предикат simple_directly_access_own(x, y, G), который будет истинным тогда и только тогда, когда или x = y, или выполняется одно из условий: если y N U и x N U, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и или r y UA(x), или x fa(y, e y ). если y N U и x N U, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и или r y UA(x), или x fa(y, e y ). если y N U и x N S S, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и или r y UA(user(x)), или x fa(y, e y ). если y N U и x N S S, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и или r y UA(user(x)), или x fa(y, e y ). если y N U и x L S S, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и или r y roles(x), или x fa(y, e y ). если y N U и x L S S, то существуют сущность e y E и роль r y R такие, что (e y, execute r ) PA(UA(y)), r y can_manage_rights(AUA(y)), и или r y roles(x), или x fa(y, e y ). если y S и x N U, то или (y, own r ) PA(UA(x)), или x [y]. если y S и x N U, то или (y, own r ) PA(UA(x)), или x [y]. если y S и x N S S, то или (y, own r ) PA(UA(user(x))), или x [y], или (x, y, own a ) A. если y S и x N S S, то или (y, own r ) PA(UA(user(x))), или x [y], или (x, y, own a ) A. если y S и x L S S, то или (y, own r ) PA(roles(x)), или x [y], или (x, y, own a ) A. если y S и x L S S, то или (y, own r ) PA(roles(x)), или x [y], или (x, y, own a ) A.

36 Случай без информационных потоков по памяти. Остров Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором существует субъект-сессия или недоверенный пользователь x N U S. Назовем множество X N U S островом субъект-сессии или недоверенного пользователя x, если справедливо равенство X = {x} {y (N U S) \ {x}: существует последовательность s 1, …, s m (N U S) \ {x}, где s 1 = x, s m = y и m 2, такая, что для каждого 1 i < m истинен предикат simple_directly_access_own(s i, s i + 1, G)}. Определим island: N U S 2 Nu 2 S функцию, задающую для каждого субъект-сессии или недоверенного пользователя соответствующий им остров. island_roles: N U (N S S) 2 R 2 AR функция, задающая для каждых недоверенного пользователя или недоверенной субъект-сессии x N U (N S S) роли, которыми обладают все субъект-сессии или недоверенные пользователи, принадлежащие острову x. При этом по определению справедливо равенство island_roles(x) = {r R AR: существует y island(x) и либо y N U и r UA(y) AUA(y), либо y N S S и r UA(user(y)) AUA(user(y)), либо y L S S и r roles(y)}. island_rights: N U (N S S) 2 P функция, задающая для каждых недоверенного пользователя или недоверенной субъект- сессии x N U (N S S) права доступа, которыми обладают все субъект-сессии или недоверенные пользователи, принадлежащие острову x. При этом по определению справедливо равенство island_rights(x) = {p P: существует r island_roles(x) и p PA(r)}. island_actions: N U (N S S) 2 P 2 R функция, задающая для каждых недоверенного пользователя или недоверенной субъект-сессии x N U (N S S) возможные действия, которыми обладают все субъект-сессии или недоверенные пользователи, принадлежащие острову x. При этом по определению справедливо равенство island_actions(x) = {(p, r) P R: существует y island(x) и либо y N U и (p, r) PA(UA(y)) can_manage_rights(AUA(y)), либо y N S S и (p, r) PA(UA(user(y))) can_manage_rights(AUA(user(y))), либо y L S S и (p, r) PA(roles(y)) can_manage_rights(roles(y) AR)}. Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь или недоверенная субъект-сессия x N U (N S S 0 ) и субъект-сессия или недоверенный пользователь y island(x) \ {x}. Тогда выполняется одно из условий: если x N U, то истинен предикат simple_can_access_own(x, y, G 0 ); если x N U, то истинен предикат simple_can_access_own(x, y, G 0 ); если x N S S 0, то истинен предикат simple_can_access_own(user 0 (x), y, G 0 ). если x N S S 0, то истинен предикат simple_can_access_own(user 0 (x), y, G 0 ).

37 Случай без информационных потоков по памяти. Обозначения в графе доступов если для роли r R AR и права доступа (e, ) P выполняется условие (e, ) PA(r), то в графе доступов r соединена с e ребром вида (а), и помеченным ; если для роли r R AR и права доступа (e, ) P выполняется условие (e, ) PA(r), то в графе доступов r соединена с e ребром вида (а), и помеченным ; если для недоверенного пользователя x N U и роли r R AR выполняется условие r UA(x) или r AUA(x), то в графе доступов x соединен с r ребром вида (б), и помеченным UA или AUA, соответственно; если для недоверенного пользователя x N U и роли r R AR выполняется условие r UA(x) или r AUA(x), то в графе доступов x соединен с r ребром вида (б), и помеченным UA или AUA, соответственно; если для недоверенной субъект-сессии x N S S и роли r R AR выполняется условие r UA(user(x)) или r AUA(user(x)), то в графе доступов x соединена с r ребром вида (в), и помеченным UA или AUA, соответственно; если для недоверенной субъект-сессии x N S S и роли r R AR выполняется условие r UA(user(x)) или r AUA(user(x)), то в графе доступов x соединена с r ребром вида (в), и помеченным UA или AUA, соответственно; если для доверенной субъект-сессии x L S S и роли r R AR выполняется условие r roles(x), то в графе доступов x соединена с r ребром вида (г), и помеченным roles; если для доверенной субъект-сессии x L S S и роли r R AR выполняется условие r roles(x), то в графе доступов x соединена с r ребром вида (г), и помеченным roles; если для административной роли ar AR и роли r R выполняется условие r can_manage_rights(ar), то в графе доступов ar соединена с r ребром вида (д), и помеченным cmr; если для административной роли ar AR и роли r R выполняется условие r can_manage_rights(ar), то в графе доступов ar соединена с r ребром вида (д), и помеченным cmr; если для субъект-сессий или недоверенных пользователей x, y N U S выполняется условие y island(x), то в графе доступов x соединен с y ребром вида (е), и помеченным island. если для субъект-сессий или недоверенных пользователей x, y N U S выполняется условие y island(x), то в графе доступов x соединен с y ребром вида (е), и помеченным island.

38 Случай без информационных потоков по памяти. Мосты Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором существуют недоверенная субъект-сессия или недоверенный пользователь x N U (N S S), субъект-сессии или недоверенные пользователи y, z N U S. Будем говорить, что субъект-сессия или недоверенный пользователь y соединен простым мостом с субъект- сессией или недоверенным пользователем z через недоверенную субъект-сессию или недоверенного пользователя x, когда z island(x) и существует роль r y R такая, что выполняются условия. Условие 1. Или y N U и r y UA(y), или y N S S и r y UA(user(y)), или y L S S и r y roles(y). Условие 2. Или z N U и r y can_manage_rights(AUA(z)), или z N S S и r y can_manage_rights(AUA(user(z))), или z L S S и r y can_manage_rights(roles(z) AR). Определение. Пусть G = (PA, user, roles, A, F, H E ) состояние системы (G*, OP), в котором существуют недоверенная субъект-сессия или недоверенный пользователь x N U (N S S), субъект-сессии или недоверенные пользователи y, z N U S. Будем говорить, что субъект-сессия или недоверенный пользователь y соединен мостом с субъект-сессией или недоверенным пользователем z через недоверенную субъект-сессию или недоверенного пользователя x, когда существуют субъект-сессии или недоверенные пользователи v, w N U S и роли r v, r y R такие, что v, w, z island(x), w, z island(v), z island(w), и выполняются условия. Условие 1. Или y N U и r y UA(y), или y N S S и r y UA(user(y)), или y L S S и r y roles(y). Условие 2. Или v N U и r v UA(v), r y can_manage_rights(AUA(v)), или v N S S и r v UA(user(v)), r y can_manage_rights(AUA(user(v))), или v L S S и r v roles(v), r y can_manage_rights(roles(v) AR). Условие 3. Или w N U и r v can_manage_rights(AUA(w)), или w S и (w, own r ) PA(r v ). is_simple_bridge: (N U (N S S)) × (N U S) × (N U S) {true, false} функция, для которой по определению справедливо равенство is_simple_bridge(x, y, z) = true тогда и только тогда, когда y соединен простым мостом с z через x, где недоверенная субъект-сессия или недоверенный пользователь x N U (N S S), субъект-сессии или недоверенные пользователи y, z N U S. is_bridge: (N U (N S S)) × (N U S) × (N U S) {true, false} функция, для которой по определению справедливо равенство is_bridge(x, y, z) = true тогда и только тогда, когда y соединен мостом с z через x, где недоверенная субъект-сессия или недоверенный пользователь x N U (N S S), субъект-сессии или недоверенные пользователи y, z N U S.

39 Случай без информационных потоков по памяти. Мосты Простой мост Мост

40 Случай без информационных потоков по памяти. Условия истинности получения доступа владения Теорема. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) состояние системы (G*, OP), в котором существуют недоверенный пользователь x N U и субъект-сессия или недоверенный пользователь y N U S 0 такие, что x y. Предикат simple_can_access_own(x, y, G 0 ) является истинным тогда и только тогда, когда существуют последовательности недоверенных субъект-сессий или недоверенных пользователей x 1, …, x m N U (N S S 0 ), субъект-сессий или недоверенных пользователей y 1, …, y m N U S 0, где m 1, таких, что x 1 = x, y m = y, y i island(x i ), где 1 i < m, и выполняются условия. Условие 1. Если m 2, то справедливо равенство is_bridge(x m, y m 1, y) = true. Условие 2. Если m 3, то для каждого 2 i < m справедливо равенство или is_bridge(x i, y i 1, y i ) = true, или is_simple_bridge(x i, y i 1, y i ) = true.

41 Фрагменты доказательств Фрагмент доказательства 1 Существуют сущность e y E 0 и роль r y R такие, что (e y, execute r ) PA 0 (UA 0 (y)), r y can_manage_rights(AUA 0 (y)). По условию утверждения (e, own r ) PA 0 (UA 0 (user 0 (x))), следовательно, существует роль r e UA 0 (user 0 (x)) такая, что (e, own r ) PA 0 (r e ). Тогда положим: op 1 = create_first_session(y, r y, e y, s y ); op 2 = take_role(x, r e ); op 3 = take_role(x, ar); op 4 = take_role(s y, r). op 5 = grant_right(x, r, (e, )). Таким образом, при выполнении условия 2 определения 6 G 0 op1 … op5 G 5 траектория без кооперации доверенных и недоверенных субъект-сессий для передачи прав доступа, и в состоянии G 5 выполняется условие user 5 (s y ) = y и право доступа к сущности (e, ) de_facto_rights 5 (s y ). Следовательно, истинен предикат can_share((e, ), y, G 0 ), и условие 1 утверждения выполнено. Фрагмент доказательства 2 Проведем доказательство индукцией по длине траекторий N. Пусть N = 0, тогда (e, ) de_facto_rights 0 (s x ). По определению функции de_facto_rights 0 (s x ) возможны два случая. Первый случай: право доступа (e, ) PA 0 (roles 0 (s x )) PA 0 (UA 0 (user 0 (s x ))). Положим y = x, s y = s x. Тогда истинен предикат directly_access_own(s x, s x, G 0 ), выполнено условие 2 определения 8, и предикат directly_can_share((e, ), x, G 0 ) является истинным. Второй случай: существует субъект-сессия s y S 0 такая, что (s x, s y, own a ) A 0, r e roles 0 (s y ), и (e, ) PA 0 (r e ) PA 0 (roles 0 (s y )) PA 0 (UA 0 (user 0 (s y ))). Тогда выполнено условие 4 определения 7, и предикат directly_access_own(s x, s y, G 0 ) является истинным. Положим y = user 0 (s y ), следовательно, выполнено условие 2 определения 8, и предикат directly_can_share((e, ), x, G 0 ) является истинным. Пусть N = 1, тогда из минимальности N следует, что выполняется условие (e, ) de_facto_rights 0 (s x ). По определению функции de_facto_rights 1 (s x ) возможны два случая…

42 Развитие ДП-моделей Разработка моделей адекватных условиям функционирования существующих компьютерных систем; Разработка моделей адекватных условиям функционирования существующих компьютерных систем; Построение ДП-моделей существующих компьютерных систем для формального анализа их безопасности; Построение ДП-моделей существующих компьютерных систем для формального анализа их безопасности; Анализ условий кооперации доверенных и недоверенных субъектов при реализации информационных потоков; Анализ условий кооперации доверенных и недоверенных субъектов при реализации информационных потоков; Построение алгоритмов замыкания графа доступов; Построение алгоритмов замыкания графа доступов; Анализ условий передачи прав доступа ролей для случая произвольного числа субъект-сессий, а также анализ условий возникновения информационных потоков по памяти или по времени; Анализ условий передачи прав доступа ролей для случая произвольного числа субъект-сессий, а также анализ условий возникновения информационных потоков по памяти или по времени; Исследование способов использования динамических ограничений; Исследование способов использования динамических ограничений; Исследование возможности реализации мандатного ролевого управления доступом с применением динамических ограничений, не позволяющих порождать запрещенные информационные потоки по времени. Исследование возможности реализации мандатного ролевого управления доступом с применением динамических ограничений, не позволяющих порождать запрещенные информационные потоки по времени.