FLs*(s) < FLo*(o), read ∉ A[s,o].
Определение 2.2.8. Функция перехода FT : (V x Q) → V является безопасной по записи, если для любого перехода FT(v,q)=v* выполняются следующие три условия:
если write ∈A*[s,o] и write ∉ A[s,o], то FL s(s)≥ FLo(o) и FL = FL* ;
если FLs ≠ FLs*, то A=A*, FLo= FLo*, для ∀s и o, у которых
FLs*(s) > FLo*(o), write ∉ A[s,o];
если FLo ≠ FLo*, то A = A*, FLs= FLs *, для ∀s и o, у которых FLs*(s) >
FLo*(o), write ∉ A[s,o].
Определение 2.2.9 (Критерий безопасности МакЛина). Функция перехода FT : (V x Q) → V является безопасной тогда и только тогда, когда она безопасна и по чтению, и по записи.
Смысл ограничений на безопасность функции перехода в оп-
ределениях 2.2.8 и 2.2.9 в неформальном выражении заключается в том, что в процессе перехода может меняться, во-первых, только лишь один из компонентов состояния системы безопасности (или отношение доступа определенного субъекта к определенному объекту, т. е. ячейка матрицы доступа, или решетка уровней безопасности субъектов, или решетка уровней безопасности объектов), а, во-вторых, при условии того, что правила NRU и NWD соблюдаются как в предыдущем, так и в новом состоянии.
Основываясь на введенных определениях, МакЛин сформулировал и доказал следующую теорему.
Теорема 2.2.2. (Теорема безопасности МакЛина). Система Σ(v0 , Q, FT) безопасна в любом состоянии и в процессе переходов между ними, если ее начальное состояние v0 безопасно, а ее функция перехода удовлетворяет критерию безопасности МакЛина.
Условия безопасности переходов МакЛина снимают проблему Zсистемы, но, тем не менее, не решают всех проблем практической реализации КС на основе модели Белла-ЛаПадулы. В частности, введенные условия по определениям 2.2.7 и 2.2.8 накладывают ограничения, но не специфицируют сам процесс изменения уровней безопасности сущностей системы. Иначе говоря, вопросы о том, кто, при каких условиях имеет право изменять уровни безопасности сущностей системы (т. е. инициировать соответствующие переходы), по-прежнему остаются неопределенными.
МакЛин для решения данной проблемы расширил модель БеллаЛаПадулы введением уполномоченных субъектов.
Определение 2.2.10. Подмножество субъектов P (S), которым разрешается инициировать переходы системы, изменяющие уровни безопасности субъектов или объектов, называется уполномоченными (доверенными) субъектами.
На этой основе в модели вводится дополнительная функция управления уровнями безопасности.
Определение 2.2.11. Функцией управления уровнями безопасности
Do'stlaringiz bilan baham: |