Формальные модели безопасности

 

В Заметим, что  если существует Stream(Si, Oj)→Оm и существует Stream (Sk, Om) →Оl, то существует и Stream ((Si, Sk), Oj)→Оl, т. е. отношение «между объектами существует поток» является транзитивным относительно пары субъектов). Именно в этом смысле будем говорить об участии субъекта (Sk) в потоке (если Оm является ассоциированным объектом субъекта, не тождественного Si). Введем несколько определений.

Определение 8. Монитор обращений (МО) - субъект, активизирующийся при возникновении потока от любого субъекта к любому объекту. 

Можно выделить два вида МО:

Индикаторный  МО - устанавливающий только факт обращения  субъекта к объекту.

Содержательный  МО - субъект, функционирующий таким  образом, что при возникновении потока от ассоциированного объекта Оm нового субъекта (Si(Si(Om)) к объекту Oj и обратно существует ассоциированный в МО объект Оm о (в данном случае речь идет об ассоциированных объектах-данных), тождественный объекту Оm или Si(Оm). Содержательный МО полностью участвует в потоке от субъекта к объекту (в том смысле, что информация проходит через его ассоциированные объекты-данные и существует тождественное отображение объекта на какой-либо ассоциированный объект МО).

Теперь сформулируем понятие монитора безопасности (в литературе также применяется понятие монитора ссылок). Это понятие связано с упоминаемой выше задачей фильтрации потоков. Поскольку целью является обеспечение безопасности КС, то и целевая функция монитора - фильтрация с целью обеспечения безопасности (отметим еще раз, что разделение на N и L задано априорно).

Определение 9. Монитор безопасности объектов (МБО) - монитор обращений, который разрешает  поток, принадлежащий только множеству  легального доступа L. Разрешение потока в данном случае понимается как выполнение операции над объектом - получателем потока, а запрещение -г как невыполнение (т. е. неизменность объекта - получателя потока).

Монитор безопасности объектов фактически является механизмом реализации политики безопасности в КС. Обратимся теперь к основным моделям работы МБО. [С. 344-363, 7]

 

3.   Формальные модели безопасности

3.1. Применение формальных моделей безопасности

«Модель политики безопасности — формальное выражение политики безопасности. Только с помощью формальных моделей безопасности можно доказать безопасность системы, опираясь при этом на объективные и неопровержимые постулаты математической теории». [С. 2, 17]

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

Основная цель создания политики безопасности и описания ее в виде формальной модели — это  определение условий, которым должно подчиняться поведение системы, выработка критерия безопасности и проведение формального доказательства соответствия системы этому критерию при соблюдении установленных правил и ограничений.

Формальные  модели безопасности позволяют решить ряд задач, возникающих в ходе проектирования, разработки и сертификации защищенных систем.

Производители защищенных информационных систем используют модели безопасности в следующих  случаях:

- при составление формальной спецификации политики безопасности разрабатываемой системы;

-   при выборе и обосновании базовых принципов архитектуры защищенной системы, определяющих механизмы реализации средств защиты;

-   в процессе анализа безопасности системы в качестве эталонной модели;

-   при подтверждении свойств разрабатываемой системы путем формального доказательства соблюдения политики безопасности.

 

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

Эксперты по квалификации в ходе анализа адекватности реализации политики безопасности в  защищенных системах используют модели безопасности в качестве эталонов. [С. 253-254, 1]

3.1.1. Базовые представления моделей безопасности

Все рассматриваемые  модели безопасности основаны на следующих базовых представлениях:

1. Система является совокупностью взаимодействующих сущностей — субъектов и объектов. Безопасность обработки информации обеспечивается путем решения задачи управления доступом объектов к субъектам в соответствии с заданным набором правил и ограничений, образующих политику безопасности. Система безопасна, если субъекты не имеют возможности нарушить правила политики безопасности. Общим подходом для всех моделей является разделение множества сущностей, составляющих систему, на множества субъектов и объектов, хотя сами определения понятий объект и субъект в разных моделях могут существенно различаться.

2. Все взаимодействия в системе моделируются установлением отношений определенного типа между субъектами и объектами. Множество типов отношений определяется в виде набора операций, которые субъекты могут производить над объектами.

3. Все операции контролируются монитором взаимодействий и либо запрещаются, либо разрешаются в соответствии с правилами политики безопасности.

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

5. Совокупность множеств субъектов, объектов и отношений между ними определяет состояние системы. Каждое состояние системы является либо безопасным, либо небезопасным в соответствии с предложенным в модели критерием безопасности.

6.  Основной элемент модели безопасности — это доказательство утверждения (теоремы) о том, что система, находящаяся в безопасном состоянии, не может перейти в небезопасное состояние при соблюдении всех установленных правил и ограничений.

Среди моделей  политик безопасности можно выделить два основных класса: дискреционные (произвольные) и мандатные (нормативные). [С. 212, 4]

3.1.2.  Мандатная и дискреционная модели

«Мандатной политикой безопасности будем считать любую политику, логика и присвоение атрибутов безопасности которой строго контролируются системным администратором политики безопасности.

Дискреционной политикой безопасности будем считать  любую политику, в которой обычные  пользователи могут принимать участие в определении функций политики и/или присвоении атрибутов безопасности». [С. 2,19]

Ролевая политика безопасности представляет собой существенно  усовершенствованную модель Харрисона-Руззо-Ульмана  (управление доступом в ней осуществляется как на основе матрицы прав доступа для ролей, так и с помощью правил, регламентирующих назначение ролей пользователям и их активацию во время сеансов).

Политика доменов  и типов (Domain and Type Enforcement - DTE) модель, являющаяся расширением типизированной матрицы доступа, в которой типы приписаны не только объектам, но и субъектам. [С. 48, 20]

3.2. Дискреционная модель Харрисона-Руззо-Ульмана

Данная модель реализует произвольное управление доступом субъектов к объектам и  контроль за распространением прав доступа.

1. Обозначения

Обозначим: S - множество субъектов (осуществляют доступ к информации); О — множество объектов, содержащих защищаемую информацию; R  = {r1,...,r„} — конечное множество прав доступа, означающих полномочия на выполнение соответствующих действий (чтение, запись, выполнение). Принято считать, что S с О, т.е. субъекты одновременно являются и объектами (это сделано для того, чтобы включить в область действия модели отношения между субъектами).

Поведение системы  моделируется с помощью понятия состояния О х S х R  — пространство состояний системы; М — матрица прав доступа, описывающая текущие права доступа субъектов к объектам (строки - субъекты, столбцы - объекты); Q  = (S, О, M) — текущее состояние системы.

Любая ячейка матрицы M [s, o] содержит набор прав доступа s к объекту o, принадлежащих множеству прав доступа R.

2. Поведение системы

Поведение системы  во времени моделируется переходами между различными состояниями. Переход  осуществляется путем внесения изменений  в матрицу М с помощью команд следующего вида: command a(x1,...,xk) if n in M[xS1,x01] and (условия выполнения команды) r2 inM[xS2,x02] and r . minM[xs ,x0 ] and then op1,op2,...,op, (операции, составляющие команду) где а — имя команды; х,- — параметры команды, являющиеся идентификаторами субъектов и объектов; st и о - индексы субъектов и объектов в диапазоне от 1 до k; opt — элементарные операции (выполняются только в том случае, если все условия, означающие присутствие указанных прав доступа в ячейках матрицы М,  являются истинными).

3. Элементарные операции

В классической модели допустимы только следующие  элементарные операции:

enter r into M[s,o] (добавление субъекту s права r для объекта о) delete r  from M[s,o] (удаление у субъекта s права r для объекта о) create subject s (создание нового субъекта s) create object о (создание нового объекта о) destroy subject s (удаление существующего субъекта s) destroy object о (удаление существующего объекта о). Применение любой элементарной операции ор в системе, находящейся в состоянии Q = (S,O,M),  влечет за собой переход в другое состояние Q' = (S',O',M'), которое отличается от предыдущего состояния Q по крайней мере одним компонентом. Выполнение базовых операций приводит к следующим изменениям в состоянии системы: enter r  into M[s, о], O' = O, S' = S.

