Если полученное значение – 1 (истинно), то доступ разрешен. Если – 0 (ложно), то неразрешен. Ясно, что язык , на котором мы выразили политику безопасности , опирается на услуги:
· вычисление функций принадлежности ;
· вычисление логического выражения;
· вычисление оператора «».
Для поддержки услуг языку , требуется свой язык , на котором мы определим основные выражения для предоставления услуг языку верхнего уровня. Возможно, что функции необходимо реализовать, опираясь на язык более низкого уровня и т.д.
Пусть услуги, описанные на языке мы умеем гарантировать. Тогда надежность выполнения политики определяется полнотой ее описания в терминах услуг . Если модель – формальная, то есть язык формально определяет правила политики , то можно доказать или опровергнуть утверждение, что множество предоставленных услуг полностью и однозначно определяет политику . Гарантии выполнения этих услуг равносильны гарантиям соблюдения политики. Тогда более сложная задача сводится к более простым и к доказательству того факта, что этих услуг достаточно для выполнения политики. Все это обеспечивает доказанность защиты с точки зрения математики, или гарантированность с точки зрения уверенности в поддержке политики со стороны более простых функций.
Одновременно, изложенный подход представляет метод анализа систем защиты, позволяющий выявлять слабости в проектируемых или уже существующих системах. При этом иерархия языков может быть неоднозначной, главное - удобство представления и анализа.
Однако проводить подобный анализ в каждой системе дорого. Кроме того, методика проведения анализа государственных систем – конфиденциальная информация. Выход был найден в том, что условия теорем, доказывающих поддержку политики безопасности (включая соответствующую политику), формулировать без доказательства в виде стандарта. Такой подход американцы впервые применили в 1983 году, опубликовав открыто проект стандарта по защите информации в электронных системах обмена данными («Оранжевая книга»), где сформулированы требования гарантированной поддержки двух классов политик – дискреционной и политики MLS. Затем этот метод они применили в 1987 г. для описания гарантированно защищенных распределенных сетей, поддерживающих те же политики, и в 1991 г.для описания требований гарантированно защищенных баз данных. Этот же путь использовали канадцы и европейские государства, создав свои стандарты защиты.
ПРИМЕР ГАРАНТИРОВАННО ЗАЩИЩЕННОЙ СИСТЕМЫ ОБРАБОТКИ ИНФОРМАЦИИ.
Построим пример гарантированно защищенной системы обработки информации. Сначала определим модель системы , которая оперирует с ценной информацией. Считаем, что время дискретно и принимает значения из множества , информация в системе , включая описание самой системы, представима в форме слов некоторого гипотетического языка над некоторым конечным алфавитом . Напомним, что объект в – это конечное множество слов из , состояние объекта – выделенное слово из множества, определяющего этот объект. С понятием объекта связано агрегирование информации в и о . Например, объектом является принтер, который можно рассматривать как автомат с конечным множеством состояний, а эти состояния – суть слова языка . Другой пример объекта – файл. Множество слов, которые могут быть записаны в файле, является конечным и определяет объект, а состояния объекта -это текущая запись в файле, которая тоже является словом в языке .
Принято считать, что вся информация о в данный момент может быть представлена в виде состояний конечного множества объектов. Поэтому будем считать, что состояние системы – это набор состояний ее объектов. Объекты могут создаваться и уничтожаться, поэтому можно говорить о множестве объектов системы в момент , которое мы будем обозначать .
Для каждого выделим в подмножество субъектов . Любой субъект есть описание некоторого преобразования информации в системе . Для реализации этого преобразования в необходимо выделить определенные ресурсы (домен) и организовать определенное взаимодействие ресурсов, приводящее к преобразованию информации, которое назовем процессом. Тогда каждый субъект может находиться в двух состояниях: в форме описания, в котором субъект называется неактивизированным, и в форме <домен, процесс>, в которой субъект называется активизированным.
Активизировать субъект может только другой активизированный субъект. Для каждого на множестве можно определить орграф , где и из соединены дугой тогда и только тогда, когда в случае активизации возможна активизация . Если субъект – такой, что для каждого в вершину не входит дуг, то такой субъект будем называть пользователем. Для простоты положим, что в системе всего два пользователя: и . Пользователи считаются активизированными по определению и могут активизировать другие субъекты.
Если в любой момент в графе в вершину не входят и не выходят дуги, то такие субъекты исключаем из рассмотрения.
Предположение 1. Если субъект активизирован в момент , то существует единственный активизированный субъект , который активизировал . В момент активизированы только пользователи.
Лемма 1. Если в данный момент активизирован субъект , то существует единственный пользователь , от имени которого активизирован субъект , то есть существует цепочка .
Доказательство. Согласно предположению 1 существует единственный субъект , активизировавший . Если или , то лемма доказана. Если , то существует единственный субъект , активизировавший . В силу конечности времени работы системы и того факта, что в начальный момент активизированы могут быть только пользователи, получаем в начале цепочки одного из них. На этом, согласно определению пользователей, цепочка обрывается. Лемма доказана.
Предположение 1 требует единственности идентификации субъектов. Далее будем предполагать, что каждый объект в системе имеет уникальное имя.
Кроме активизации в системе существуют и другие виды доступа активизированных субъектов к объектам. Будем обозначать множество всех видов доступов через и считать . Если , то будем обозначать множество доступов активизированного субъекта к объекту через . Если в некоторый промежуток времени реализована последовательность доступов , то будем считать, что произошел доступ от имени субъекта к объекту . Нас не интересует, какую задачу решает система , мы лишь моделируем функционирование системы последовательностью доступов.
Предположение 2. Функционирование системы описывается последовательностью доступов множеств субъектов к множествам объектов в каждый момент времени .
Обобщим введенный орграф добавив дуги , обозначающие возможность любого доступа субъекта к объекту в момент , в случае активизации . Обозначим , где означает возможность осуществления цепочки доступов (возможность доступа к от имени ). Тогда для любого в системе определены и . Будем считать, что фиксировано для всех , , в начальный момент .
Определение. Множество объектов называется общими ресурсами системы.
В частности, средствами из пользователь может создавать объекты и уничтожать объекты, не принадлежащие . Создание и уничтожение каких-либо объектов является доступом в к некоторым объектам из (и к уничтожаемым объектам).
Мы считаем, что из объектов системы построена некоторая подсистема, которая реализует доступы. Будем полагать, что любое обращение субъекта за доступом к объекту в эту подсистему начинается с запроса, который мы будем обозначать .
При порождении объекта субъект обращается к соответствующей процедуре, в результате которой создается объект с уникальным именем. Тогда в силу леммы 1, существует единственный пользователь, от имени которого активизирован субъект, создавший этот объект. Будем говорить, что соответствующий пользователь породил данный объект. Обозначим через множество объектов из , которые породил пользователь . Естественно, будем считать, что .
Лемма 2. Для каждого , для каждого , , существует единственный пользователь такой, что .
Доказательство. Поскольку , то объект , , порожден в некоторый момент , . Тогда в существовал активизированный субъект , создавший О. Тогда, как отмечено ранее, существует единственный пользователь U, породивший . Лемма доказана.
Обратимся теперь к вопросам безопасности информации в системе. Если в есть доступы и , то ограничимся опасностью утечки информации через каналы по памяти, которые могут возникнуть при доступах к объектам. Таким каналом может быть следующая последовательность доступов при :
в момент и в момент , .
При определенных условиях может оказаться опасным доступ от имени пользователя: в момент и в момент , , .
С некоторой избыточностью мы исчерпаем возможные каналы по памяти, если будем считать неблагоприятными какие-либо доступы вида
, ,
(1)
которые мы и считаем каналами утечки.
Предположение 3. Если , то доступы в (1) при любых не могут создать канал утечки.
Это значит, что мы предположили невозможным отразить какую-либо ценную информацию в объектах общего доступа. Это очень сильное предположение и оно противоречит, по крайней мере, возможности присваивать уникальные имена объектам. В самом деле, если объектам присвоены уникальные имена, то в необходимо иметь информацию о уже присвоенных именах, что противоречит предположению 3 о том, что доступы от имени пользователей не отражаются в информации объектов общего пользования. В случае имен можно выйти из положения, используя случайные векторы, вероятности совпадения которых за обозримый период работы системы можно сделать как угодно малыми. Все построения и выводы возможны при стохастическом способе присвоения имен, но должны содержать элементы вероятностной конструкции. Чтобы не усложнять систему стохастическими элементами мы будем следовать сделанным выше предположениям.
Тогда в (1) достаточно ограничиться объектами . Это значит, что в одном из доступов в (1) имеется , где , . Таким образом, в системе считаются неблагоприятными доступы вида:
(2)
то есть доступы от имени какого-либо пользователя к объекту, созданному другим пользователем. Такие доступы будем далее называть утечкой информации.
Предположение 4. Если некоторый субъект активизирован от имени пользователя (т.e. ), в свою очередь субъекту предоставлены в момент доступ к объекту , то либо , либо , либо система прекращает работу и выключается.
Определим следующую политику безопасности (ПБ):
«Если , то при доступ разрешается. Если , , , то доступ невозможен».
Теорема 1. Пусть в построенной системе выполняются предположения 1-4. Если все доступы осуществляются в соответствии с ПБ, то утечка информации вида (2) невозможна.
Доказательство. Предположим противное, то есть
Пусть – все активизированные субъекты, имеющие доступы в момент к объекту . Тогда согласно лемме 2 множество этих субъектов разбивается на три непересекающиеся множества: , и .
Согласно лемме 1 для любого , существует единственный пользователь, от имени которого активизирован субъект .
Если , то согласно предположению 4 и условию теоремы 1, что доступ – разрешен, получаем, что , активизирован от имени . Это противоречит предположению.
Если , то невозможен согласно политике безопасности. Значит, если , то существует цепочка длины вида , и субъект . Тогда существует цепочка длины такая, что . Повторяя эти рассуждения, через шагов получим, что .
Последний доступ невозможен, если выполняется ПБ. Поэтому предположение неверно и теорема 1 доказана. ▲
Теперь построим удобное для реализации множество «услуг» более низкого уровня, поддерживающих ПБ. То есть мы хотим определить множество условий, реализованных в системе , таких, что можно доказать теорему о достаточности выполнения этих условий для выполнения правил ПБ.
Условие 1. (Идентификация и аутентификация). Если для любых , , , , , то вычислены функции принадлежности и к множествам , , .
Условие 2. (Разрешительная подсистема). Если , и в момент , то из следует (разрешение доступа), и из следует (запрещение доступа).
Условие 3. (Отсутствие обходных путей политики безопасности). Для любых , , если субъект , активизированный к моменту , получил в момент доступ , то в момент произошел запрос на доступ .
studopediasu.com - Студопедия (2013 - 2026) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав!Последнее добавление