Безопасная функция перехода. Теорема Мак-Лина. Модель с уполномоченными субъектами
Мандатная модель Мак-Лина является интерпретацией мандатной модели Белла-ЛаПадулы. Основная теорема безопасности основывается на понятии безопасного перехода, а не на понятии безопасного состояния.
При таком подходе функция уровня безопасности представляется с помощью двух функций, определнных на множестве субъектов и объектов: Fs : S -►L и Fo: O -►L.
Функция перехода T является безопасной по чтению, если для любого перехода T(r,v) = v* выполняются следующие условия:
1) если readeM*[s,o] и read iM[s,o], то:
Fs(s) >Fo(o) иF = F*
2) если Fs^F*, то:
M = M s Fo = F*для Vs, o, для которых F*(s) < Fo*(o), read ^M[s,o]
3) если Fo^F* то:
M = M o Fs = F*
для Vs, o, для которых F*(s) < Fo*(o), read ^M[s,o] Функция перехода T является безопасной по записи, если для любого перехода T(r,v) = v* выполняются следующие условия:
1) если writeeM*[s,o] и write ЈM[s,o], то:
Fo(o) >Fs(s) иF = F*
2) если Fs^F*, то:
M = M s Fo = F;для Vs, o, для которых F*(s) > F*(o), write &M[s, o]
3) если Fo^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 0,R, Ta) состоит из начального состояния v 0, множества запросов R и функции перехода Ta : (S хV хR) —>V, которая переводит систему из состояния в состояние по мере выполнения запросов (a — субъект, от которого исходит запрос). Система, находящаяся в состоянии v eV, при получении запроса rеRот субъекта s eS, переходит в состояние v* = Ta(s, v, r).
2.2.8.2. Авторизованная функция перехода
Функция перехода Ta в модели с уполномоченными субъектами называется авторизованной функцией перехода тогда и только тогда, когда для каждого перехода Ta(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, Ta)
Система У( v 0,R, Ta) считается безопасной в том случае, если:
1. начальное состояние v0 и все состояния, достижимые из него путем
применения конечного числа запросов из R, являются безопасными
по критерию Белла-ЛаПадулы;
2. функция перехода Ta является авторизованной функцией перехода.
Из этого определения следует только необходимое условие безопас
ности системы. В качестве достаточного условия может использоваться
совокупность критерия авторизации функции перехода и критериев без
опасного состояния Белла-ЛаПадулы, либо критериев безопасности функ
ции перехода Мак-Лина.