Модель типизированных матриц доступа

Модель типизированной матрицы доступов

Другая дискреционная модель, получившая название Типизирован­ная матрица доступов (ТМД), представляет собой развитие моделиХРУ, дополненной концеп­цией типов, что позволяет несколько смягчить те условия, для которых возможно доказательство безопасности системы. Будем рассматривать модель ТМД на основе.

Формальное описание модели ТМД включает в себя следующие элементы:

O ¾ множество объектов системы;

S ¾ множество субъектов системы (S Í O);

R ¾ множество прав доступа субъектов к объектам;

M ¾ матрица доступов;

C ¾ множество команд;

Т ¾ множество типов объектов;

t: О ® Т ¾ функция, ставящая в соответствие каждому объекту его тип;

Q­ ¾ множество состояний системы.

Состояния системы изменяются в результате применения к ним команд из множества C. Команды в модели ТМД имеют тот же формат, что и в модели ХРУ, при этом для всех параметров команд указывается их тип:

Перед выполнением команды происходит проверка типов фактических параметров, и, если они не совпадают с указанными в определении команды, то команда не выполняется. В модели ТМД используются следующие шесть видов примитивных операторов, отличающихся от аналогичных операторов модели ХРУтолько использованием типизированных параметров (табл. 4.2).

Таблица 4.2. Примитивные операторы модели ТМД

Примитивный оператор	Исходное состояние q = (S, O, t, M)	Результирующее состояние q’ = (S’, O’, t’, M’)
«внести» право r в M[s, o]	sÎ S, o Î O, r Î R	S’ = S, O’ = O, t’(o) = t(o) для oÎ O, M’[s, o] = M[s, o] È <r>, для (s’, o’) ¹ (s, o) выполняется равенство M’[s’, o’] = M[s’, o’]
«удалить» право r из M[s, o]	s Î S, o Î O, r Î R	S’ = S, O’ = O, t’(o) = t(o) для oÎ O, M’[s, o] = M[s, o] <r>, для (s’, o’) ¹ (s, o) выполняется равенство M’[s’, o’] = M[s’, o’]
«создать» субъекта s’ с типом ts	s’Ï S	S’ = S È <s’>, O’ = O È <s’>, для oÎ O выполняется равенство t’(o) = t(o), t’(s’) = ts, для (s, o) Î S ´ O выполняется равенство M’[s, o] = M[s, o], для o Î O’выполняется равенство M’[s’, o] = Æ, для s Î S’выполняется равенство M’[s, s’] = Æ
«создать» объект o’ с типом to	o’Ï O	S’ = S, O’ = O È <o’>, t’(o’) = to, для (s, o) Î S ´ O выполняется равенство M’[s, o] = M[s, o], для s Î S’выполняется равенство M’[s, o’] = Æ
«уничтожить» субъекта s’	s’Î S	S’ = S <s’>, O’ = O <s’>,для o Î O’ выполняется равенство t’(o) = t(o), для (s, o) Î S’´ O’выполняется равенство M’[s, o] = M[s, o]
«уничтожить» объект o’	o’Î O, o’Ï S	S’ = S, O’ = O <o’>,для o Î O’ выполняется равенство t’(o) = t(o), для (s, o) Î S’´ O’выполняется равенство M’[s, o] = M[s, o]

Таким образом, ТМД является обобщением модели ХРУ, которую можно рассматривать как частный случай ТМД с одним единственным типом для всех объектов и субъек­тов. С другой стороны любую систему ТМД можно выразить через систему ХРУ, введя для обозначения типов специальные права доступа, а проверку типов в командах заменив проверкой наличия соответствующих прав доступа.

Определение 4.5.Пусть c(x₁: t₁, …, x_k: t_k) — некоторая команда ТМД. Будем говорить, что x_i является дочерним параметром, а t_i является дочерним типом в c(x₁: t₁, …, x_k: t_k), если в нейимеется один из следующих примитивных операторов:

В противном случае будем говорить, что x_i является родительским параметром, а t_i является родительским типом в команде c(x₁: t₁, …, x_k: t_k).

Заметим, что в одной команде тип может быть одновременно и ро­дительским, и дочерним. Например:

Здесь u является родительским типом относительно s₁и дочерним типом относительно s₂. Кроме того, w и b являются родительскими типа­ми, а v ¾ дочерним типом.

Появление в каждой команде дополнительных неявных условий, ограничивающих область применения команды только объектами соответствующих типов, позволяет несколько смягчить жесткие условия клас­сической модели, при которых критерий безопасности является разрешимым.

Определение 4.6. Система монотонной ТМД (МТМД) ¾ система ТМД, в командах которой отсутствуют немонотон­ные примитивные операторы вида «удалить»… и «уничтожить»….

Определение 4.7. Каноническая форма системы МТМД (КФМТМД) ¾ система МТМД, в которой команды, содержащие примитивные операторы вида «создать»…, не содержат условий и примитивных операторов вида «внести»….

Терема 4.3. Для каждой системы МТМД существует эквивалентная ей система КФМТМД.

Доказательство. Пусть задана система МТМД, в которой определены множества R, T, Q, C. Построим эквивалентную ей систему КФМТМД, определив множества R*, T*, Q*, C*.

В каждом состоянии q* = (S*, O*, t*, M*), соответствующем состоянию q = (S, O, t, M), справедливы равенства:

Пусть также для каждого o Î O справедливо равентсво t*(o) = t(o) и s_active ¾ единственный субъект такой, что t*(s_active) = t_active. Кроме того, для s Î S, o Î O справедливо равенство M*[s, o] = M[s, o], и в начальном состоянии системы для o Î O₀ справедливо равенство M₀*[s_active, o] = <active>.

Таким образом, право доступа active обозначает активизированные субъекты и объекты КФМТМД.

Каждую команду c(x₁: t₁, …, x_k: t_k) системы МТМД, содержащую примитивные операторы «создать»…, представим монотонными командами КФМТМД:

— c’_xi(x_j1: t_j1, …, x_jk: t_jk) ¾ команды без проверки условий, каждая их которых соответствует одному дочернему параметру x_i команды c(x₁: t₁, …, x_k: t_k), содержит все ее родительские параметры и параметр x_i и содержит соответствующий примитивный оператор вида «создать»…;

Таким образом, только «активизированные» объекты (в том числе и субъекты) системы КФМТМД соответствуют объектам системы МТМД, а все преобразования над ними в системе КФМТМД соответствуют преобразованиям системы МТМД. Теорема доказана. ■

Для того чтобы сформулировать ограничения достаточные для алгоритмической разрешимости задачи проверки безопасности в системах МТМД опишем взаимосвязи между различными типами с помощью графа, определяющего отношение «на­следственности» между типами, устанавливаемые через команды порож­дения объектов и субъектов.

Определение 4.8. Граф создания системы МТМД ¾ ориентированный граф с множеством вершин T, в котором ребро от вершины u к вершине v существует тогда и только тогда, когда в сис­теме имеется команда, в которой u является родительским типом, а v ¾ дочерним типом.

Граф создания для каждого типа позволяет опре­делить:

— объекты, каких типов должны существовать в системе, чтобы в ней мог появиться объект или субъект заданного типа;

— объекты, каких типов могут быть порождены при участии объектов заданного типа.

Определение 4.9. Система МТМД (КФМТМД) называется ацикличе­ской (АМТМД или, соответственно, АКФМТМД) тогда и только тогда, когда ее граф создания не содержит циклов; в противном случае говорят, что система является циклической.

Например, граф создания для приведенной выше команды foo, содержит следующие реб­ра: <(u, u), (u, v), (w, u), (w, v), (b, u), (b, v)>. Система МТМД, содер­жащая эту команду, будет циклической, поскольку тип u является для нее одновременно и родительским, и дочерним, что приводит к появлению в графе цикла (u, u).

Алгоритм проверки безопасности систем АМТМД будет строиться для эквивалентных им систем АКФМТМД. Он состоит из трех шагов.

Алгоритм 4.1. Алгоритм проверки безопасности системы АМТМД.

Шаг 1. Для системы АМТМД построить эквивалентную ей систему АКФМТМД.

