ТОКБ

81. Математические методы анализа политики безопасности. Модель Белла - Лападула (б-л).

Модель Б-Л построена для обоснования безопасности систем, использующих политику MLS. Материалы, в которых опубликована модель в 1976г., до сих пор недоступны. Поэтому в изложении модели Б-Л будем следовать работе J. McLean (1987), в которой классы объектов предполагаются неизменными. Для описания модели нам потребуется несколько другое описание самой вычислительной системы. Пусть определены конечные множества S, О, R, L.

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

О - множество объектов, не являющихся субъектами;

R - множество прав доступа; R = {read (r), write(w), execute (е), append (а)};

L - уровни секретности.

Множество V состояний системы определяется произведением множеств:

где сомножители определяются следующим образом. В - множество текущих доступов и есть подмножество множества подмножеств произведения . Множество подмножеств будем обозначатьэлементы множестваВ будем обозначать b и они представляют в текущий момент t графы текущего доступа (в каждый момент субъект может иметь только один вид доступа к данному объекту).

М - матрица разрешенных доступов, M=|M_i_j|, M_ijR. F - подмножество множества , где каждый, - вектор, который состоит из трех компонент, каждая из которых тоже вектор (или отображение).

f_s - уровень допуска субъектов (это некоторое отображение f: S->L);

f_o - уровень секретности объектов (это некоторое отображение f: O->L);

f_c - текущий уровень секретности субъектов (этотоже некоторое отображение f_c: S->L).

Элементы подмножества F, которые допущены для определения состояния, должны удовлетворять соотношению:

Н - текущий уровень иерархии объектов, в работе McLean этот уровень не изменяется, совпадает с f₀и далее не рассматривается.

Элементы множества V состояний будут обозначаться через v. Пусть определены множество Q - запросов в систему и множество D - решений по поводу этих запросов (D = {yes, nо, error}). Определим множество W действий системы как

Каждое действие системы (q, d, v₂, v₁) имеет следующий смысл: если система находилась в данный момент в состоянии v₁, поступил запрос q, то принято решение d и система перешла в состояние v₂.

Пусть Т - множество значений времени (для удобства будем считать, что T=N - множество натуральных чисел). Определим набор из трех функций (х, у, z)

x: T->Q,

у: T->D,

z: T->V,

и обозначим множества таких функций X, Y, Z соответственно.

Рассмотрим и определим понятие системы в модели Б-Л.

Определение. Системой (Q, D, W, z₀) называетсяподмножество такое,что,

(x, y, z)(Q, D, W, z₀)(x_t, y_t, z_t, z_t_-1)W

для каждого значения tT, где z₀- начальное состояние системы.

Определение. Каждый набор (х, у, z)(Q, D, W, z₀) называется реализацией системы.

Определение. Если (х, у, z) - реализация системы, то каждая четверка (x_t, y_t, z_t, z_t_-1) называется действием системы.

Нетрудно видеть, что при отсутствии ограничений на запросы таким образом определен некоторый автомат, у которого входной алфавит Q, а выходной D, а множество внутренних состояний V. Автомат задается множеством своих реализаций. Перейдем к определению понятий, связанных с безопасностью системы.

Определение. Тройка (S, О, X)SOR удовлетворяет свойству простой секретности (ss-свойство) относительно f, если X=execute, или X=append, или, если X=read и f_s(S)>f_o(0), или X=write и f_s(S)>f₀(S).

Определение. Состояние v=(b, М, f, h) обладает ss-свойством, если для каждого элемента (S,О,Х)B этот элемент обладает ss-свойством относительно f.

Определение. Состояние v=(b, М, f, h) обладает *-свойством, если для каждого (S, О, X)B при X=write текущий уровень субъекта f_c(S) равен уровню объекта f₀(O), или при X=read f_c(S)>f₀(O), или при X=append f_o(O)>f_c(S).

Определение. Состояние обладает *-свойством относительно множества субъектов S', S'S, если оно выполняется для всех троек (S, О, X) таких, что SS'

