Модель конечного автомата описывает систему как абстрактную математическую машину. В этой модели переменные состояния представляют состояния машины, а функции перехода описывают способ изменения переменных.
Напомним, что модель управления доступом имеет дело только с наиболее существенными переменными состояния, влияющими на безопасность, и потому намного проще, чем полная модель конечного автомата для данной системы.
Модель матрицы доступа (Harrison, Ruzo и Ullman 1976) это частный случай реализации модели машины состояний. Состояния безопасности системы представлены в виде таблицы, содержащей по одной строке для каждого субъекта системы и по одной колонке для каждого субъекта и объекта (таблица 3). Каждое пересечение в массиве определяет режим доступа данного субъекта к каждому объекту или другому субъекту системы.
Таблица 3
| Субъекты | Объекты | Субъекты | ||||
| Чтение Запись | Чтение | --------- | Запись | Пересылка | ||
| Чтение | Чтение Исполне-ние | Чтение Запись | Пересылка | --------- | ||
| Чтение Запись | Исполне-ние | Пересылка | Запись | --------- |
Второй составляющей модели матрицы доступа является набор функций перехода, описывающих способ изменения матрицы доступа.
Более часто матрица доступа используется не как самостоятельная модель управления доступом, а в качестве одной из нескольких переменных состояния в более общей модели конечного автомата.
Другим способом описания управления доступом является модель, выраженная в терминах меток безопасности, приписываемых субъектам и объектам системы. Режим доступа, которым обладает субъект по отношению к объекту, определяется при сравнении их меток безопасности, вместо того, чтобы искать соответствующее пересечение строки и столбца в матрице доступа. Модель может использовать как матрицу доступа, так и атрибуты безопасности. Все подобные модели, рассматривающие доступ субъекта к объекту, могут быть названы моделями управления доступом.
Вариантом модели управления доступом является модель информационных потоков ( Denning, 1983), которая предназначена для анализа потоков информации из одного объекта в другой на основании их меток безопасности
Еще одним типом модели является модель интерференции, в которой субъекты, работающие в различных доменах, защищены от взаимовлияния друг на друга любым способом, нарушающим свойства безопасности системы (Goguen и Meseguer, 1982).
Характеристики модели безопасности
Модель является лишь формулировкой в математических терминах свойств безопасности, которым должна удовлетворять система. Не существует формального способа, с помощью которого можно доказать, что формальная модель управления доступа соответствует правилам управления доступа, принятым в данной системе.
С другой стороны модель может иметь ряд характеристик, назначение которых не столь очевидно. Поскольку модель должна стремиться к математическому совершенству (завершенности и последовательности) в определении свойств, составляющих политику безопасности, это часто влечет за собой включение ограничений или дополнительных свойств, присутствие которых ранее не предусматривалось.
Описание модели управления доступом в системе
Как конечного автомата
Представления модели управления доступом как конечного автомата получили предпочтение из-за того, что они представляют компьютерную систему способом, имитирующим работу операционной системы и аппаратуры. Переменная состояния является абстракцией для каждого бита и байта в системе, изменяющихся по мере работы системы. Функции переходов из состояния в состояние - это абстракция обращений к операционной системе, явно описывающие то, как состояние может (или не может) изменяться.
Модель управления доступом работает не со всеми переменными состояния и функциями системы. Выбор для моделирования переменных и функций, имеющих отношение к безопасности, остается за разработчиком модели.
Разработка модели управления доступом включает в себя определение элементов модели (переменных, функций, правил и т.д) а также безопасного начального состояния. Математически доказывается, что начальное состояние безопасно и что все функции безопасны, после чего путем математической индукции делается вывод о том, что если система первоначально находилась в безопасном состоянии, система останется в безопасном состоянии независимо от того, какие функции и в каком порядке будут выполнены.
Таким образом в разработке модели управления доступом можно выделить следующие шаги:
1. Определение переменных состояния, имеющих отношение к безопасности. Обычно переменные состояния представляют субъекты и объекты системы, их атрибуты безопасности и права доступа между субъектами и объектами.
2. Определение условий для безопасного состояния. Это определение является выражением отношений между значениями переменных состояния, истинность которого должна обеспечиваться при переходах состояния.
3. Определение функций переходов из состояния в состояние. Эти функции описывают допустимые способы изменения переменных состояния. Они также называются правилами изменения доступа, поскольку их цель состоит в указании изменений, которые может производить система, а вовсе не в определении всех возможных изменений. Правила могут быть очень общими и могут допускать наличие функций, которых нет в реальной системе, однако система не может менять переменные состояния каким-либо способом, который не допускается функциями.
Можно выделить несколько характерных черт функций перехода:
· назначение функции - определение взаимосвязи между переменными в предыдущем и новом состояниях;
· функция не задает какого-либо конкретного порядка в выполнении алгоритма операции. Иными словами, функция может рассматриваться как определение того, что произойдет с состоянием по завершении операции;
· функция элементарна. Это значит, что ее эффект не разделяем на более мелкие действия и не прерываем. Указанное изменение состояния происходит моментально, т.е. какого-либо промежутка времени, "в течение" которого происходил бы переход состояния, определить невозможно.
Следует помнить, что каждая дополнительная переменная состояния и сопутствующие ей операции существенно усложняют как саму модель, так и доказательство ее свойств. Модель управления доступом предполагает представление только поведения системы, связанного с безопасностью.
4. Доказывается, что функции обеспечивают сохранение безопасного состояния. Чтобы удостовериться в том, что модель является безопасной, необходимо для каждой функции перехода доказать, что, если система находится в безопасном состоянии до начала выполнения функции перехода, то система останется в безопасном состоянии по ее завершению.
5. Определение начального состояния. Математически начальное состояние выражается как множество начальных значений всех переменных состояния системы. Простейшим начальным состоянием является состояние вообще без каких-либо субъектов и объектов. При этом нет необходимости определять начальные значения каких-либо других переменных состояния, поскольку состояние будет безопасным независимо от их значений. Более реалистичное безопасное начальное состояние предполагает наличие некоторого начального (произвольного) множества субъектов и объектов.
6. Доказывается, что начальное состояние безопасно в соответствии с определением.