Шаг 2. Используя команды, содержащие только примитивные операторы «создать»… и не содержащие условий, перейти из начального состояния системы в некоторое «развернутое» состояние, обеспечивающее минимально необходимый и достаточный для распространения прав доступа состав объектов.

Шаг 3. Используя команды, не содержащие примитивные операторы «создать»…, перейти из развернутого состояния в «замкнутое» состояние, в котором дальнейшее применение таких команд не приводит к изменениям в матрице доступов.

Третий шаг алгоритма, очевидно, всегда будет иметь конечную сложность. Так как множество объектов не изменяется, то необходимо перебрать все последовательности различных команд (по аналогии с доказательством теоремы 1.1), а их конечное число.

Наибольшую трудность в общем случае представляет разработка алгоритма построения «развернутого» состояния. Однако для АМТМД или АКФМТМД такой алгоритм существует. Перед его рассмотрением дадим определение.

Определение 4.10. Пусть a и b ¾ две различные команды системы МТМД, содержащие примитивные операторы «создать»…. Будем считать, что a g _i, O g _i, t g _i, M g _i), где i ³ 0, существует объект o ( i ) Î O g _i такой, что p(o ( i ) ) Ï P_l. Если объект o ( i ) Î O₀, то выполняется условие p(o ( i ) ) = o ( i ) Î P_l, противоречие. Следовательно, существуют 0 £ k ( i ) создается командой a. При этом объекты o₁, o₂, …, o_m Î O g _k последовательность входящих в команду a параметров-объектов родительских типов, и по определению 1.11 выполняется равенство p(o ( i ) ) = a(p(o₁), p(o₂), …, p(o_m)).

Команда aсодержится в списке, созданном при выполнении шага 1 алгоритма 1.2. Пусть q_n ¾ состояние, к которому при выполнении алгоритма 1.2 впервые применена команда a, где 0 £ n £ l. Так как p(o ( i ) ) Ï P_l, то, как минимум, для одного из значений p(o₁), p(o₂), …, p(o_m) в состоянии q_n должен отсуствовать соответсвующий ему объект. Пусть объект o ( k ) Î <o₁, o₂, …, o_m> и выполнятся условие p(o ( k ) ) Ï P_n. По определению алгоритма 1.2 выполняется условие p(o ( k ) ) Ï P_l.

Многократно повторяя руссуждения, получим, что существует объект o (0) Î O₀ такой, что выполняется условие p(o (0) ) = o (0) Ï P_l, противоречие. Следовательно, в «развернутом» состоянии q_l для каждого возможного значения функции p существует соответствующий объект.

Так как на шаге 2 алгоритма 1.2 при применении каждой команды создается один объект с новым значением функции p, то в «развернутом» состоянии q_l для каждого возможного значения функции p существует ровно один соответствующий объект.

Теорема 4.4.Существует алгоритм проверки безопасности систем АМТМД.

Доказательство. Без ограничения общности по теореме 1.3 будем рассматривать системы АКФМТМД.

Пусть f ¾ начальное состояние системы, q ¾ «развернутое» состояние, полученное из f по алгоритму 1.1, m ¾ «замкнутое» состояние, полученное из q, используя все команды, не содержащие примитивные операторы «создать»…, при этом дальнейшее применение таких команд в m не приводит к изменениям в матрице доступов.

Покажем, что для систем АКФМТМД для любой истории (f, …, h, …) может быть найдена история (q, …, g, …) без команд, содержащих примитивные операторы вида «создать»…, где для (s, o) Î S_h ´ O_h выполняется условие

Заметим, что по лемме 1.3 в «развернутом» состоянии q каждому возможному значению функции p соответствует ровно один объект.

Если (1.2) выполняется, то из (1.1) и (1.2) следует, что для (s, o) Î S_f ´ O_f выполняется условие

что означает алгоритмическую разрешимость задачи проверки безопасности систем АКФМТМД и, следовательно, систем АМТМД. Например, для начального состояния f заменяем p(s) на s, p(o) на o и получаем, что для (s, o) Î S_f ´ O_f выполняется условие

Обоснуем (1.2), для чего построим алгоритм преобразования последовательности команд истории (f, …, h, …) в последовательность команд истории (q, …, g, …), который состоит из двух шагов.

