Модель Белла-Ла Падулле

В модели Белла-Ла Падулле по грифам секретности распределяются субъекты и объекты, действующие в системе и при этом выполняются следующие правила:

1. Простое правило безопасности, Simple Security (SS) – Субъект с уровнем секретности Xs может читать информацию из объекта с уровнем секретности X0 тогда и только тогда, когда Xs преобладает над X0; «no read up»

2. * - свойство (property) – субъект с уровнем секретности Xs может писать информацию в объект с уровнем секретности X0 тогда и только тогда, когда X0 преобладает над Xs. «no write down»

S#принадлежит#O

R={r,w} L={u,su,s,ts} (unclassified, sensitive but unclassified, secret, top secret)

#дельта# - решетка уровня секретности.

V – множество состояний системы, представляемое в виде набора упорядоченных пар (F,M)

F: SvO->L, где F – функция уровня секретности, ставящая каждому объекту и субъекту в системе в соответствие определенный уровень секретности.

M = матрица текущих прав доступа

#дельта# (L, <= ,#жирная точка#,#крестик в кружочке#)

<= - оператор, определяющий частичное нестрогое отношение порядка для уровней секретности

#жирная точка# - оператор наименьшей верхней границы

#крестик в кружочке# - оператор наибольшей нижней границы

Отношение, имеющее <=, обладает следующими свойствами:

1. Рефлексивность (#для любых# а #принадлежит# L:а <= а) Разрешена передача информации между субъектами и объектами одного уровня секретности.

2. Антисимметричность (#для любых# а1,a2 #принадлежит# L:(( а1 <= а2)&(a2<=a1))->a2=a1) В данном случае это означает, что информация может передаваться как от субъектов и объектов уровня А к субъектам и объектам уровня В, так и от субъектов и объектов уровня В к субъектам и объектам уровня А, в таком случае эти уровне эквивалентны.

3. Транзитивность (#для любых# а1,a2,a3 #принадлежит# L: (( а1 <= а2)&(a2<=a3))->a1<=a3) Транзитивность означает, что если информация может передаваться от субъектов и объектов уровня А к субъектам и объектам уровня В, а от субъектов и объектов уровня В к субъектам и объектам уровня С, то информация также может передаваться от субъектов и объектов уровня А к субъектам и объектам уровня С.

Операторы наибольшей нижней #крестик в кружочке# и наименьшей верхней #жирная точка# границы определяются следующим образом:

а=а1#жирная точка#a2<=>(а1,a2<=a)&(#любой#a’#принадлежит#L:(a’<=a)->(a’<=a1Va’<=a2))

а=а1#крестик в кружочке#a2 <=> <=>(a<=а1,a2)&(#любой#a’#принадлежит#L:(a’<=a1)&(a’<=a2)->(a’<=a))

Для каждой пары существует единственный элемент наименьшей верхней границы и единственный элемент наибольшей нижней границы.

Система ∑=(V0,R,T) в данной модели состоит из следующих элементов:

V0 – начальное состояние системы

R – множество прав доступа

T:VxR->V – функция перехода, которая в ходе выполнения запросов переводит систему из одного состояния в другое

Изменение состояния системы происходит следующим образом:

Система, находящаяся в состоянии v#принадлежит#V, получает запрос на доступ r#принадлежит#R и переходит в состояние V*=T(v,r). Состояние Vn называется достижимым для системы ∑, если существует последовательность:

{ (Z0,V0),…,(Zn-1,Vn-1),(Zn,Vn)}:T(Zi,Vi)=Vi+1,#любой#i=0,n-1

Начальное состояние V0 является достижимым по определению.

Состояние системы (F,M) называется безопасным по чтению или Simple-безопасным, если для каждого субъекта, осуществляющего в этом состоянии доступ по чтению к объекту, уровень безопасности субъекта доминирует над уровнем безопасности объекта.

#любой#s#принадлежит#S, #любой#o#принадлежит#O, z#принадлежит#M[s,o]->F(o)<=F(s)

#любой#s#принадлежит#S, #любой#o#принадлежит#O, w#принадлежит#M[s,o]->F(s)<=F(o)

Состояние (F,M) называется безопасным по записи в случае, если для каждого субъекта, осуществляющего в этом состоянии доступ по записи к объекту, уровень безопасности объекта доминирует над уровнем безопасности субъекта.

Состояние (F,M) называется безопасным, если оно безопасно по чтению и по записи. Полностью система ∑=(V0,R,T) называется безопасной, если ее начальное состояние V0 безопасно и все состояния, достижимые из V0 путем применения конечной последовательности запросов из R безопасны.

Основная теорема безопасности Беллы-Ла Падулле

Система ∑=(V0,R,T) безопасна тогда и только тогда, когда выполнены следующие условия:

1. Начальное состояние V0 безопасно

2. Для любого состояния V, достижимого из V0, путем применения конечной последовательности запросов из R таких, что T(v,z)=V* v=(F,M) V*=(F*,M) для #любой#s#принадлежит#S, #любой#o#принадлежит#O Выполнены условия:

   1. If z#принадлежит#M*[s,o] и z#не принадлжит#M[s,o] then F*(o)<=F*(s)

   2. If z#принадлежит#M[s,o] и F*(s)< F*(o), then z#не принадлжит#M*[s,o]

   3. If w#принадлежит#M*[s,o] и w#не принадлжит#M[s,o] then F*(s)<=F*(o)

   4. If w#принадлежит#M[s,o] и F*(o)< F*(s), then w#не принадлжит#M*[s,o]

Пусть система ∑=(V0,R,T) безопасна.

V0 безопасно по определению

Предположим, что существует такое безопасное состояние V*, достижимое из состояния V:T(v,r)=V*

Допустим, для данного состояния нарушено одно из условий (a-d), во всех случаях мы получаем противоречия с тем, что состояние V* является безопасным. Покажем достаточность утверждения.

Система ∑=(V0,R,T) может быть небезопасна в двух случаях:

1. В случае, если изначальное состояние V0 небезопасно (противоречит условию теоремы).

2. В случае, если существует небезопасное состояние V*, достижимое из безопасного V0 путем применения конечного числа запросов из R. Это означает, что на каком-то этапе произошел переход Т(v,r)=V*, где v – безопасное состояние, а V* - небезопасное, однако условия (a-d) делают данный переход невозможным.

ЧТД

Формальные модели целостности