Монитор безопасности обращений (мбо)

Концепция МБО является достаточно естественной формализацией некого механизма, реализующего разграничение доступа в системе. МБО представляет собой фильтр, который разрешает или запрещает доступ, основываясь на установленных в системе правилах разграничения доступа. Получив запрос на доступ от субъекта S к объекту O, МБО анализирует базу правил, соответствующую установленной в системе политике безопасности и разрешает, либо запрещает доступ. МБО удовлетворяет следующим свойствам:

1. Ни один запрос на доступ к объектам не должен выполняться в обход МБО

2. Работа МБО должна быть защищена от постороннего вмешательства.

3. Представление МБО должно быть достаточно простым, для возможности верификации корректности его работы.

Формальные модели управления доступа

Модель Харрисона-Руззо-Ульмана

Разработан в 1971 году и формализует матрицу доступа

М – матрица прав доступа

Q – текущее состоянии системы Q(S,O,M)

М(S,O) – ячейка матрицы, содержащая набор прав доступа субъекта S к объекту O

Поведение системы во времени моделируется переходами между различными ее состояниями. Переходы осуществляются путем внесения изменений в матрицу M с использованием команд следующего вида:

Command a(x1,xk) if r1 in M[Xs1,Xo1] and if r2 in M[Xs2,Xo2] and … if rm in M[Xsm,Xom] and then op1 op2 …

a – Имя команды xi – параметры команды, представляющие идентификаторы субъектов и объектов opi – элементарные операции, которые будут выполнены в том случае, если выполняются все без исключения условия из блока if … then.

В результате выполнения операции команда переходит из состояния Q=(S,O,M) в состояние Q’=(S’,O’,M’).

Модель предусматривает наличие 6 элементарных операций

1. Enter r into M[s,o] (s*принадлежит*S,o*принадлежит*O) Добавление к субъекту S права r по отношению к объекту O. В результате выполнения команды происходит следующее изменение в состоянии системы: S’=S O’=O M’[xs,xo]= M[xs,xo], если (xs,xo) не равно (s,o) M’[s,o]= M’[s,o]v{r}

2. Delete r from M[s,o] (s*принадлежит*S,o*принадлежит*O) Удаление у субъекта S права r по отношению к объекту O S’=S O’=O M’[xs,xo]= M[xs,xo], если (xs,xo) не равно (s,o) M’[s,o]= M’[s,o]\{r}

3. Create subject s (s#не принадлежит#S) Создание нового субъекта s O’=Ov{s} S’=S v{s} M’[xs,xo]= M[xs,xo] для любых (xs,xo)#принадлежащих#S*O M’[s,xo]=#не пустое множество# для любых xo#принадлежащих#O’ M’[s,xo]=#не пустое множество# для любых xs#принадлежащих#S’

4. Destroy subject s (s#принадлежит#S) Удаление существующего субъекта s S’=S\{s} O’=O\{s} M’[xs,xo]= M[xs,xo] для любых (xs,xo)#принадлежащих#S*O

5. Create object o (o#не принадлежит#O) O’=Ov{o} S’=S M’[xs,xo]= M[xs,xo] для любых (xs,xo)#принадлежащих#S*O M’[xs,o]=#не пустое множество# для любых xs#принадлежащих#S’

6. Destroy object o (o#принадлежит#O) Удаление существующего объекта o O’=O\{o} S’=S M’[xs,xo]= M[xs,xo] для любых (xs,xo)#принадлежащих#S’*O’

Пример

1. Создание файла command create_file (p,f) create object f enter own into M[p,f] enter r into M[p,f] enter w into M[p,f] end создает объект own, наделяет пользователя правами чтения и записи.

2. Создание процесса (процесс p создает процесс q и получает на него права чтения, записи и владения, передавая процессу q права записи и чтения по отношению к самому себе) command exec_process (p,q) create subject q enter own into M[p,q] enter r into M[p,q] enter w into M[p,q] enter r into M[q,p] enter w into M[q,p] end

3. Передача права чтения по отношению к файлу. Право чтения на файл f передается владельцем p субъекту q command grand_read (p,q,f) if own in M[p,f] then enter r into M[q,f] end

Формальное описание системы в модели Харрисона-Руззо-Ульмана выглядит следующим образом

#Система#=(Q,R,C)

Состоит из следующих элементов:

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

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

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

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

5. Конечный набор команд C={ai(x1,…,xk)}

Поведение системы во времени рассматривается как последовательность состояний {Qi}, каждое последующее состояние является результатом применений некоторой команды к предыдущей.

… Чётотам…

Покажем, является ли заданная система с некоторым начальным состоянием безопасной относительно того или иного права доступа для частного случая. Система E=(Q,R,C)называется монооперационной, если каждая команда ai#принадлежит#С выполняет один примитивный оператор

Th:

Существует алгоритм, который проверяет исходное состояние монооперационной системы безопасным для данного права А. Доказательство: Покажем, что число последовательностей команд системы, которые необходимо проверить, является ограниченным. В этом случае проверка безопасности системы сведется к полному перебору всех последовательностей и к проверке конечного состояния каждой из них на отсутствие утечки права А. Нет необходимости рассматривать более одного оператора create, т.к. система является монооперационной и одна команда не может одновременно создать объект или субъект и модифицировать его права доступа, поскольку путем замены параметров можно ограничиться работой с последовательностями команд, которые оперируют над существующими объектами или субъектами. Единственная команда create будет необходима на случай, если в начальном состоянии в системе не было ни одного субъекта.

Пусть С1,С2,…,Сn – последовательность команд, в результате выполнения которой происходит утечка права А. Упростим эту последовательность команд следующим образом:

1. Удалим все команды Delete и Destroy.

2. Добавим в начало последовательности С1,С2,…,Сn команду Sinit следующего вида: create subject.

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

4. Аналогично удалим все команды вида create object, заменяя на Sinit.

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

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

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

Th:

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