Шаг 1. В командах истории (f, …, h, …) удалить примитивные операторы вида «создать»….

По индукции по длине истории (f, …, h, …) легко показать, что выполняются два условия.

Условие 1. Для каждой команды истории (f, …, h, …), если истинно ее условие, то истинно условие соответствующей ей команды истории (q, …, g, …).

Условие 2. Для состояния h истории (f, …, h, …) и соответствующего ему состояния g истории (q, …, g, …) верно, что для (s, o) Î S_h ´ O_h выполняется условие

Таким образом, (1.2) обосновано. Теорема доказана. ■

Следствие 4.2. Алгоритм проверки безопасности систем АМТМД имеет экспоненциальную сложность.

Доказательство. При построении «замкнутого» состояния из «развернутого» состояния используется алгоритм, аналогичный алгоритму, использованному в теореме 1.1. По следствию 1.1, получаем, что алгоритм проверки безопасности систем АМТМД имеет экспоненциальную сложность. ■

Определим подмножество АМТМД, называемое тернарными АМТМД.

Определение 4.12. Тернарными называются АМТМД, в которых каждая команда имеет не более трех параметров.

Для тернарной АМТМД в доказано, что алгоритм проверки ее безопасности имеет полиномиальную сложность.

Таким образом, введение строгого контроля типов в дискреционную модель ХРУпозволило доказать критерий безопас­ности систем для более приемлемых ограничений, что существенно рас­ширило область ее применения.

Контрольные вопросы

1. Как произвольную систему ТМД представить системой ХРУ?

3. Что такое субъект системы?

4. Что такое объект системы?

Дата добавления: 2014-11-20 ; Просмотров: 1848 ; Нарушение авторских прав? ;

Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет

Страницы работы

Содержание работы

Федеральное агенство по образованию

Государственное образовательное учреждение

Высшего профессионального образования

«Сибирский государственный аэрокосмический университет

Имени академика М.Ф.Решетнёва»

Факультет информатики и систем управления(ИСУ)

Кафедра безопасности информационных технологий(БИТ)

Лабораторная работа №4.

«Дискреционная модель, основанная на «типизиро­ванной матрице доступа» »

«Теоретические основы компьютерной безопасности»

Выполнил: группа КБ-51

Ломакин Д.В. ______

Красноярск 2008 г.

Модель относится к дискреционному управлению доступа, идея модели: в модели добавляются типы безопасности и каждый элемент (субъект или объект) создается с конкретным типом. Существует сильная и слабая организация типов: сильная – когда тип в последствии вообще не меняется; слабая – когда типы меняются в определенных условиях, но без нарушения политики безопасности.

1 этапом в модели является определение типов и прав доступа.

Определение 1. Существует конечное множество прав доступа.

Определение 2. Существует конечное множества типов объекта или типов субъектов.

Управление в системе происходит полностью по матрице доступа.

Определение 3. защищенным состоянием системы называется 4 элемента: типы, субъекты, объекты, матрица доступа.

В модели существует 6 операций:

Создание, удаление субъектов;

Создание, удаление объекта;

Добавления, удаления права.

1. Отсутствие контроля типов.

2. Возможность косвенного доступа.

3. Возможность создания субъекта наделенного большими полномочиями чем, его создатель.

Устранить 3 недостаток можно при помощи политики контролируемого источника, она требует, что бы создатель или источник документа поддерживал контроль за доступом к документу.

Существует разновидности модели ТАМ это монотонная модель, основанная на типизированной матрице доступа.

Запустим нашу реализованную модель ТАМ программно.

Зайдем под администратором. Эта учетная запись существует всегда, её удалить нельзя, она идет под типом S3(администратор).

Под этой учетной записью мы можем создавать и удалять объекты и субъекты. Но также мы создавать учетные записи можем не заходя под администратором:

Создадим новую учетную запись и зайдем потом под администратором.

У созданной учетной записи тип S1(гость), имеется еще S2(пользователь).Если создавать не под администратором, то учетная запись будет под типом гость. Под администратором можно создавать, как гостя, так и пользователей. Создадим еще учетную запись с типом пользователь. Также разберем объекты они тоже с типами, у нас 2 типа секретно (O2), простой документ(O1). Создадим документ с типом секретно.