Определение. Субъекты из множества S\S' называются доверенными.

Лемма. Из * -свойства для состояния v=(b, М, f, h) следует ss-свойство относительно f для всех (S, О,Х)B.

Доказательство. Утверждение следует из условия f_s(S)>f_c(S).

Определение. Состояние v=(b, М, f, h) обладает ds -свойством, если (S, О, X)b=>Xm_so, где M=||m_so||- матрица доступа состояния v.

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

Напомним формулировку политики MLS, связанной с решеткой ценностей SCL, где L - линейный порядок, SC - решетка подмножеств в информации: информационный поток между двумя объектами называется разрешенным, если класс объекта источника доминируется классом объекта получателя. Из определения ss-свойства следует, что в безопасном состоянии возможно чтение вниз, что согласуется с эквивалентным определением MLS политики. Кроме того, ss-свойство определяет ограничение на возможность модификации, которое связано с write:

fs(S)>fo(0).

Объясним *-свойство. Если субъект может понизить свой текущий допуск до f_c(S)=f₀(O), то, согласно *-свойству, он может писать в объект. При этом он не может читать объекты на более высоких уровнях, хотя допуск f_s(S) ему это может позволить. Тем самым исключается возможный канал утечки:

High O f_s(S)

| r

Low S ---- O₂f_c(S)

Таким образом, при записи информационный поток опять не может быть направлен вниз. Исключение возможно только для доверенных субъектов, которым разрешено строить информационный поток вниз. При этом доверенность субъекта означает безопасность такого потока вниз (поэтому эти потоки считаются разрешенными). Сказанное выше означает, что безопасное состояние модели Б-Л поддерживает политику MLS. Значит, для того, чтобы доказать, что любой поток на траектории вычислительной системы разрешен, достаточно показать, что выходя из безопасного состояния и следуя допустимым действиям мы опять приходим в безопасное состояние, тем самым любая реализация процесса будет безопасной. Проведем строгое обоснование этого вывода.

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

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

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

Теорема A1. (Q, D, W, z₀) обладает ss -свойством для любого начального z₀, которое обладает ss-свойством тогда и только тогда, когда W удовлетворяет следующим условиям для каждого действия (q, d, (b*, М*, i*, h*), (b, М, f, h)):

(I) (S, 0, X)b*| b обладает ss-свойством относительно f*.

(2) если (S, О, X)b и не обладает ss-свойством относительно f*, то (S, О, X)b*

Доказательство. (S, О, Х)b* возможно либо (S,О, Х)b, или (S, О, X)b*\b. Условие (1) означает, что состояние (b*, М*, f*, h*) пополнилось элементами (S, О, X), обладающими ss - свойством относительно f*. Условие (2) означает, что элементы b*, перешедшие из b, обладают ss - свойством относительно f*. Следовательно, (S, О, X)b* обладает ss-свойством относительно f*. Пусть любое состояние обладает ss-свойством относительно своего f. Тогда (1) выполняется, т.к. ss-свойство выполняется для всех (S, О,X) из b*. И, если (S, О, X)b и перешло в b*, то, в силу ss-свойства (S, О, X) обладает ss - свойством относительно f*. Что и требовалось доказать.

Теорема A2. Система (R, D, W, z₀) обладает *- свойством относительно S' для любого начального состояния z₀, обладающего *-свойством относительно S' тогда и только тогда, когда W удовлетворяет следующим условиям для каждого действия (q, d, (b*, М*,f*, h*), (b, М, f, h)):

SS’, (S, O, X)b*\ b обладает *-свойством относительно f*;
SS’, (S, O, X)b и (S, O, X) обладает *-свойством относительно f*, то (S, O, X)b*.

Доказательство проводится аналогично.

Упражнение. Доказать теорему А2.

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

(S, О, X)b*| b то Хт_so*,
(S, 0, X)b*| b Xm_so*, то (S, 0, X)b*

Доказательство проводится аналогично.

Упражнение. Доказать теорему АЗ.

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

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

Содержание