Теоретические основы защиты информации


Теоретические основы защиты информации - стр. 59


Доказательство. Предположим противное, то есть

Пусть S1,..., Sm - все активизированные субъекты, имеющие доступы bÊр, i=l,...,m, в момент t к объекту О. Тогда согласно лемме 2 множество этих субъектов разбивается на три непересекающиеся множества:

A = {S1|S1ÎD},

B = {S1|S1ÎOt(Ui)},

C = {S1|S1ÎOt(Uj),i¹j}.

Согласно лемме 1 для любого Sl, l=l.....m, существует единственный пользователь, от имени которого активизирован субъект Sl. Если S1ÎA, то согласно предположению 4 и условию теоремы 1, что доступ

-

разрешен, получаем, что S, активизирован от имени Uj. Это противоречит предположению.

Если S1ÎВ, то

 невозможен согласно политике безопасности. Значит, если
, то существует цепочка длины (k+l)

,

и субъект

.Тогда существует цепочка длины k такая, что

.

Повторяя эти рассуждения, через k шагов получим, что

.

Последний доступ невозможен, если выполняется ПБ. Поэтому предположение неверно и теорема 1 доказана.

Теперь построим удобное для реализации множество "услуг" более низкого уровня, поддерживающих ПБ. То есть мы хотим определить множество условий, реализованных в системе 2, таких, что можно доказать теорему о достаточности выполнения этих условий для выполнения правил ПБ.

Условие 1. (Идентификация и аутентификация). Если для любых tÎN, pÍR, S, ОÎОt,

, то вычислены функции принадлежности S и О к множествам Оt(U1), Оt(U2), D.

Условие 2. (Разрешительная подсистема). Если SÎОt(Ui), OÎОt(Uj) и

 в момент t, то из i=j следует
, и из i¹j следует
 (не разрешается доступ).

Условие 3. (Отсутствие обходных путей политики безопасности). Для любых tÎN, рÍR, если субъект S, активизированный к моменту t, получил в момент t доступ

, то в момент t произошел запрос на доступ
.

Теорема 2. Если в построенной системе å выполняются предположения 1-4 и условия 1-3, то выполняется политика безопасности.

Доказательство. Утверждение теоремы следует из двух утверждений:




Начало  Назад  Вперед



Книжный магазин