Здесь мы видим что, пользователь с типом гость может читать и записывать документ с типом простой, пользователь все. Но также следует сказать что распределение между чтением и записью распределяет администратор. То есть администратор может разрешать чтение и запись, если типы это го разрешают. В нашем случае администратор не может открыть доступ на чтение и запись гостю на документ 1, так как тип гость не позволяет записывать и читать документы с типом секретно. Все остальное можем изменять:

Недостатки нашей модели:

Частичное отсутствие моделей типов, ложится много работы на администратора по распределению на доступ чтения и записи, сильно большие полномочия у администратора.

Зато устранен 3 общий недостаток, тем что мы не можем именно в нашей модели создать субъект с полномочиями больше чем у администратора.

Мы разобрали модель ТАМ, реализованной программно. Посмотрели в работе эту модель. Научились работать с ней, посмотрели недостатки модели.

Модель Харрисона–Руззо–Ульмана (HRU) разработана и впервые предложена в 1971 г., а в 1976 г. появилось ее формальное описание. Она используется для анализа системы защиты, реализующей дискреционную политику безопасности, и ее основного элемента – матрицы доступов. При этом система защиты представляется конечным автоматом, функционирующим согласно определенным правилам перехода.

Обозначим: O – множество объектов системы; S – множество субъектов системы (S≤ O); R – множество прав доступа субъектов к объектам, например права на чтение (read), на запись (write), владения (own); M – матрица доступа, строки которой соответствуют субъектам, а столбцы – объектам; M[s, о] ≤ R – права доступа субъекта s к объекту о. Отдельный автомат, построенный согласно положениям модели HRU, будем называть системой. Функционирование системы рассматривается только с точки зрения изменений в матрице доступа. Возможные изменения определяются шестью примитивными операторами:

«Внести» право r R в M[s, о] – добавление субъекту s права доступа r к объекту о.При этом в ячейку M[s, о] матрицы доступов добавляется элемент r.

«Удалить» право r R из M[s, о] – удаление у субъекта s права доступа r к объекту о. При этом из ячейки M[s, о] матрицы доступов удаляется элемент r.

«Создать» субъект s‘ – добавление в систему нового субъекта s‘. При этом в матрицу доступов добавляются новые столбец и строка.

«Создать» объект о‘ – добавление в систему нового объекта о‘. При этом в матрицу доступов добавляется новый столбец.

«Уничтожить» субъект s‘ – удаление из системы субъекта s‘. При этом из матрицы доступов удаляются соответствующие столбец и строка.

«Уничтожить» объект о‘ – удаление из системы объекта о‘. При этом из матрицы доступов удаляется соответствующий столбец.

В результате выполнения примитивного оператора а осуществляется переход системы из состояния Q = (S, О, M) в новое состояние Q ‘ = (S ‘, O ‘, M ‘) (табл. 5.2). Данный переход обозначим через Q ├ α Q ‘.

Таблица 1Таблица переходов из состояния состояние модели HRU

Из примитивных операторов могут составляться команды. Каждая команда состоит из двух частей: условия, при котором выполняется команда, и последовательности примитивных операторов.

Модель системы безопасности Бэлла-Лападула (Пример мандатного разграничения доступа).

Классическая модель Белла–Лападула (БЛ) построена для анализа систем защиты, реализующих мандатное (полномочное) разграничение доступа. Модель БЛ была предложена в 1975 г.Пусть определены конечные множества: S – множество субъектов системы (например, пользователи системы и программы); О – множество объектов системы (например, все системные файлы); R = (read, write, append, execute) – множество видов доступа субъектов из S к объектам из О, где read – доступ на чтение, write – на запись, append – на запись в конец объекта, execute – на выполнение.

В = <b S × O × R> – множество возможных множеств текущих доступов в системе;

М = sо М – матрица разрешенных доступов, где Мso R – разрешенный доступ

субъекта s к объекту о;

L – множество уровней секретности, например L = <U, С, S, TS>, где U

Дата добавления: 2018-05-12 ; просмотров: 494 ; ЗАКАЗАТЬ РАБОТУ