Модель матрицы доступов Харрисона-Руззо-Ульмана 2 страница

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

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

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

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

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

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

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

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

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

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

q = (S, O, t, M) ¾ состояние системы;

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

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

command c (x ₁: t ₁, …, x_k : t_k)

if (r ₁Î M [ x_{s 1}, x_{o 1}]) and … and (r_m Î M [ x_sm, x_om ]) then

a₁;

…

a _n;

endif

end

Перед выполнением команды происходит проверка типов фактических параметров, и, если они не совпадают с указанными в определении команды, то команда не выполняется. В модели ТМД используются следующие шесть видов примитивных операторов, отличающихся от аналогичных операторов модели ХРУтолько использованием типизированных параметров (табл. 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,

- «создать» объект x_i с типом t_i.

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

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

command foo (s ₁: u, s ₂: u, s ₃: v, o ₁: w, o ₂: b)

«создать» субъекта s ₂с типом u;

«создать» субъекта s ₃с типом v;

end

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

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

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

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

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

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

Пусть

R* = R È { active };

T* = T È { t_active }.

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

S* = S È { s_active };

O* = O È { s_active }.

Пусть также для каждого 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 системы МТМД, не содержащую примитивные операторы «создать»…, представим командой c (x ₁: t ₁, …, x_k: t_k, s: t_active) системы КФМТМД, полученной из исходной команды добавлением условий проверки active Î M [ s, x_i ], для i­ = 1, …, k.

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

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

- c ’’(x ₁: t ₁, …, x_k: t_k, s: t_active) ¾ команда, содержащая условия и примитивные операторы «внести»… команды c (x ₁: t ₁, …, x_k: t_k), условия проверки active Î M [ s, x_i ], для всех родительских (не создаваемых в команде c (x ₁: t ₁, …, x_k: t_k)) объектов x_i, примитивные операторы «внести» право active в M [ s, x_i ] для всех объектов x_i, создаваемых в команде c (x ₁: t ₁, …, x_k: t_k).

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

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

Определение 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 < b тогда и только тогда, когда для некоторого дочернего типа команды a в графе создания найдется путь в некоторый родительский тип команды b.

Лемма 4.1. В системе АМТМД отношение «<» на множестве команд является отношением строгого порядка (обладает свойствами антирефлексивности, транзитивности и антисимметричности).

Доказательство. Так как граф создания систем АМТМД не содержит циклов, то для любой команды a не выполняется сравнение a < a. Следовательно, отношение «<» обладает свойством антирефлексивности.

Пусть для команд a, b и g выполняются сравнения a < b и b < g. Тогда для некоторого дочернего типа команды a в графе создания существует путь в некоторый родительский тип команды b, и для некоторого дочернего типа команды b в графе создания существует путь в некоторый родительский тип команды g. Кроме того, по определению графа создания для каждого родительского типа команды b существует путь в каждый дочерней тип команды b. Следовательно, для некоторого дочернего типа команды a в графе создания существует путь в некоторый родительский тип команды g. Таким образом, выполняется сравнение a < g, и отношение «<» обладает свойством транзитивности.

Пусть для команд a и b выполняются сравнения a < b и b < a. Предположим противное, что выполняется неравенство a ¹ b. Тогда, повторяя рассуждения, выполненные при обосновании транзитивности отношения «<», получаем, что для некоторого дочернего типа команды a в графе создания существует путь в некоторый родительский тип команды a. По определению графа создания для каждого родительского типа команды a существует путь в каждый дочерней тип команды a. Следовательно, в графе создания существует цикл. Противоречие. Таким образом, отношение «<» обладает свойством антирефлексивности.

Лемма доказана. ■

Алгоритм 4.2. Алгоритм построения «развернутого» состояния для системы АКФМТМД.

Шаг 1. Упорядочить линейно в списке все команды, содержащие примитивные операторы вида «создать»… (команда a следует в списке перед командой b тогда и только тогда, когда или a < b, или a и b несравнимы).

Шаг 2. Начиная с начального состояния применять по созданному на шаге 1 списку все команды, при этом каждая команда применяется со всеми возможными для нее наборами родительских объектов.

Лемма 4.2. Алгоритм 1.2 заканчивает работу за конечное время на любом начальном состоянии произвольной системы АКФМТМД.

Доказательство. Число команд в списке конечно, для каждой команды из списка на каждом шаге работы алгоритма существует конечный набор объектов, которые могут являться ее параметрами. Следовательно, алгоритм 1.2 всегда заканчивает работу за конечное время. Лемма доказана. ■

Определение 4.11. Пусть (q ₀, q ₁, …, q_i, …) некоторая история системы МТМД. Для каждого состояния q_i = (S_i, O_i, t_i, M_i), i = 0, 1, …, на множестве O_i рекурсивно определим функцию порождения объектов p:

- для каждого o Î O ₀Ì O_i положим p(o) = o,

- если объект o Î O_k Ì O_i создан на шаге 0 < k £ i истории командой a _k, где o ₁, o ₂, …, o_m Î O_{k – 1} последовательность входящих в нее параметров-объектов родительских типов, то положим p(o) = a _k (p(o ₁), p(o ₂), …, p(o_m)).

Пример 4.3. Пусть система МТМД с двумя командами:

command cv (x: u, y: v)

«создать» субъекта y с типом v;

end,

command cw (x: u, y: v, z: w)

«создать» объект z с типом w;

end,

и история имеет вид q ₀├ _{cv ( x , y )} q ₁├ _{cw ( x , y , z )} q ₂, где q ₀ = (S ₀, O ₀, t ₀, M ₀) = ({ x }, { x }, {(x, u)}, M ₀). Тогда в состоянии q ₂= (S ₂, O ₂, t ₂, M ₂) = ({ x, y }, { x, y, z }, {(x, u), (y, v), (z, w)}, M ₂) функция p будет иметь значения:

p(x) = x,

p(y) = cv (x),

p(z) = cw (x, сv (x)). ■

Лемма 4.3. В «развернутом» состоянии системы АМТМД для каждого возможного значения функции порождения объектов p существует ровно один соответствующий объект.

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

Пусть (q ₀, q ₁, …, q_l) ¾ история системы, полученная в результате применения к начальному состоянию q ₀ алгоритма 1.2, P _j ¾ множества значений функции p от всех объектов в состоянии q_j, где 0 £ j £ l. При этом P _l ¾ множество значений функции p от всех объектов в «развернутом» состоянии q_l. Очевидно, что выполняются включения P₀ Ì P₁ Ì … Ì P _l.

Докажем от противного, что в «развернутом» состоянии q_l для каждого возможного значения функции p существует соответствующий объект. Пусть (g ₀, g ₁, …, g_i) некоторая история системы АКФМТМД, где g _{0 =} q ₀, такая, что в состоянии g_i = (S^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 такие, что g_k ├ _a g_{k + 1}, и объект o ^{( 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 ⁽⁰⁾ Î O ₀ такой, что выполняется условие p(o ⁽⁰⁾) = o ⁽⁰⁾ Ï P _l, противоречие. Следовательно, в «развернутом» состоянии q_l для каждого возможного значения функции p существует соответствующий объект.

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

Лемма доказана. ■

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

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

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

Так как система монотонная, то для (s, o) Î S_q ´ O_q = S_m ´ O_m выполняется условие

M_q [ s, o ] Í M_m [ s, o ]. (1.1)

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

M_h [ s, o ] Í M_g [p(s), p(o)]. (1.2)

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

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

M_h [ s, o ] Í M_g [p(s), p(o)] Í M_m [p(s), p(o)],

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

M_h [ s, o ] Í M_g [ s, o ] Í M_m [ s, o ].

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

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

Шаг 2. Команды вида c (x ₁: t ₁, …, x_k: t_k) истории (f, …, h, …) заменить на команды c (p(x ₁): t ₁, …, p(x_k): t_k) истории (q, …, g, …).

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

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

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

M_h [ s, o ] Í M_g [p(s), p(o)].

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

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

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

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

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

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

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

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

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

2. Для команды С (q_{i 0}, a_{i 0}) = (q_{i 1}, a_{i 1}, l) машины Тьюринга выпишите две представляющие ее команды модели ХРУ.

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

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

Дата добавления: 2014-11-20