Модель Харрисона-Руззо-Ульмана. Формальное описание системы. Критерий безопасности (с доказательством).

Описать в общих чертах модель (см. начало 14 вопроса).

Формальное описание системы в модели Харрисона-Руззо-Ульмана выглядит следующим образом. Система Σ = (Q, R,C) состоит из следующих элементов:

1. Конечный набор прав доступа R={r1, …, rn}.

2. Конечный набор исходных субъектов S0={s1, …, sl}.

3. Конечный набор исходных объектов O0={o1, .., om}.

4. Исходная матрица доступа M0.

5. Конечный набор команд { ( ,..., )} i 1 k C = α x x .

Поведение системы во времени рассматривается как последовательность состояний {Qi}, каждое последующее состояние является результатом применения некоторой команды к предыдущему: Qn+1=Cn(Qn). Для заданной системы начальное состояние Q0={S0, O0, M0} называется безопасным относительно права r, если не существует применимой к Q0 последовательности команд, в результате выполнения которой право r будет занесено в ячейку матрицы M, в которой оно отсутствовало в состоянии Q0. Другими словами это означает, что субъект никогда не получит право доступа r к объекту, если он не имел его изначально. Если же право r оказалось в ячейке матрицы M, в которой оно изначально отсутствовало, то говорят, что произошла утечка права r.

Система Σ = (Q, R,C) называется монооперационной, если каждая команда C i α ∈ выполняет один примитивный оператор.

Теорема. Существует алгоритм, который проверяет, является ли исходное состояние монооперационной системы безопасным для данного права a.

◄ Покажем, что число последовательностей команд системы, которое необходимо проверить, является ограниченным. В этом случае проверка безопасности исходного состояния системы сведётся к полному перебору всех последовательностей и проверке конечного состояния каждой из них на отсутствие утечки права a. Заметим, что команды delete и destroy можно не рассматривать, поскольку нас интересует наличие права a, а не его отсутствие. Аналогично, нет необходимости рассматривать более одного оператора create: система является монооперационной, и одна команда не может одновременно создать объект или субъект и модифицировать его права доступа, поскольку путём замены параметров можно ограничиться работой с последовательностями команд, которые оперируют над существующими субъектами и объектами. Единственная команда create будет необходима на случай, если в начальном   состоянии в системе не было ни одного субъекта. Итак, пусть c1, c2, …, cn – последовательность команд, в результате выполнения которой происходит утечка права a. Упростим эту последовательность команд следующим образом:

1. Удалим все команды delete и destroy.

2. Добавим в начало последовательности c1, c2, …, cn команду sinit вида create subject.

3. Проходя последовательность команд справа налево, последовательно удалим все команды вида create subject и заменим все ссылки на создаваемые с помощью этих команд субъекты ссылкой на sinit.

4. Аналогично удалим все команды вида create object, заменяя ссылки на создаваемые с помощью этих команд объекты ссылками на sinit.

5. Удалим все команды вида enter, вносящие право a в ячейку, которая уже содержит это право.

Согласно приведённым выше замечаниям, получившаяся в результате данных преобразований последовательность команд также приводит к утечке права a.

Проанализируем состав возможных команд в получившейся последовательности.

Команды вида create object, destroy subject, destroy object и delete в последовательности отсутствуют. Команда create subject присутствует в единственном числе. Максимальное число команд вида enter равно ( 1)( 1) 0 0 R S + O + . Тем самым, общее число возможных команд равно ( 1)( 1) 0 0 R S + O + + 1 – а значит, количество последовательностей команд ограничено.►

К сожалению, расширить полученный результат на произвольные системы невозможно.

Теорема. Для систем общего вида задача определения того, является ли исходное состояние системы безопасным для данного права a, является вычислительно неразрешимой.

◄Для доказательства этого утверждения достаточно свести задачу проверки безопасности системы к заведомо неразрешимой задаче остановки машины Тьюринга.►