• Основные положения модели
  
• Пример некорректного определения безопасности в модели БЛ
  
• Эквивалентные подходы и определения безопасности в модели БЛ
  
• Подход Read-Write
  
• Подход Transaction
  
• Пробдемы использования модели БЛ
  
• Модель Low-Water-Mark

Основные положения модели

Классическая модель Белла - Лападула ( БЛ ) построена для анализа систем защиты, реализующих мандатное ( полномочное ) разграничение доступа. Возможность ее использования в качестве формальной модели таких систем непосредственно отмечена в критерии TCSEC ( "Оранжевая книга" ). Модель БЛ была предложена в 1975 г. Однако ее полное описание до сих пор недоступно, поэтому мы приведем его в урезанном виде.

Пусть определены конечные множества:

S - множество субъектов системы ( например, пользователи системы и программы )

O - множество объектов системы ( например, все системные файлы )

R = {read, write, append, execute}- множество видов доступа субъектов из S к объектам из O, где read -доступ на чтение, write - на запись, append - на запись в конец объекта, execute - на выполнение

Обозначим:

B = {b ≤ S × O × R} – множество возможных множеств текущих доступов в системе.

M – матрица разрешенных доступов, где M_so R – разрешенный доступ субъекта s к объекту o

L – множество уровней секретности, например L = {U, C, S, TS}, где U < C < S < TS

(f_s, f_o, f_c) F = L^s × L^o × L^s – тройка функций (f_s, f_o, f_c), определяющих:

• f_s: S → L – уровень доступа субъекта
• f_o: O → L – уровень секретности объекта
• f_c: S → L – текущий уровень доступа субъекта, при этом s S f_c(s) ≤ f_s(s)

H – текущий уровень иерархии объектов ( далее не рассматривается )

V = B × M × F × H – множество состояний системы

Q – множество запросов системе

D – множество решений по запросам, например { yes, no, error }

W ≤ Q × D × V × V – множество действий системы, где четверка (q, d, v₂, v₁) W означает, что система по запросу q с ответом d перешла из состояния v₁ в состояние v₂

N₀ – множество значений времени (N₀ = 0, 1, 2, ...)

X – множество функций x: N₀ → Q задающих все возможные последовательности запросов к системе

Y – множество функций y: N₀ → D задающих все возможные последовательности ответов системы по запросам

Z – множество функций z: N₀ → V задающих все возможные последовательности состояний системы

Определение 1. ∑ (Q, D, W, z₀) ≤ X × Y × Z называется системой, если выполняется (x, y, z) ∑ (Q, D, W, z₀) тогда и только тогда, когда (x_t, y_t, z_t+1, z_t) W для каждого t N₀ где z – начальное состояние системы. При этом каждый набор (x, y, z) ∑ (Q, D, W, z₀) называется реализацией системы, а (x_t, y_t, z_t+1, z_t) W – действие системы для любого t N₀.

Безопасность системы определяется с помощью трех свойств:

1. ss – свойства простой безопасности ( simple security )
2. * - свойства “звезда”
3. ds – свойства дискретной безопасности ( discretionary security )

Определение 2. Доступ (s, o, r) S × O × R обладает ss – свойством относительно f = (f_s, f_o, f_c) F, если выполняется одно из условий:

• r {execute, append}
• r {read, write} и f_s(s) ≥ f_o ( o )

Определение 3. Состояние системы (b, M, f, h) V обладает ss – свойством, если каждый элемент (s, o, r) b обладает ss – свойством относительно f.

Определение 4. Доступ (s, o, r) S × O × R удовлетворяет * - свойству относительно f = (f_s, f_o, f_c) F, если выполняется одно из условий:

• r = execute
• r = append и f_o(o) = f_c(s)
• r = read и f_c(s) = f_o(o)
• r = write и f_c(s) = f_o(o)

Определение 5. Состояние системы (b, M, f, h) V обладает * - свойством, если каждый элемент (s, o, r) b обладает * - свойством относительно f.

Определение 6.Состояние системы (b, M, f, h) V обладает * - свойством, относительно подмножества S’ ≤ S, если каждый элемент (s, o, r) b, где s S’ обладает * - свойством относительно f. При этом S \ S’ называются множеством доверенных субъектов, т.е. субъектов, имеющих право нарушать политику безопасности.

Определение 7. Состояние системы (b, M, f, h) V обладает ds - свойством, если для каждого элемента (s, o, r) b выполняется r M_so.

