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

Описать в общих чертах модель (см. начало 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, является вычислительно

неразрешимой.

◄Для доказательства этого утверждения достаточно свести задачу проверки безопасности

системы к заведомо неразрешимой задаче остановки машины Тьюринга.►

16. Модель Белла-ЛаПадулы. Решѐтка уровней безопасности.

Данная модель была предложена в 1975 году для формализации механизмов мандатного управления доступом. Мандатный принцип разграничения доступа, в свою очередь, ставил своей целью перенести на автоматизированные системы практику секретного документооборота, принятую в правительственных и военных структурах, когда все документы и допущенные к ним лица ассоциируются с иерархическими уровнями секретности. В модели Белла-ЛаПадулы по грифам секретности распределяются субъекты и объекты, действующие в системе, и при этом выполняются следующие правила: