2.2. Типизованная матрица доступов

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

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

1.конечный набор прав доступа R = {r₁ ,... r_i};

2.конечный набор типов Т = {t₁, ..., t_g};

3.конечные наборы исходных субъектов S₀ ={s_i, ..., s_n} и объектов

O₀ ={o_i, ..., о_m}, где S₀  О_о;

4.матрица М, содержащая права доступа субъектов к объектам, и ее начальное

состояние М ₀;

5.конечный набор команд С = {_i(x₁,., x_k)}, включающий условия вы­полнения команд и их интерпретацию в терминах элементарных опе­раций

Тогда состояние системы описывается четверкой Q = (S, О, t, М), где S, О, и М обозначают соответственно множество субъектов, объектов и матрицу доступа, a t: O  Т - функция, ставящая в соответствие каждому объекту некоторый тип.

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

command (x₁:t₁, … ,x_kt_k)

if r₁ in M[x_S1, x₀₁] and (условия выполнения команды)

r₂ in M[x_S2, x₀₂]

.

.

.

r_m in M[x_Sm, x_0m]

then

op₁, op₂ … op_n (операции, составляющие команду)

Перед выполнением команды происходит проверка типов фактиче­ских параметров, и, если они не совпадают с указанными в определении, команда не выполняется.

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

Монотонные операции	Немонотонные операции
enter r into M[s, o]	delete r from M[s, o]
create subject s of type t	destroy subject s
create object o of type t	destroy object o

Смысл элементарных операций совпадает со смыслом аналогичных операций из классической модели Харрисона-Руззо-Ульмана с точностью до использования типов:

enter r into M[s, o] (где s  S, o  O)

O^` = O

S^` = S

t^`(o) = t(o) для всех o  O

M^`[x_s, x_o] = M[x_s, x_o], если (x_s, x_o)  (s, o)

M^`[s, o] = M[s, o] {r}

delete r from M[s, o] (где s  S, o  O)

O^` = O

S^` = S

t^`(o) = t(o) для всех o  O

M^`[x_s, x_o] = M[x_s, x_o], если (x_s, x_o)  (s, o)

M^`[s, o] = M[s, o] \ {r}

create subject s of type t_s (где s  S)

O^` = O  {s}

S^` = S  {s}

t^`(o) = t(o) для всех o  O

t^`(s) = t_s

M^`[x_s, x_o] = M[x_s, x_o] для всех (x_s, x_o) S  O

M^{`</sup>[s, x<sub>o</sub>] =  для всех x<sub>o</sub>  O<sup>`}

M^{`</sup>[s, x<sub>s</sub>] =  для всех x<sub>s</sub>  S<sup>`}

destroy subject s (где s  S)

O^` = O \{s}

S^` = S \ {s}

t^{`</sup>(o) = t(o) для всех o  O<sup>`}

t^`(s) = не определено

M[x_s, x_o]^{`</sup> = M[x<sub>s</sub>, x<sub>o</sub>] для всех (x<sub>s</sub>, x<sub>o</sub>) S<sup>`}  O^`

create object o of type t_o (где o  O)

O^` = O  {o}

S^` = S

t^`(o) = t(o) для всех o  O

t^`(o) = t_o

M^`[x_s, x_o] = M[x_s, x_o] для всех (x_s, x_o)  S  O

M^{`</sup>[x<sub>s</sub>, x<sub>o</sub>] =  для всех x<sub>s</sub>  S<sup>`}

Destroy object o (где o  O\S)

O` = O\{o}

S^` = S

t`(x<sub>o</sub>) = t(x<sub>o</sub>) для всех x<sub>o</sub>  O`

t`(o) = не определено

M^{`</sup>[x<sub>s</sub>, x<sub>o</sub>] = M[x<sub>s</sub>, x<sub>o</sub>] для всех (x<sub>s</sub>, x<sub>o</sub>)  S<sup>`} O^`

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

Харрисон, Руззо и Ульман показали, что критерий безопасности дискреционной модели может быть доказан для систем, в которых все команды _i(x_i,., x_k) являются одноусловными и монотонны­ми. Строгий контроль соответствия типов позволяет смягчить требование одноусловности, заменив его ограничением на типы параметров команд, при выполнении которых происходит создание новых сущностей.

Для того чтобы сформулировать это ограничение определим отно­шения между типами.

Пусть (x₁:t₁,x₂:t₂, ..., x_k:t) - некоторая команда ТАМ.

Будем говорить, что t, является дочерним типом в , если в теле  имеет место одна из следующих элементарных операций: create subject х, of type t, или create object x, of type t,.

В противном случае будем говорить, что t, является родительским типом в .

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

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

create subject s₂ of type u;

create subject s₃ of type v;

end

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

Тогда можно описать взаимосвязи связи между различными типами с помощью графа, определяющего отношение "наследственности" между типами, устанавливаемые через операции порож­дения сущностей (объектов и субъектов). Такой граф называется графом создания и представляет собой направленный граф с множеством вершин Т, в котором ребро от u к v существует тогда и только тогда, когда в сис­теме имеется создающая команда, в которой u является родительским типом, а v -дочерним типом. Этот граф для каждого типа позволяет опре­делить:

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

2) сущности каких типов могут быть порождены при участии сущ­ностей заданного типа.

Модель монотонной типизированной матрицы доступа (МТАМ) идентична ТАМ за исключением того, что в ней отсутствуют немонотон­ные элементарные операции delete, destroy subject и destroy object.

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

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

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

Это означает, что поведение системы становится предсказуемым, поскольку в любом состоянии можно определить сущности каких типов могут появиться в системе, а каких — нет. Но, к сожалению, доказано, что в общем случае сложность проверки критерия безопасности для МТАМ является NP-трудной задачей, т. е. с ростом размерности задачи (количе­ства объектов и субъектов) время на ее решение растет в степенной зави­симости от ее размерности. Этот недостаток может быть преодолен с по­мощью тернарной ТАМ, в которой команды могут иметь не более трех параметров. Тернарная МТАМ является монотонной версией тернарной ТАМ. Для тернарной МТАМ доказательство безопасности радикально упрощается, поскольку при проверке условной части команды всегда используется только небольшой фрагмент матрицы доступа. Тернарная МТАМ по своим выразительным способностям эквивалентна МТАМ, но несмотря на это, доказано, что безопасность ее ациклической реализации разрешима за время, зависящее от размера начальной матрицы доступа полиномиально.

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