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

Рассказать про эту модель (смотри начало 16 вопроса). Рассказать про систему в модели:

Система ( , , ) 0 Σ = v R T в модели Белла-ЛаПадулы состоит из следующих элементов:

- v0 – начальное состояние системы;

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

- T :V × R →V - функция перехода, которая в ходе выполнения запросов переводит систему из одного состояния в другое.

Изменение состояний системы во времени происходит следующим образом: система, находящаяся в состоянии v∈V , получает запрос на доступ r ∈ R и переходит в состояние v∗ = T(v, r) .

Основная теорема безопасности Белла-ЛаПадулы). Система  Σ = v R T безопасна тогда и только тогда, когда выполнены следующие условия:

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

2. Для любого состояния v, достижимого из v0 путём применения конечной последовательности запросов из R, таких, что T(v, r) = v∗ , v=(F, M) и v∗ = (F∗ ,M ∗ ) , для ∀s∈S,∀o∈O выполнены условия:

1. Если r ∈M∗[s,o] и r ∉M[s,o], то F∗ (o) ≤ F∗ (s) .

2. Если r ∈M[s,o]и F ∗ (s) < F∗ (o) , то r ∉M∗[s,o] .

3. Если w∈M ∗[s,o] и w∉M[s,o] , то F∗ (s) ≤ F ∗ (o) .

4. Если w∈M[s,o] и F ∗ (o) < F∗ (s) , то w∉M ∗[s,o].

Проще: Основная теорема безопасности Белла — Лападулы утверждает, что если информационная система начинает работу из безопасного состояния и переход из состояние в состояние безопасен, то все состояния системы безопасны.  

◄ Пусть система ( , , ) 0 Σ = v R T безопасна. В этом случае начальное состояние v0 безопасно по определению. Предположим, что существует безопасное состояние v∗ , достижимое из состояния v: T(v, r) = v∗ , и для данного перехода нарушено одно из условий 1-4. Легко заметить, что в случае, если нарушены условия 1 или 2, то состояние v∗ будет небезопасным по чтению, а если нарушены условия 3 или 4 – небезопасным по записи. В обоих случаях мы получаем противоречие с тем, что состояние v∗ является безопасным. Докажем достаточность утверждения. Система ( , , ) 0 Σ = v R T может быть небезопасной в двух случаях: 

1. В случае если начальное состояние v0 небезопасно. Однако данное утверждение противоречит условию теоремы.

2. Если существует небезопасное состояние v∗ , достижимое из безопасного состояния v0 путём применения конечного числа запросов из R. Это означает, что на каком-то промежуточном этапе произошёл переход T(v, r) = v∗ , где v – безопасное состояние, а v∗ - небезопасное. Однако условия 1-4 делают данный переход невозможным. ►