Курс лекций Защита Информации/Модель Белла-ЛаПадулы: различия между версиями

Содержимое удалено Содержимое добавлено
Строка 58:
## Если <math> w \mathcal {2} M^*[s,o] </math> и <math>w \notin M[s,o] </math>, то <math> F^*(s) \le F^*(o) </math>
## Если <math> w \mathcal {2} M[s,o] </math> и <math>~F^*(o) < F^*(s) </math>, то <math> w \notin M^*[s,o] </math>
==== Доказательство теоремы ====
 
==== Доказательство теоремы ====
===== Необходимость =====
 
===== Необходимость =====
Пусть система <math> ~\Sigma=( \nu_0, R, T ) </math> безопасна. В этом случае начальное состояние <math> \nu_0\ </math> безопасно по определению. Предположим, что существует безопасное состояние <math> \nu^*\ </math>, достижимое из состояния <math> \nu : ~ T (\nu, r ) = \nu^* </math>, и для данного перехода нарушено одно из условий 1-4. Легко заметить, что в случае, если нарушены условия 1 или 2, то состояние <math> \nu^*\ </math> будет небезопасным по чтению, а если нарушены условия 3 или 4 – небезопасным по записи. В обоих случаях мы получаем противоречие с тем, что состояние <math> \nu^*\ </math> является безопасным.
 
===== Достаточность =====
 
Система <math> ~\Sigma=( \nu_0, R, T ) </math> может быть небезопасной в двух случаях: