Безопасная функция перехода. Теорема Мак-Лина. Модель с уполномоченными субъектами

для V s, o, для которых F * (s) < F_o *(o), read ^M[s,o] Функция перехода T является безопасной по записи, если для любого перехода T(r,v) = v * выполняются следующие условия:

1) если writeeM*[s,o] и write Ј M[s,o], то:

F_o(o) > F_s (s) иF = F *

2) если F_s^F*, то:

M = M _s Fo = F; для V s, o, для которых F*(s) > F*(o), write & M[s, o]

3) если F_o^F* то:

M =M*

Fs = F *

для V s, o, для которых F*(s) > F*(o), write & M[s, o]

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

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

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

Поскольку безопасный переход из состояния v в состояние v * позво­ляет изменяться только одному элементу из v, и т.к. этот элемент может быть изменен только способами, сохраняющими безопасность состояния, была доказана следующая теорема о свойствах безопасной системы:

Теорема 2.2 (безопасности Мак-Лина). Система безопасна в любом состоянии и в процессе перехода между ними, если ее начальное состояние является безопасным, а ее функция перехода удовлетворяет критерию Мак-Лина.

Обратное утверждение неверно. Система может быть безопасной по определению Белла-ЛаПадулы, но не иметь безопасной функции перехода.

Формулировка основной теоремы безопасности в интерпретации Мак-Лина позволяет расширить область ее применения по сравнению с клас­сической теоремой Белла-ЛаПадулы, но используемый критерий безопас­ности перехода не всегда соответствует требованиям контроля доступа, возникающим на практике.

Модель уполномоченных субъектов

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

Для решения этой задачи Мак-Лин расширил базовую модель путем выделения подмножества уполномоченных субъектов. Таким субъектам разрешается инициировать переходы, в результате которых у сущностей системы изменяются уровни безопасности.

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

Система с уполномоченными субъектами описывается множествами

S, O и L.

Состояние системы описывается набором упорядоченных пар (F,M),

где

F - функция перехода;

M - матрица отношений доступа (введенные обозначения сов­падают с аналогичными понятиями модели Белла-ЛаПадулы). Функция управления уровнями C:SuO —> P (S) определяет подмно­жество субъектов, которым позволено изменять уровень безопасно­сти для заданного объекта или субъекта. P (S) — множество всех подмножеств S.

Модель системы ^(v ₀ ,R, T^a) состоит из начального состояния v ₀, множества запросов R и функции перехода T^a: (S х V х R) —> V, которая переводит систему из состояния в состояние по мере выполнения запросов (a — субъект, от которого исходит запрос). Система, находящаяся в состоянии v e V, при получении запроса r е R от субъекта s e S, переходит в состояние v * = T^a(s, v, r).

2.2.8.2. Авторизованная функция перехода

Функция перехода T^a в модели с уполномоченными субъектами на­зывается авторизованной функцией перехода тогда и только тогда, ко­гда для каждого перехода T^a(s,v,r) = v *, при котором v = (F,M) и v* = (F*,M*), выполняется условие:

Уx е S U O: если F*(x) = F(x), то s G C(x)

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

2.2.8.3. Безопасность системы J2(v0,R, T^a)

Система У(v ₀, R, T^a) считается безопасной в том случае, если:

1. начальное состояние v0 и все состояния, достижимые из него путем
применения конечного числа запросов из R, являются безопасными
по критерию Белла-ЛаПадулы;

2. функция перехода T^a является авторизованной функцией перехода.
Из этого определения следует только необходимое условие безопас­
ности системы. В качестве достаточного условия может использоваться
совокупность критерия авторизации функции перехода и критериев без­
опасного состояния Белла-ЛаПадулы, либо критериев безопасности функ­
ции перехода Мак-Лина.