Формальные модели управления доступом

27. Модель Харрисона – Руззо – Ульмана. Элементарные операции. Теоремы.

Разработанная в 1971 г. модель Харрисона-Руззо-Ульмана формализует упоминавшееся ранее понятие матрицы доступа – таблицы, описывающей права доступа субъектов к объектам (рис. 2.3.1.1).

Строки матрицы доступа соответствуют субъектам, существующим в системе, а столбцы – объектам. На пересечении строки и столбца указаны права доступа соответствующего субъекта к данному объекту: например, на рис. 2.3.1.1 субъект subj 3 обладает правами чтения и записи по отношению к объекту obj 3.

Введём следующие обозначения:

- S – множество возможных субъектов,

- O – множество возможных объектов (напомним, что S ⊂ O);

- R={r1, …, rn} – конечное множество прав доступа

- O× S × R - пространство состояний системы;

- M – матрица прав доступа, описывающая текущие права доступа субъектов к объектам;

- Q=(S, O, M) – текущее состояние системы;

- M[s,o] – ячейка матрицы, содержащая набор прав доступа субъекта s∈ S к объекту o∈O .

Поведение системы во времени моделируется переходами между различными её состояниями. Переходы осуществляются путём внесения изменений в матрицу М с использованием команд следующего вида:

commandα (x₁,…,x_n)

ifr1 in M[xs1, xo1] and

r2 in M[xs2, xo2] and

…

rm in M[xsm, xom]

Then

op1,

op2,

…

opn,

End

Здесь α - имя команды; xi – параметры команды, представляющие собой идентификаторы субъектов и объектов, opi – элементарные операции. Элементарные операции op1…opn будут выполнены в том случае, если выполняются все без исключения условия из блока if … then. При описании элементарных операций мы будем полагать, что в результате выполнения операции система переходит из состояния Q=(S, O, M) в состояние Q’=(S’, O’, M’).

Модель предусматривает наличие 6 элементарных операций:

1. enter r into M[s,o] ( s∈S,o∈O ) – добавление субъекту s права r по отношению к объекту o. В результате выполнения команды происходят следующие изменения в состоянии системы:

- S’=S,

- O’=O,

- M’[xs, xo]=M[xs, x0], если (xs, xo) ≠ (s,o),

- M’[s, o]=M[s, o] ∪ {r}.

Заметим, что содержимое ячейки таблицы рассматривается как множество. Это, в частности, означает, что если добавляемый элемент уже присутствовал в ячейке, то её содержимое не изменяется.

2. delete r from M[s,o] ( s∈S,o∈O ) – удаление у субъекта s права r по отношению к объекту o. Изменения в состоянии системы:

- S’=S,

- O’=O,

- M’[xs, xo]=M[xs, x0], если (xs, xo) ≠ (s,o),

- M’[s,o]=M[s.o] \ {r}.

Если удаляемое право отсутствовало в ячейке, то состояние системы в результате выполнения данной команды никак не изменяется.

3. create subject s (s∉S ) – создание нового субъекта s. Изменения в состоянии системы:

- O’=O∪ {s},

- S’=S ∪ {s},

- M’[xs, xo]=M[xs, xo] для ∀ (xs, xo)∈S×O,

- M’[s, xo]=Ø для ∀ x O' o ∈

- M’[s, xs]=Ø для ∀ x S' s ∈

Как видим, при создании субъекта в матрицу M добавляются строка и столбец.

4. destroy subject s (s∈S) – удаление существующего субъекта s. Изменения в состоянии системы:

- S’=S \ {s},

- O’=O \ {s},

- M’[xs, xo]=M[xs, xo] для ∀ (xs, xo)∈S’×O’.

5. create object o (o∉O) – создание нового объекта o. Изменения в состоянии системы:

- O’=O∪ {o},

- S’=S,

- M’[xs, xo]=M[xs, xo] для ∀ (xs, xo)∈S×O,

- M’[xs, o]= Ø для ∀ x S' s ∈

При добавлении объекта в матрице доступа создаётся новый столбец.

6. destroy object o (o∈O \ S) – удаление существующего объекта o. Изменения в состоянии системы:

- O’=O \ {o},

- S’=S,

- M’[xs, xo]=M[xs, xo] для ∀ (xs, xo)∈S’×O’.

Приведём несколько примеров команд:

1. Создание файла.

Пользователь p создаёт файл f и получает на него права владения, чтения и записи.

commandcreate_file (p, f)

create objectf,

enterown intoM[p, f],

enterr intoM[p, f],

enterw intoM[p, f],

End

2. Создание процесса.

Процесс p создаёт процесс q и получает на него право чтения, записи и владения, передавая процессу q права записи и чтения по отношению к самому себе.

commandexec_process(p, q)

create subjectq,

enterown intoM[p, q],

enterr intoM[p, q],

enterw intoM[p, q],

enterr intoM[q, p],

enterw intoM[q, p],

End