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

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

При таком подходе функция уровня безопасности представляется с по­мощью двух функций, определнных на множестве субъектов и объектов: F_s : S -►L и F_o: O -►L.

Функция перехода T является безопасной по чтению, если для любо­го перехода T(r,v) = v* выполняются следующие условия:

1) если readeM*[s,o] и read iM[s,o], то:

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

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

M = M _s Fo = F*для Vs, o, для которых F*(s) < F_o*(o), read ^M[s,o]

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

M = M _o F_s = F*

для Vs, 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;для Vs, o, для которых F*(s) > F*(o), write &M[s, o]

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

M =M*

Fs = F*

для Vs, 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 eV, при получении запроса rеRот субъекта s eS, переходит в состояние 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 является авторизованной функцией перехода.
Из этого определения следует только необходимое условие безопас­
ности системы. В качестве достаточного условия может использоваться
совокупность критерия авторизации функции перехода и критериев без­
опасного состояния Белла-ЛаПадулы, либо критериев безопасности функ­
ции перехода Мак-Лина.