Определение 8. Состояние системы (b, M, f, h) называется безопасным, если обладает * -свойством относительно S’, ss - свойством и ds – свойством.

Определение 9. Реализация системы (x, y, z) ∑ (Q, D, W, z₀) обладает ss - свойством ( * -свойством, ds – свойством ), если в последовательности (z₀, z₁, ...) каждое состояние обладает ss - свойством ( * - свойством, ds - свойством).

Определение 10. Система ∑ (Q, D, W, z_o) обладает ss - свойством ( * - свойством, ds - свойством), если каждая ее реализация обладает ss – свойством ( * - свойством, ds - свойством )

Определение 11. Система ∑ (Q, D, W, z₀) называется безопасной, если она обладает ss - свойством, * - войством, ds - свойством одновременно.

Прокомментируем введенные выше свойства безопасности системы. Во - первых, из обладания доступом * - свойством относительно f следует обладание этим доступом ss - свойством относительно f. Во-вторых, из обладания системой ss - свойством следует, что в модели БЛ выполняется запрет на чтение вверх, принятый в мандатной ( полномочной ) политике безопасности. Кроме того, ss - свойство не допускает модификацию с использованием доступа write, если f_s(s) < f_o(o). Таким образом, функция f_s(s) определяет для субъекта s верхний уровень секретности объектов, к которым он потенциально может получить доступ read или write.

В-третьих, поясним * - свойство. Если субъект s может понизить свой текущий доступ до f_с(s) = f_o(o), то он может получить доступ write к o объекту o, но не доступ read к объекту o’, с уровнем f_o(o’) > f_c(s). Хотя при этом, возможно, выполняется f_s(s) = f_o(o’) и в каких - то других состояниях системы субъект s может получить доступ read к объекту o’. Таким образом, * - свойство исключает появление в системе канала утечки информации сверху вниз и соответствует требованиям мандатной ( полномочной ) политики безопасности.

Проверка безопасности системы по определению в большинстве случаев не может быть реализована на практике в связи с тем, что при этом требуется проверка безопасности всех реализаций системы, а их бесконечно много. Следовательно, необходимо определить и обосновать иные условия безопасности системы, которые можно проверять на практике. В классической модели БЛ эти условия определяются для множества действий системы W.

Теорема А1. Система ∑ (Q, D, W, z₀) обладает ss – свойством для любого начального состояния z₀, обладающего ss – свойством, тогда и только тогда, когда для любого (q, d, (b*, M*, f*, h* ), (b, M, f, h )) W удовлетворяет условиям:

Условие 1. Для любого (s, o, r) b* \ b обладает ss – свойством относительно f*.

Условие 2. Если (s, o, r) b и не обладает ss – свойством относительно f*, то (s, o, r) b*.

Достаточность. Пусть выполнены условия 1 и 2 и пусть (x, y, z) ∑ (Q, D, W, z₀) – произвольная реализация системы. Тогда (x_t, y_t, (b_t+1, M_t+1, f_t+1, h_t+1 ), (b_t, M_t, f_t, h_t)) W, где z_t+1 = (b_t+1, M_t+1, f_t+1, h_t+1), z_t = (b_t, M_t, f_t, h_t) для t N₀.

Для любого (s, o, r) b_t+1 выполняется или (s, o, r) b_t+1 \ b_t или (s, o, r) b_t. Из условия 1 следует, что состояние системы z_t+1 пополнилось доступами, которые обладают ss – свойством относительно f*. Из условия 2 следует, что доступы из b_t, которые не обладают ss – свойствами относительно f*, не входят в b_t+1. Следовательно, для любого (s, o, r) b_t+1 обладает ss – свойством относительно f* и по определению состояние z_t+1 обладает ss – свойством для t N₀. Так как по условию и состояние z₀ обладает ss – свойством, то выбранная нами произвольная реализация (x, y, z) также обладает ss –свойством. Достаточность доказана.

Необходимость. Пусть система ∑ (Q, D, W, z₀) обладает ss – свойством. Будем считать, что в множестве W входят только те действия системе, которые используются в ее реализациях. Тогда для любого (q, d, ( B*, M*, f*, h* ), (b, M, f, h ) ) W существует (x, y, z) ∑ (Q, D, W, z₀) и существует t N₀: (q, d, ( b*, M*, f*, h* ), ( b, M, f, h ) ) = (x_t, y_t, z_t+1, z_t). Так как реализация системы (x, y, z) обладает ss – свойством, то и состояние z_t+1 = (b*, M*, f*, h* ) обладает ss – свойством по определению. Следовательно, условия 1 и 2 очевидно выполняются. Необходимость доказана.

