Модель матрицы доступа HRU

1. Определение 3. Система называется монооперационной, если каждая команда выполняет один примитивный оператор.

2. Определение 2. Начальное состояние О° называется безопасным по отношению к некоторому праву r, если невозможен переход системы в такое состояние Q, в котором может возникнуть утечка права r.

3. Определение 1 Будем считать, что возможна утечка права r ­∈ R в результате выполнения команды c, если при переходе системы в состояние О' выполняется примитивный оператор, вносящий r в элемент матрицы доступов М, до этого r не содержавший.

4. Теорема 1

4.1. Безопасность исходного состояния монооперационной системы

4.1.1. Док-во

5. Теорема 2

5.1. Проверка безопасности производных систем алгоритмически неразрешима.

5.1.1. Док-во