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

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

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

3 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. Если сущность e H(c), то e < c и не существует сущности- контейнера d C, такой, что e < d, d < c. Условие 2. Для любых сущностей e 1, e 2 E, e 1 e 2, по определению выполняются равенство H(e 1 ) H(e 2 ) = и условия: если o O, то выполняется равенство H(o) = ; если o O, то выполняется равенство H(o) = ; если e 1 < e 2, то или e 1, e 2 E \ S, или e 1, e 2 S; если e 1 < e 2, то или e 1, e 2 E \ S, или e 1, e 2 S; если e E \ S, то H(e) E \ S; если e E \ S, то H(e) E \ S; если s S, то H(s) S. если s S, то H(s) S. 4

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* множество всех возможных состояний; G* множество всех возможных состояний; OP множество правил преобразования состояний. OP множество правил преобразования состояний. G op G переход системы (G*, OP) из состояния G в состояние G Определение системы а) б) в)г) r a write m write t r a write m write t 5

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 6

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

8 Условия реализации информационного потока по времени Теорема. Пусть G 0 = (S 0, E 0, R 0 A 0 F 0, H 0 ) состояние системы (G*, OP) и сущности x, y E 0, x y. Предикат can_write_time(x, y, G 0 ) истинен тогда, и только тогда, когда существует последовательность сущностей e 1, …, e m E 0, где e 1 = x, e m = y и m 2, таких, что выполняется одно из условий: Условие 1. m = 2 и (x, y, f ) F 0, где f {write m, write t }. Условие 2. Для каждого i = 1,..., m – 1 выполняется одно из условий: e i S 0 и (e i, e i + 1, write t ) F 0 ; e i S 0 и (e i, e i + 1, write t ) F 0 ; e i S 0 и истинен предикат can_write_memory(e i, e i + 1, G 0 ); e i S 0 и истинен предикат can_write_memory(e i, e i + 1, G 0 ); e i S 0 и существует сущность e i + 1 E 0, такая, что e i + 1 e i + 1 и истинен предикат can_share( r, e i, e i + 1, G 0 ), r R r ; e i S 0 и существует сущность e i + 1 E 0, такая, что e i + 1 e i + 1 и истинен предикат can_share( r, e i, e i + 1, G 0 ), r R r ; e i + 1 S 0 и истинен предикат can_share(read r, e i + 1, e i, G 0 ); e i + 1 S 0 и истинен предикат can_share(read r, e i + 1, e i, G 0 ); e i, e i + 1 S 0 и существуют сущности e i, e i + 1 E 0 : или e i e i + 1, или e i + 1 e i, и истинны предикаты can_share( r, e i, e i, G 0 ) и can_share( r, e i + 1, e i + 1, G 0 ), r, r R r. e i, e i + 1 S 0 и существуют сущности e i, e i + 1 E 0 : или e i e i + 1, или e i + 1 e i, и истинны предикаты can_share( r, e i, e i, G 0 ) и can_share( r, e i + 1, e i + 1, G 0 ), r, r R r. 8

9 Информационные потоки по времени x read a s x write t f e0 (x) write t read a z x write t B write a z y s y write a write m write t f e0 (y) y Пример доступов и информационных потоков в мандатной ДП-модели 9

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

11 ДП-модель с функционально и параметрически ассоциированными с субъектами сущностями (ФПАС ДП-модель, Колегов Д.Н.) 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[ 11

12 ДП-модель веб-системы (Назаров И.О.) 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 ) является истинным и возможно нарушение безопасности системы. 12

13 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 ) является истинным и возможно нарушение безопасности системы. ДП-модель веб-системы на основе СУБД (Назаров И.О.) 13

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

15 БР ДП-модель. Мосты Простой мост Мост 15

16 БР ДП-модель. Условия истинности получения доступа владения Теорема. Пусть 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. 16

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