Теорема А2. Система ∑ (Q, D, W, z) обладает * - свойством относительно S’ ≤ S для любого начального состояния z₀, обладающего * - свойством относительно S’, тогда и только тогда, когда для любого (q, d, (b*, M*, f*, h* ), (b, M, f, h ) ) W удовлетворяет условиям:

Условие 2. Для любого s S’, существует (s, o, r) b* \ b обладает * - свойством относительно f*.

Условие 2. Для любого s S’, если (s, o, r) b и не обладает * - свойством относительно f*, то (s, o, r) b*.

Доказательство. Аналогично доказательству теоремы А1.

Теорема А3. Система ∑ (Q, D, W, z₀) обладает ds – свойством для любого начального состояния z₀, обладающего ds – свойством, тогда и только тогда, когда для любого (q, d, (b*, M*, f*, h* ), (b, M, f, h ) ) W удовлетворяет условиям:

Условие 1. Для любого (s, o, r) b* \ b выполняется r m_so.

Условие 2. Если (s, o, r) b и r m_so, то (s, o, r) b*.

Доказательство. Аналогично доказательству теоремы А1.

Теорема BST ( Basic Security Theorem ). Система ∑ (Q, D, W, z₀) безопасна тогда и только тогда, когда z₀ безопасное состояние и множество действий системы W удовлетворяет условиям теорем А1, А2, АЗ.

Доказательство.Теорема BST следует из теорем А1, А2, АЗ.

Описанная выше классическая модель БЛ предлагает общий подход к построению систем, реализующих мандатную ( полномочную ) политику безопасности. В модели БЛ определяется, какими свойствами должны обладать состояния и действия системы, чтобы она была безопасной согласно определению 11. В то же время в модели не указывается конкретно, что должна делать система по запросам на доступ субъектов к объектам при переходе из состояния в состояние, как конкретно должны при этом изменяться значения элементов модели.

Пример 1. Пусть субъект s запрашивает доступ read к объекту o'. В данной ситуации система может выбрать один из двух возможных путей:

1. запретить субъекту s запрашиваемый им доступ read на объект o'
2. закрыть доступ write субъекта s к объекту o, повысить текущий уровень секретности f_c(s) до High, разрешить субъекту s запрашиваемый им доступ read к объекту o'.

Каждый из описанных путей соответствует требованиям безопасности модели БЛ.

В реальных системах возможны более сложные ситуации, чем ситуация, описанная в примере 1. Кроме того, возможно использование в системе каких - то других видов доступа субъектов к объектам, которые потребуют доопределения свойств безопасности, что не всегда легко сделать. В связи с этим большое значение имеет корректное определение свойств безопасности.

Пример некорректного определения безопасности в модели БЛ

Определение 12. Доступ (s, o, r) S × O × R удовлетворяет ♣ - свойству относительно f = (f_s, f₀, f_c) F, если выполняется одно из условий:

• r {read, append, execute}
• r= write и f_c(s) = f_o(o)

Определение 13. Состояние системы (b, M, f, h) V обладает ♣ - свойством, если каждый элемент (s, o, r) b обладает ♣ - свойством относительно f.

Определение 14. Состояние системы (b, M, f, h) V называется ♣ - безопасным, если обладает ss – свойством, ♣ - свойством, ds – свойством одновременно.

Определение 15. Реализация (x, y, z) системы ∑ (Q, D, W, z₀) обладает ♣ - свойством, если в последовательности (z₀, z₁ ... ) каждое состояние обладает ♣ - свойством.

Определение 16. Система ∑ (Q, D, W, z₀) обладает ♣ - свойством, если каждая ее реализация обладает ♣ - свойством.

Определение 17. Система ∑ (Q, D, W, z₀) называется ♣ - безопасной, если она обладает ss – свойством, ♣ - свойством, ds – свойством одновременно.