M'[xs,x0] =M[xs,x0], если (xs,x0) & (s,o)

M'[s,o] =M[s,o]U{r} -  данная операция вводит право r в существующую ячейку матрицы доступа. Содержимое ячейки рассматривается как множество, т.е. если это право уже имеется, то ячейка не изменяется. Операция enter называется монотонной, т.к. она только добавляет права в матрицу и ничего не удаляет. Предусловие выполнения операции — существование ячейки (существование соответствующих субъекта и объекта). delete r  from M[s, о],        O' =O, S' = S.

M'[xs,x0] =M[Xs, x0], если (xs,x0) & (s, o).

M'[s,o] LM[s,o]\{r} -  данная операция удаляет право r из ячейки матрицы доступа, если оно там присутствует. Содержимое ячейки рассматривается как множество, т.е. если удаляемое право отсутствует в данной ячейке, то данная операция ничего не делает. Операция delete называется немонотонной, т.к. она удаляет информацию из матрицы. Предусловие выполнения операции - существование ячейки (существование соответствующих субъекта и объекта). create subject s (где s  £ S) О' = О и {s}, S' = Su{s}.

M'[xs,x0] =M[xs,x0] для  всех (xs,x0)

M'[s,x0] =0 для всех x0<0, M'[s,xs] =0 для всех S>0