18 18 РОСЛ ДП-модель. Предположения Предположение 1. В рамках РОСЛ ДП-модели пользователям соответствуют их учетные записи, для каждой из которых задаются множества авторизованных ролей. Каждая учетная запись пользователя вне зависимости от имеющихся у нее авторизованных ролей является учетной записью либо доверенного, либо недоверенного пользователя. Каждая субъект-сессия является либо доверенной, либо недоверенной, и функционирует от имени учетной записи доверенного или недоверенного пользователя, соответственно. Доверенные субъект-сессии не инициируют создание субъект-сессий. Каждая недоверенная субъект-сессия может создать недоверенную субъект-сессию. Предположение 2. Для каждой учетной записи пользователя задается множество сущностей, параметрически с ней ассоциированных, реализация от каждой из которых информационного потока по памяти к субъект-сессии позволяет ей создать субъект-сессию от имени данной учетной записи пользователя. Предположение 3. Функционально ассоциированными с субъект-сессией являются сущности, от которых зависит вид преобразования данных, реализуемого субъект-сессией. Только информационный поток по памяти к сущности, функционально ассоциированной с субъект- сессией, приводит к изменению вида преобразования данных, реализуемого этой субъект- сессией. Предположение 4. Параметрически ассоциированными сущностями с субъект-сессией являются сущности, которые содержат данные, позволяющие идентифицировать вид преобразования данных, реализуемого субъект-сессией. Предположение 5. Для каждой роли или административной роли задается множество сущностей, параметрически с ней ассоциированных. При этом для получения или удаления роли из множества текущих ролей субъект-сессии необходимо реализовать к себе информационные потоки по памяти от всех сущностей, параметрически ассоциированных с данной ролью.

19 19 Основные элементы E = O C множество сущностей, где O множество объектов, C множество контейнеров; U 2 E множество учетных записей пользователей; ]u[ E \ S множество сущностей, параметрически ассоциированных с учетной записью пользователя u U; UE = {e ]u[: u U} множество сущностей, каждая из которых параметрически ассоциирована хотя бы с одной учетной записью пользователя; L U множество учетных записей доверенных пользователей; N U множество учетных записей недоверенных пользователей; S E множество субъект-сессий учетных записей пользователей; L S S множество доверенных субъект-сессий; N S = S \ L S множество недоверенных субъект-сессий; R множество ролей; AR множество административных ролей (AR R = ); ]r[ E \ S множество сущностей-параметров роли или административной роли r R AR; RE = {e ]r[: r R AR} множество сущностей-параметров ролей; 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 } множество видов информационных потоков;