Теорема А2♣. Система ∑ (Q, D, W, z₀) обладает ♣ - свойством для любого начального состояния z₀, обладающего ♣ - свойством, тогда и только, когда для любого (q, d, (b*, M*, f*, h*, (b, M, f, h)) W удовлетворяет условиям:

Условие 1. Для каждого (s, o, r) b* \ b обладает ♣ - свойством относительно f*.

Условие 2. Если (s, o, r) b и не обладает ♣ - свойством относительно f*, то (s, o, r) b*.

Доказательство. Аналогично доказательству теоремы А1.

Теорема BST♣. Система ∑ (Q, D, W, z₀) ♣ - безопасна тогда и только тогда, когда z₀ ♣ - безопасное состояние и множество действий системы W удовлетворяет условиям теоремы А1, А2♣, А3.

Доказательство. Теорема BST♣ следует из теоремы А1, А2♣, А3.

Эквивалентные подходы к определению безопасности в модели БЛ

В зависимости от условий практического использования модели или в целях ее дальнейшего исследования возможно использование эквивалентных подходов к определению свойств безопасности. Мы приведем два подхода, изменяющих значения отдельных элементов модели, но не меняющих ее по сути. При рассмотрении этих подходов положим R = {read, write} и для каждой s S f_s(s) = f_c(s). Исключим из рассмотрения матрицу доступов M и множество ответов системы D. Вместо множества действий системы W используем функцию переходов T(q, v) = v* - переход из состояния v по команде q в состояние v* и будем обозначать систему через ∑ (V, T, z₀).

Подход Read-Write ( RW )

Переопределим ss – свойство и & - свойство. Так как основные ограничения на доступ write следует из * - свойства, то в ss – свойстве зададим ограничения только на read.

Определение 18. Доступ (s, o, r) b обладает ss – свойством, если выполняется одно из условий:

• r = write
• r = read и f_s(s) ≥ f_o(o)

Определение 19. Доступ (s, x, r) b обладает * - свойством, если выполняются одно из условий:

• r = read и не существует y O: (s, y, write) b и f ₀( x) > f₀(y)
• r = write и не существует y O: (s, y, read) b и f ₀(y) > f₀(x)

Заметим особо, что в * - свойстве не рассматривается уровень доступа субъекта посредника s. В этом нет необходимости, так как если требовать выполнения * - свойства и ss - свойства одновременно и считать, что субъект не может накапливать в себе информацию, то не возникают противоречия по существу с положениями мандатной ( полномочной ) политики безопасности. Субъект может читать информацию из объектов с уровнем секретности не выше его уровня доступа, и при этом субъект не может стать каналом утечки информации сверху вниз.

По аналогии со свойствами классической модели БЛ определяются ss – свойство, * - свойство и свойство безопасности для состояния, реализации и системы в целом.

Теорема А1 – RW. Система ∑ (V, T, z₀) обладает ss – свойством для любого начального состояния z₀, обладающего ss – свойством, тогда и только тогда, когда функция переходов T(q, v) = v* удовлетворяет условиям:

Условие 1. Если (s, o, read) b* \ b, то f_s*(s) = f_o*(o)

Условие 2. Если (s, o, read) b и f_s*(s) < f₀* (o), то (s, o, read) b*

Доказательство. Аналогично доказательству теоремы А1.

Теорема А2 - RW. Система ∑ (V, T, z₀) обладает * - свойством для любого начального состояния z₀, обладающего * - свойством, тогда и только тогда, когда функция переходов T(q, V) = v* удовлетворяет следующим условиям:

Условие 1. Если { (s, x, read), ( s, y, write) }≤ b* \ b, то f₀*(y) = f₀*(x)

Условие 2. Если { (s, x, read), (s, y, write) } ≤ b и f₀*(y) < f₀*(x), то { (s, x, read), (s, y, write) } ≠ b*

Доказательство. Аналогично доказательству теоремы А1.

Теорема BST-RW. Система ∑ (V, T, z₀) безопасна для безопасного начального состояния z₀, тогда и только тогда, когда выполнены условия теоремы А1-RW и теоремы А2-RW.

Доказательство. Теорема BST-RW следует из теоремы А1-RW, F2-RW.

В данном подходе * -свойство определено таким образом, что его смысл – предотвращение возникновения информационных каналов сверху вниз становится более ясным, чем при использовании функции f_c в классической модели БЛ. В этом заключена основная ценность подхода Read-Write.

Подход Transaction ( T )

В данном подходе используются определения безопасных состояния, реализации и системы подхода Read-Write. Однако в подходе Transaction основной акцент делается на определении свойств безопасности функции переходов T. При этом на T накладывается дополнительное ограничение: за один шаг работы системы вносится только одно изменение в один из параметров, т.е. изменяется на один элемент множество доступов или одно из значений одной из функций. При этом остальные параметры остаются неизменными.

Определение 20. Функция переходов T(q, (b, f)) = (b*, f*) обладает ss – свойством, если выполнены условия:

• если (s, o, read) b* \ b, то f_s(s) = f₀(o) и f* = f
• если f_s(s) ≠ f_s*(s), то f₀* = f₀, b* = b и (s, o, read) b, где f_s*(s) < f₀(o)
• если f₀(o) ≠ f₀*(o), то f_s* = f_s, b* = b и (s, o, read) b, где f_s(s) < f₀*(o)

Определение 21. Функция переходов T(q, (b, f)) = (b*, f*) обладает * - свойством, если выполнены условия:

• если { (s, x, read), (s, y, write) } ≤ b* и { (s, x, read), (s, y, write) } ≠ b, то f₀(y) ≥ f₀(x) и f = f*
• если f₀(y) ≠ f₀(y), то b = b*, или { (s, x, read), (s, y, write) } ≠ b, где f₀*(y) < f₀(x), или { (s, x, read), (s, y, write) } ≠ b, где f₀(y) < f₀*(x)

Определение 22. Функция переходов T безопасна, если она обладает ss – свойством и * - свойством.

Теорема BST-T. Система ∑ (V, T, z₀) безопасна для безопасного начального состояния z₀, ее функция переходов безопасна.

Доказательство. По аналогии с доказательством теоремы А1 необходимо показать, что если функция переходов T(q, (b, f)) = (b*, f*) безопасна, то состояние (b*, f*) безопасно в смысле, определенном в подходе Read-Write. Этот факт, очевидно, следует из условий определений 20 и 21. Таким образом, при безопасном начальном состоянии любая реализация системы, а следовательно, и система в целом будут безопасными.

В рамках подхода Transaction можно рассмотреть вопрос о возможностях смены уровня безопасности субъектов и объектов. Пусть для любого x S, c_c(x) ≤ S - множество субъектов, имеющих право менять уровень допуска субъекта x, для любого y O, c₀(y) ≤ S-множество субъектов, имеющих право менять гриф секретности объекта y. В этом случае в функции переходов необходимо внести еще один параметр, определяющий субъекта, дающего запрос системе.

Определение 23. Функция переходов T(s, q, (b, f)) = (b*, f*) безопасна в смысле изменения уровней, если выполнены условия:

• если f_s*(x) ≠ f_s(x), то s c_s(x)
• если f₀*(x) ≠ f₀(x), то s c₀(y)

Таким образом, задавая множества c₀(y) и c_s(x), можно рассматривать случаи, когда все субъекты могут менять уровни безопасности, никто не может, или только системный администратор может менять уровни безопасности.

Проблемы использования модели БЛ

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

Пример 1. Временный канал утечки информации

Пусть:

F₁ – секретный файл, который может содержать или запись "A" или запись "B"

F₂ - несекретный файл

S₁ – субъект, работающий по программе:

Process S₁ ( F₁ : file )
   Open F₁ for read
   While F₁ = "A" Do End
   Close F₁
end;

S₂ – субъект злоумышленник, работающий по программе:

Process S ( F₁ : file, F₂ : file )
   Start S₁ ( F₁ )
   Wait 10 seconds
   Open F₂ for write
   if stop S₁ then write "B" to F₂
   else Write "A" to F₂
   Close F₂
  End;

Субъект - злоумышленник S₂, не открывая на чтение секретные файлы, запускает процесс S₁ и в зависимости от результатов его выполнения ( процесс S₁ либо сразу завершится, либо "зависнет" ) записывает информацию в несекретный файл. При этом предполагается, что злоумышленник S₂ имеет уровень доступа секретно, так как S₁ наследует права запустившего его процесса.

Пример 2.Каналы утечки информации через локальную и логическую переменные.

Пусть F₁и F₂ - секретный и несекретный файлы соответственно. Приведенные ниже процедуры реализуют каналы утечки информации через локальную переменную ( процедура P₁ ) и логическую переменную ( процедура P₂ ).

Procedure P₁ ( F₁ : file, F₂ : file )
   Open F₁ for read
   Read A from F₁
   Close F₁
   Open F₂ for write
   Write A to F₂
   Close F₂
End

Считаем, что файл F₁ может содержать либо запись “A” либо запись “B”.

Procedure P₂ ( F₁ : file, F₂ : file )
   Open F₁ for read
   if F₁ = “A” then
     Close F₁
     Open F₂ for write
     Write “A” to F₂
  else
     Close F₁
     Open F₂ for write
     Write “B” to F₂
   Close F₂
End

Для предотвращения возникновения каналов утечки информации через локальные или логические переменные при написании программ можно предложить руководствоваться следующими рекомендациями:

• открывать все файлы, необходимые для работы программы вначале ее выполнения
• закрывать все файлы в конце выполнения программы
• непосредственную обработку информации из открытых файлов осуществлять во внутренних процедурах, использующих только локальные переменные

Таким образом, без дополнительных уточнений свойств безопасности и порядка написания кода программ классическая модель БЛ не способна предотвратить возникновение некоторых каналов утечки информации. В тоже время слишком строгая политика безопасности может привести к трудностям или даже невозможности практического использования системы защиты. Кроме того, как уже отмечалось выше, доопределение и усложнение свойств безопасности также несет в себе скрытую угрозу.

Модель Low-Water-Mark ( LWM )

Модель LWM представляет близкий к модели БЛ подход к определению свойств системы безопасности, реализующей мандатную ( полномочную ) политику безопасности. В модели LWM предлагается порядок безопасного функционирования системы в случае, когда по запросу субъекта ему всегда необходимо предоставлять доступ на запись в объект.

Пусть определены конечные множества:

S – множество субъектов системы

O – множество объектов системы

R = {read, write} – множество видов доступа субъектов из S к объектам из O

Обозначим:

B = {b ≤ S × O × R} – множество возможных множеств текущих доступов в системе

L – множество уровней секретности

(f_s, f₀) F = L^s × L⁰ – двойка функций (f_s, f₀), определяющих: f_s: S → L – уровень допуска субъектов и f₀: O → L – уровень секретности объекта

V = B × F – множество состояний системы

W ≤ OP × V × V – множество действий системы, где тройка (op, (b, f ), (b*, f*)) W означает, что система в результате выполнения операции op OP перешла из состояния (b, f) в состояние (b*, f*)

Множество OP содержит операции Read, Write, Reset описанные в таблице 4.3

Операции	Условия выполнения	Результат выполнения операции
Read(s, o)	fs(s) ≥ f0(o)	f* = f b* = b { (s, o, read) }
Write(s, o)	fs(s) = f0(o)	fs* = fs для любого o’ ≠ o f0*(o’) = f0(o’), f0*(o’) = fs(s), if (f0*(o’) < f0(o’)) then    o =0,    b* = b { (s, o, read ) }
Reset(s, o)	fs(s) > f0(o)	fs* = fs для любого o’ ≠ o. f0*(o’) = f0(o’), f0*(o) = max(L)

Таблица 4.3

В результате выполнения операции Write уровень секретности объекта снижается до уровня доступа субъекта. Если это снижение реально происходит, то вся информация в объекте стирается. В результате выполнения операции Reset уровень секретности объекта становится максимально возможным в системе.

Дадим определения ss - свойства и * - свойства для модели LWM.

Определение 24. Доступ (s, o, r) S × O × R обладает ss – свойством относительно f F, если r {read, write} и f_s(s) ≥ f₀(o).

Определение 25. Доступ (s, o, r) S × O × R обладает ss – свойством относительно f F, если он удовлетворяет одному из условий:

• r = read и f_s(s) ≥ f₀(o)
• r = write и f_s(s) = f₀(o)

Определение 26. Состояние системы (b, f) V обладает ss - свойством ( * - свойством ), если каждый элемент (s, o, r) b обладает ss - свойством ( * - свойством ) относительно f.

Определение 27. Состояние системы называется безопасным, если оно обладает ss - свойством и * - свойством одновременно.

Утверждение 1. Операции Read, Write, Reset переводят систему из безопасного состояния в безопасное состояние.

Доказательство. Из описания операций Read, Write, Reset следует, что в результате их выполнения новое состояние системы обладает ss – свойством и * - свойством.

Заметим, что условие стирания информации при выполнении операции Write является существенным. Хотя при его отсутствии утверждение 1 формально останется истинным. Однако в этом случае с позиций здравого смысла система не будет безопасной, так как возможно возникновение канала утечки информации. Субъект, запрашивая доступ на запись в объект, понижает его уровень секретности, после чего он может запросить доступ на чтение из этого объекта.

Данный пример еще раз демонстрирует уязвимость определения безопасности в модели БЛ.