Операция является монотонной. Предусловие выполнения операции -    отсутствие создаваемого субъекта / объекта.

destroy subject s О' = 0\{s}, S> = S\{s}

M' [xs, x0] = M [xs, x0] - для всех (xs, x0). Операция является немонотонной. Предусловие выполнения опера­ции - наличие субъекта / объекта. create object о О1 = О U {о}, S' = S.

M' [xs, x0] =M [xs, x0], если (xs,x0), [W', o] = 0 для всех  xS'. Операция является монотонной. Предусловие выполнения операции - отсутствие создаваемого субъекта / объекта.

destroy object о О' = O\{о}, S' = S.

M'[xs,x0] =M[xs,x0] для всех (xs,x0). Операция является немонотонной. Предусловие выполнения операции - наличие субъекта / объекта.

4.  Формальное описание системы

Формальное описание системы состоит из следующих элементов:

1. конечный набор прав доступа R = {r1, ... ,r};

2. конечные наборы исходных субъектов S0 = {s1,...,st} и объектов О0 = {о1,...,оt}, где S0 С О0;

3.  исходная матрица доступа, содержащая права доступа субъектов к объектам - М0;

4.   конечный набор команд С =  {а,(х1, ... ,х)}, каждая из которых состоит из условий выполнения и интерпретации в терминах перечисленных элементарных операций.

 

Поведение системы  во времени моделируется с помощью  последовательности состояний Qi, причем Qi+1 = Cj(Qj), где С —  множество команд. Попадание системы в то или иное состояние для заданного начального состояния зависит только от условий команд из С и составляющих их операций. Каждое состояние определяет отношения доступа, которые существуют между сущностями системы в виде множества субъектов, объектов и матрицы прав. Должна существовать возможность определить множество состояний системы, в которые она сможет попасть из заданного начального состояния (т.к. для обеспечения безопасности необходимо наложить запрет на некоторые отношения доступа). Это позволит задавать такие начальные условия (интерпретацию команд С,  множества объектов О0, субъектов S0 и матрицу доступа М0), при которых система никогда не сможет попасть в состояния, нежелательные с точки зрения безопасности.

Следовательно, для построения системы с предсказуемым поведением необходимо для заданных начальных условий получить ответ на вопрос: сможет ли некоторый субъект s когда-либо приобрести право доступа r для некоторого объекта o.

Критерий безопасности модели Харрисона-Руззо-Ульмана:

Критерий 2.1. Для  заданной системы начальное состояние Q0 = (S0,O0,M0) является безопасным относительно права r, если не существует применимой к Q0 последовательности команд, в результате которой право r  будет занесено в ячейку памяти матрицы M, в которой оно отсутствовало в состоянии Q0.