20 20 Основные элементы P E R r множество прав доступа к сущностям; A S E R a множество доступов субъект-сессий к сущностям; F E E R f множество информационных потоков; UA: U 2 R функция авторизованных ролей учетных записей пользователей; AUA: U 2 AR функция авторизованных административных ролей учетных записей пользователей; PA: R 2 P \ { } функция прав доступа ролей; user: S U функция принадлежности субъект-сессии учетной записи пользователя; roles: S 2 R 2 AR функция текущих ролей субъект-сессий; can_manage_rights: AR 2 R функция администрирования прав доступа ролей; [s] E U множество всех сущностей, функционально ассоциированных с субъект-сессией s; fa: U E 2 E 2 U ­ функция, задающая множества сущностей, функционально ассоциированных с субъект-сессией при ее создании от имени учетной записи пользователя; ]s[ E \ S множество сущностей, параметрически ассоциированных с субъект-сессией; fp: U E 2 E ­ функция, задающая множества сущностей, параметрически ассоциированных с субъект-сессией при ее создании из сущности от имени учетной записи пользователя; H R : R 2 R функция иерархии ролей; H AR : AR 2 AR функция иерархии административных ролей.

21 21 Иерархия сущностей и механизм ограничений H E : E 2 E функцию иерархии сущностей (сопоставляющую каждой сущности e E множество сущностей H E (e) E, непосредственно в ней содержащихся), удовлетворяющую условиям: Условие 1. Если сущность e H E (c), то e < c, при этом, если e C E, то не существует сущности- контейнера d C такой, что e < d, d < c. Условие 2. Для любых сущностей e 1, e 2 E, e 1 e 2, по определению выполняются равенство H E (e 1 ) H E (e 2 ) (C E) = и условия: если o O, то справедливо равенство H E (o) = ; если o O, то справедливо равенство H E (o) = ; если e 1 < e 2, то или e 1, e 2 E \ S, или e 1, e 2 S; если e 1 < e 2, то или e 1, e 2 E \ S, или e 1, e 2 S; если e E \ S, то H E (e) E \ S; если e E \ S, то H E (e) E \ S; если s S, то H E (s) S. если s S, то H E (s) S. C U : UA* {true, false} функция, задающая ограничение на значения множеств авторизованных ролей учетных записей пользователей, то есть по определению множества авторизованных ролей учетных записей пользователей, заданные функцией UA UA*, удовлетворяют ограничению C U, если выполняется равенство C U (UA) = true; C P : PA* {true, false} функция, задающая ограничение на значения множеств прав доступа ролей, то есть по определению множества прав доступа ролей, заданные функцией PA PA*, удовлетворяют ограничению C P, если выполняется равенство C P (PA) = true; C S : roles* {true, false} функция, задающая ограничение на значения множеств текущих ролей субъект-сессий, то есть по определению множества текущих ролей субъект-сессий, заданные функцией roles roles*, удовлетворяют ограничению C S, если выполняется равенство C S (roles) = true.

22 22 Мандатный контроль целостности (LI, ) линейная шкала двух уровней целостности данных, где LI = {i_low, i_high}, i_low < i_high; (i u, i e, i r, i s ) I четверка функций уровней целостности, при этом: i u : U LI функция уровней целостности субъект-сессий; i e : E \ S LI функция уровней целостности сущностей; i r : R AR LI функция уровней целостности ролей; i s : S LI функция текущих уровней целостности субъект-сессий; I множества всех четверок функций заданного вида; По предположениям выполняются условия: для ролей r, r R AR, если r r, то i r (r) i r (r); для ролей r, r R AR, если r r, то i r (r) i r (r); для сущностей e, e E \ S, если e e, то i e (e) i e (e); для сущностей e, e E \ S, если e e, то i e (e) i e (e); для субъект-сессий s, s S, если s s, то i s (s) i s (s); для субъект-сессий s, s S, если s s, то i s (s) i s (s); для каждой сущности e u, где u U, справедливо равенство i e (e) = i u (u); для каждой сущности e u, где u U, справедливо равенство i e (e) = i u (u); для субъект-сессии s S верно неравенство i s (s) i u (user(s)); для субъект-сессии s S верно неравенство i s (s) i u (user(s)); для учетной записи пользователя u U и роли r R, если r UA(u), то i r (r) i u (u); для учетной записи пользователя u U и роли r R, если r UA(u), то i r (r) i u (u); для субъект-сессии s S и роли r R, если r roles(s), то i r (r) i s (s); для субъект-сессии s S и роли r R, если r roles(s), то i r (r) i s (s); для права доступа к сущности (e, ) P, где {own r, write r, append r }, и роли r R, если (e, ) PA(r), то i e (e) i r (r); для права доступа к сущности (e, ) P, где {own r, write r, append r }, и роли r R, если (e, ) PA(r), то i e (e) i r (r); для учетной записи доверенного пользователя u L U справедливо равенство i u (u) = i_high; для учетной записи доверенного пользователя u L U справедливо равенство i u (u) = i_high; для учетной записи недоверенного пользователя u N U справедливо равенство i u (u) = i_low; для учетной записи недоверенного пользователя u N U справедливо равенство i u (u) = i_low; верно равенство i e (i_entity) = i_high. верно равенство i e (i_entity) = i_high.

23 23 Фактические роли, права доступа, доступы, возможные действия Предположение 6. Если субъект-сессия s реализовала информационный поток по памяти от себя к сущности, функционально ассоциированной с другой субъект-сессией s, или субъект-сессия s реализовала информационный поток по памяти к себе от всех сущностей, параметрически ассоциированных с другой субъект-сессией s, то субъект-сессия s получает доступ владения own a к субъект-сессии s. Предположение 7. Если субъект-сессия s имеет доступ владения own a к субъект-сессии s, то субъект-сессия s получает: возможность использовать роли из множества текущих ролей субъект-сессии s; возможность использовать роли из множества текущих ролей субъект-сессии s; возможность изменять множество текущих ролей субъект-сессии s; возможность изменять множество текущих ролей субъект-сессии s; возможность использовать текущий уровень целостности субъект-сессии s; возможность использовать текущий уровень целостности субъект-сессии s; возможность использовать доступы субъект-сессии s возможность использовать доступы субъект-сессии s; возможность получать доступ владения own a к субъект-сессиям, доступом владения к которым обладает субъект-сессия s; возможность получать доступ владения own a к субъект-сессиям, доступом владения к которым обладает субъект-сессия s; возможность использовать административные роли субъект-сессии s; возможность использовать административные роли субъект-сессии s; возможность использовать информационные потоки, которые реализует субъект-сессия s. возможность использовать информационные потоки, которые реализует субъект-сессия s. Используем обозначения: de_facto_roles: S 2 R AR фактические текущие роли субъект-сессий; de_facto_roles: S 2 R AR фактические текущие роли субъект-сессий; de_facto_rights: S 2 P фактические текущие права доступа субъект-сессий; de_facto_rights: S 2 P фактические текущие права доступа субъект-сессий; de_facto_accesses: S 2 A фактические доступы субъект-сессий; de_facto_accesses: S 2 A фактические доступы субъект-сессий; de_facto_actions: S S U 2 P 2 R фактические возможные действия субъект-сессий. de_facto_actions: S S U 2 P 2 R фактические возможные действия субъект-сессий.

24 24 Правила преобразования состояний G = (UA, AUA, PA, user, roles, (i u, i e, i r, i s ), A, F, H R, H AR, H E, Constraint U, Constraint P, Constraint S, L U, L S ) состояние системы (G = (PA, user, roles, A, F, H E ) сокращенное обозначение); (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. Определение. Монотонное правило преобразования состояний правило преобразования состояний из множества OP, применение которого не приводит к удалению из состояний: ролей из множества текущих ролей субъект-сессии; ролей из множества текущих ролей субъект-сессии; прав доступа ролей к сущностям; прав доступа ролей к сущностям; субъект-сессий, сущностей или «жестких» ссылок на сущности-объекты; субъект-сессий, сущностей или «жестких» ссылок на сущности-объекты; доступов субъект-сессий к сущностям; доступов субъект-сессий к сущностям; информационных потоков. информационных потоков. Монотонные правила: take_roles(x, x, w, {r j : 1 j k}), grant_rights(x, x, r, {(y j, rj ): 1 j k}), create_object(x, x, r, y, yi, z), create_container(x, x, r, y, yi, z), create_hard_link(x, x, y, z), rename_entity(x, x, y, z), create_first_session(x, x, u, r, y, z, zi), create_session(x, x, w, r, y, z, zi), control(x, y, z), know(x, y), take_access_own(x, y, z), access_own(x, x, w, y), access_read(x, w, y), access_write(x, x, w, y), flow_access(x, y), flow(x, y, y, z), find(x, y, z), post(x, y, z), pass(x, y, z) и take_flow(x, y). Немонотонные правила: remove_roles(x, x, w, {r j : 1 j k}), remove_rights(x, x, r, {(y j, rj ): 1 j k}), delete_entity(x, x, y, z), delete_hard_link (x, x, y, z), delete_session(x, x, w, z), delete_access(x, x, w, y, a ).

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

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

27 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), know(x, y) Уровни целостности (I) = (i u, i e, i r, i s ) de_facto_actions Ограничения (Constraint) Информационные потоки по памяти i_entity

28 28 Инвариантные относительно немонотонных правил ограничения Определение. Ограничение инвариантно относительно немонотонных правил преобразования состояний в системе (G*, OP), когда при условии, что в системе задано только данное ограничение, для любых состояния системы G 0, немонотонного правила преобразования состояний op 1, правил преобразования состояний op 2, …, op N, где N > 1, справедливо следующие: если G 0 op1 G 1 op2 … op(N – 1) G N – 1, G 0 op2 G 2 op3 … op(N – 1) G N – 2, и в состоянии G N – 1 выполнены ограничения, заданные в условиях применения правила op N, то эти ограничения выполнены в состоянии G N – 2. Ограничения, заданные в системе (G*, OP), по определению инвариантны относительно немонотонных правил преобразования состояний, когда каждое из ограничений в отдельности инвариантно относительно немонотонных правил преобразования состояний. Утверждение. Пусть G 0 = (PA 0, user 0, roles 0, A 0, F 0, H E0 ) начальное состояние системы (G*, OP, G 0 ), в котором все ограничения инвариантны относительно немонотонных правил преобразования состояний и функции (i u, i e, i r, i s ) 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. Тогда существуют состояния G 1, …, G M = (PA M, user M, roles M, A M, F M, H EM ), где 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 \ S N, не являющейся субъектом, выполняется условие H EN (e) H EM (e), и для любых сущностей e, e E N, если в состоянии G N выполняется условие e < e, то данное условие выполняется в состоянии G M. Условие 3. Для каждой роли r R выполняется условие PA N (r) PA M (r). Условие 4. Верно включение A N A M. Условие 5. Верно включение F N F M. Условие 6. Функции (i u, i e, i r, i s ) M удовлетворяют условиям предположений.

29 29 Фрагмент доказательства Пусть N > 0 и условия утверждения выполнены для всех последовательностей состояний длины 0 L 0 и условия утверждения выполнены для всех последовательностей состояний длины 0 L < N. Докажем, что условия 1-5 утверждения выполнены для последовательностей состояний длины N. По предположению индукции для последовательности состояний G 0, G 1, …, G N – 1 существует последовательность состояний G 0, G 1, …, G K = (PA K, user K, roles K, A K, F K, H EK ), где K 0, и для состояний G N – 1 и G K выполнены условия 1-5 утверждения. Рассмотрим правило преобразования состояний op N. Если условия его применения не выполняются в состоянии G N – 1, то по определению правил преобразования состояний справедливо равенство G N – 1 = G N. Положим M = K и для состояний G N и G M выполнены условия 1-5 утверждения. Пусть условия применения правила op N выполняются в состоянии G N – 1, тогда возможны два случая. Первый случай: правило преобразования состояний op N является немонотонным. Пусть op N = remove_roles(x, x, w, {r j : 1 j l}). Так как для состояний G N – 1 и G K выполнены условия 1-5 утверждения, то в случае, когда x LF S S N – 1 положим M = K, и условия 1-5 утверждения выполняются для состояний G N и G K. Пусть x (N S NF S ) S N – 1, тогда в результате применения правила возникают информационные потоки по времени из множества {(x, s, write t ): s (N S NF S ) S N – 1, x s и или s = w, или (w, own a ) de_facto_accesses N – 1 (s)}. Так как для состояний G N – 1 и G K выполнены условия 1-5 утверждения, то выполняются условия (w, user K (w),, ) de_facto_actions K (x) и для s S N – 1 S K справедливо de_facto_accesses N – 1 (s) de_facto_accesses K (s). Следовательно, справедливо либо x = w, либо (w, own a ) de_facto_accesses K (x). Положим M = K + |{(x, s, write t ): s (N S NF S ) S N – 1, x s и или s = w, или (w, own a ) de_facto_accesses N – 1 (s)}|, и последовательно для каждой субъект-сессии s i (N S NF S ) S N – 1 такой, что x s i и или s i = w, или (w, own a ) de_facto_accesses N – 1 (s i ), положим op i = flow(x, w, w, s i ), где K < i M. Пусть состояние G M получено из состояния G K в результате применения последовательности правил op K + 1, …, op M : G K op(K + 1) … opM G M. Таким образом, для состояний G N и G M выполнены условия 1-5 утверждения.

30 30 ЗОС ДП-модель (Проскурин В.Г.). Основные элементы E = O C множество сущностей, где O множество объектов, C множество контейнеров; U множество учетных записей пользователей; ]u[ E \ S множество сущностей, параметрически ассоциированных с учетной записью пользователя u U; L U множество учетных записей доверенных пользователей; N U множество учетных записей недоверенных пользователей; S E множество субъектов, функционирующих от имени учетных записей пользователей; L S множество доверенных субъектов; N S множество недоверенных субъектов; R r = {read r, write r, execute r, own r, grant r } множество видов прав доступа; R a = {read a, write a, own a } множество видов доступа; R f = {write m, write t } множество видов информационных потоков; R U (E U) R r множество прав доступа учетных записей пользователей к сущностям или учетным записям; Share = {read a, write a } R a множество видов совместных доступов к сущностям; A S E R a 2 Share множество доступов субъектов к сущностям; sa: E \ S 2 Share функция, задающая текущие доступы из множества Share к сущностям; sm: E \ S 2 Share функция, задающая разрешенные совместные доступы из множества Share к сущностям

31 31 Основные элементы. Уровни целостности F E E R f множество информационных потоков; ](e, r)[ E \ S множество сущностей-параметров права доступа r R r к сущности e E; user: S U функция принадлежности субъекта учетной записи пользователя; [s] E U множество сущностей, функционально ассоциированных с субъектом s; fa: U E 2 E 2 U ­ функция сущностей, функционально ассоциированных с субъектом при его создании от имени учетной записи пользователя из сущности; ]s[ E \ S множество сущностей, параметрически ассоциированных с субъектом s S; fp: U E 2 E ­ функция сущностей, параметрически ассоциированных с субъектом при его создании из сущности от имени учетной записи пользователя; H E : E 2 E функция иерархии сущностей; (LI, ) линейная шкала двух уровней целостности данных, где LI = {i_low, i_high}, i_low < i_high; i u : U LI функция уровней целостности учетных записей пользователей; i e : E \ S LI функция уровней целостности сущностей; i s : S LI функция уровней целостности субъектов; G = (U, S, E, user, (i u, i e, i s ), R, A, F, H E, L U, L S ) состояние системы; G = (S, E, user, R, A, F, H E ) сокращенное обозначение для состояния системы; (G*, OP) система, при этом G* множество всех возможных состояний, OP множество правил преобразования состояний, G op G переход системы из состояния G в состояние G с использованием правила преобразования состояний; (G*, OP) система, при этом G* множество всех возможных состояний, OP множество правил преобразования состояний, G op G переход системы из состояния G в состояние G с использованием правила преобразования состояний;

32 32 Требования к управлению доступом и мандатному контролю целостности Требования к распределению прав доступа и получению доступов: для учетных записей пользователей u, u U, если (u, u, r ) R, то r {own r, grant r }; для учетных записей пользователей u, u U, если (u, u, r ) R, то r {own r, grant r }; для учетной записи пользователя u U и субъекта s S, если (u, s, r ) R, то r = own r ; для учетной записи пользователя u U и субъекта s S, если (u, s, r ) R, то r = own r ; для субъектов s, s S, если (s, s, a, ) A, то a = own a, = ; для субъектов s, s S, если (s, s, a, ) A, то a = own a, = ; для учетной записи пользователя u U и сущности e E \ S, если (u, e, r ) R, то r {read r, write r, execute r, own r }. для учетной записи пользователя u U и сущности e E \ S, если (u, e, r ) R, то r {read r, write r, execute r, own r }. Требования к мандатному контролю целостности: для сущностей e, e E \ S, если e e, то i e (e) i e (e); для сущностей e, e E \ S, если e e, то i e (e) i e (e); для субъектов s, s S, если s s, то i s (s) i s (s); для субъектов s, s S, если s s, то i s (s) i s (s); для каждой сущности e ]u[, где u U, справедливо равенство i e (e) = i u (u); для каждой сущности e ]u[, где u U, справедливо равенство i e (e) = i u (u); для субъекта s S верно неравенство i s (s) i u (user(s)); для субъекта s S верно неравенство i s (s) i u (user(s)); для учетной записи доверенного пользователя u L U выполняется i u (u) = i_high; для учетной записи доверенного пользователя u L U выполняется i u (u) = i_high; для учетной записи недоверенного пользователя u N U выполняется i u (u) = i_low; для учетной записи недоверенного пользователя u N U выполняется i u (u) = i_low; верно равенство i e (i_entity) = i_high. верно равенство i e (i_entity) = i_high.

33 33 Контроль над субъектами Если субъект s реализовал информационный поток по памяти от себя к сущности, функционально ассоциированной с субъектом s, или реализовал информационный поток по памяти к себе от всех сущностей, параметрически ассоциированных с субъектом s, то субъект s получает доступ владения own a к субъекту s. Кроме того, субъект s получает: возможность использовать права доступа учетной записи пользователя субъекта s; возможность использовать права доступа учетной записи пользователя субъекта s; возможность изменять множество прав доступа учетной записи пользователя субъекта s; возможность изменять множество прав доступа учетной записи пользователя субъекта s; возможность использовать текущий уровень целостности субъекта s; возможность использовать текущий уровень целостности субъекта s; возможность использовать доступы субъекта s; возможность использовать доступы субъекта s; возможность получать доступ владения own a к субъектам, доступом владения к которым обладает субъект s; возможность получать доступ владения own a к субъектам, доступом владения к которым обладает субъект s; возможность использовать информационные потоки, в реализации которых участвует субъект s. возможность использовать информационные потоки, в реализации которых участвует субъект s. de_facto_rights: S 2 E Rr функция фактических текущих прав доступа субъектов, при этом по определению в каждом состоянии системы G = (S, E, user, R, A, F, H E ) для каждого субъекта s S по определению верно равенство: de_facto_rights(s) = {(e, r) E R r : (user(s), e, r) R} {(e, r) E R r : существует s S такой, что (s, s, own a, ) A и (user(s), e, r) R}; de_facto_accesses: S 2 A функция фактических доступов субъектов, при этом по определению в каждом состоянии системы G = (S, E, user, R, A, F, H E ) для каждого субъекта s S по определению верно равенство: de_facto_accesses(s) = {(s, e, a, ): (s, e, a, ) A} {(s, e, a, ): (s, s, own a, ), (s, e, a, ) A}.

34 34 Правила преобразования состояний Определение. Монотонное правило преобразования состояний правило преобразования состояний из множества OP, применение которого не приводит к удалению из состояний: прав доступа учетных записей пользователей к субъектам или к сущностям; прав доступа учетных записей пользователей к субъектам или к сущностям; субъектов или сущностей; субъектов или сущностей; доступов субъектов к сущностям; доступов субъектов к сущностям; информационных потоков. информационных потоков. Монотонные правила: grant_right( r, x, u, w, z), own_take( r, x, w, z), create_entity(x, w, y, z, zi), rename_entity(x, w, y, z), create_first_subject(x, u, w, y, z, zi), create_subject(x, w, y, z, zi), control(x, y, z), know(x, y), take_access_own(x, y, z), access_own(x, w, y), access_read(x, w, y, ), access_write(x, w, y, ), flow(x, y, y, z), find(x, y, z), post(x, y, z), pass(x, y, z), take_flow(x, y). Немонотонные правила: remove_right( r, x, u, w, z), delete_entity(x, w, y, z), delete_subject(x, w, z), delete_access(x, w, y, a ).

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

36 36 Зависимость условий и результатов правил Учетные записи пользователей (U) Субъекты (S) Права доступа к сущностям (R) Доступы own a к субъектам Доступы к сущностям Информационные потоки по памяти Информационные потоки по времени Уровни целостности (i u, i e, i s ) Параметры совместного доступа сущностям user A F

37 37 Развитие ДП-моделей операционных систем Построение ДП-моделей существующих или перспективных компьютерных систем (особенно операционных систем семейства Linux) для формального анализа их безопасности; Построение ДП-моделей существующих или перспективных компьютерных систем (особенно операционных систем семейства Linux) для формального анализа их безопасности; Макетирование ролевого управления доступом на основе ОС AltLinux и корректировка формальных моделей; Макетирование ролевого управления доступом на основе ОС AltLinux и корректировка формальных моделей; Исследование возможности реализации мандатного ролевого управления доступом с использованием динамических ограничений, в том числе, не позволяющих порождать запрещенные информационные потоки по времени, применительно к защищенным операционным системам; Исследование возможности реализации мандатного ролевого управления доступом с использованием динамических ограничений, в том числе, не позволяющих порождать запрещенные информационные потоки по времени, применительно к защищенным операционным системам; Разработка алгоритма построения замыкания графа прав доступа, доступов и информационных потоков для проверки корректности теоретических результатов. Разработка алгоритма построения замыкания графа прав доступа, доступов и информационных потоков для проверки корректности теоретических результатов.

38 Литература по теме доклада 1.Bishop M. Computer Security: art and science. ISBN , p. 2.Девянин П.H. Модели безопасности компьютерных систем. Управление доступом и информационными потоками. Учебное пособие для вузов. М.: Горячая линия Телеком, с. 3.Прикладная дискретная математика. Томск: ТГУ. 38