Передача права чтения по отношению к файлу.

commandcreate (s, o)

create subjecto,

enterr intoM[s, o],

enterw intoM[s, o],

End

Команда разрешает создание нового субъекта с одновременным получением по отношению к нему прав доступа на чтение и на запись.

Получение прав доступа

commandtakex(s, o, p)

ifr inM[s, o] and

x inM[o, p]

Then

enterx intoM[s, p],

End

Команда разрешает получение произвольного права доступа x от любого субъекта o, по отношению к которому исходный субъект s имеет право чтения.

Передача прав доступа

commandgrantx(s, o, p)

ifw inM[s, o] and

x inM[s, p]

Then

enterx intoM[o, p],

End

Команда разрешает передачу произвольного права доступа x от любого субъекта p любому субъекту, по отношению к которому исходный субъект s обладает правом записи. Пусть в начальном состоянии в системе имеются три субъекта: o, s и t; s обладает правом записи по отношению к t, а t обладает некоторым правом a (которое может представлять собой либо r, либо w) по отношению к o. Покажем, как cубъект s может получить право доступа a по отношению к субъекту o.

1. Система находится в начальном состоянии.

2. Субъект s создаёт новый субъект x, по отношению к которому автоматически

получает права чтения и записи.

3. Субъект s передаёт субъекту t права чтения и записи по отношению к x.

4. Субъект t передаёт субъекту x право доступа a по отношению к o.

5. Субъект s получает от субъекта x право доступа a по отношению к o.

Приведённая последовательность операций проиллюстрирована на рис. 2.3.1.2.

Как видим, в результате выполнения шагов 1-5 субъект s обходным путём получает право доступа a по отношению к субъекту o – т.е. происходит утечка права a – а это значит, что исходное состояние не является безопасным.

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

Система Σ = (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, является вычислительно неразрешимой.

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