Модель Белла-ЛаПадула. 
Информационная безопасность

Классической мандатной моделью безопасности является модель Белла-ЛаПадула. В ней для описания системы используются:

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

О — множество объектов (например, множество файлов);

L — линейно упорядоченное множество уровней безопасности (например, «общий доступ», «для служебного пользования», «секретно», «совершенно секретно»);

F: S и О -> L — функция, определяющая уровень безопасности субъекта или объекта в данном состоянии;

V — множество состояний — множество упорядоченных пар (F, М), где М — матрица доступа субъектов к объектам (матрица, строки которой соответствуют субъектам системы, столбцы — объектам, элемент матрицы M_so, далее обозначаемый как M[s, о], описывает права на доступ субъекта s к объекту о).

Система описывается начальным состоянием v₀eV, множеством запросов R и функцией переходов Т: ('V х R) —> V, описывающей переход системы из состояния в состояние под действием запроса.

В модели Белла-ЛаПадула вводится определение двух свойств безопасности системы: безопасность по чтению и безопасность по записи.

Состояние (F, М) безопасно по чтению тогда и только тогда, когда для V s е S, V о е О выполняется требование: чтение е M[s, о] => F (s) > F (o),.

т. е. субъект s может прочитать информацию из объекта о, только если уровень секретности о меньше или равен уровню доступа s. Данное свойство безопасности также называется правилом запрета чтения с верхнего уровня.

Состояние (F, М) безопасно по записи тогда и только тогда, когда для V s е S, V о е О выполняется требование: запись е Mfs, ol => F (o) > F (s),.

т. е. субъект s может записать информацию в объект о, только если уровень секретности о выше или равен уровню доступа s. Данное свойство безопасности также называется правилом запрета записи на нижний уровень.

Состояние системы veV безопасно тогда и только тогда, когда оно безопасно и по чтению, и по записи.

Система (v₀. R, Т) безопасна тогда и только тогда, когда ее начальное состояние v₀ безопасно и любое состояние, достижимое из v₀ после выполнения конечной последовательности запросов из R, также безопасно.

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

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

Система (v₀, R. Т) (т. е. система с начальным состоянием v₀, множеством запросов R, функцией переходов Т) безопасна тогда и только тогда, когда сосгояние v₀ безопасно, и функция переходов Т такова, что для V veV, досгижимого из состояния v₀ после выполнения конечной последовательности запросов из R (таких что T (v, г) = v*, где v = (F, М) — исходное состояние, v*= (F*, М*) — состояние после перехода), для V s е S, V о е О выполняются следующие условия:

• — если чтениееМ |s, o] и 4TeHHegM|s, o], то F'(s)>F*(o);
• — если 4TenHeeM|s, o] и F*(s)
• — если запись е M*[s, о] и запись g M[s, о], то F*(o) > F (s);
• — если запись е M|s, о] и F*(o) < F*(s), то запись M*[s, о).

Кратко рассмотрим доказательство теоремы.

Необходимость. Если система безопасна, то начальное состояние v₀ безопасно по определению. Пусть существует некоторое состояние v*, достижимое из v₀ путем выполнения конечного числа запросов из R и полученное в результате перехода из безопасного состояния v: T (v, г) = v*. Тогда, если при таком переходе нарушено хотя бы одно из первых двух ограничений, накладываемых теоремой на функцию Т, то состояние v' не будет безопасным по чтению. Если функция Т нарушает одно из двух последних условий теоремы, то состояние v не будет безопасным по записи. Таким образом, при нарушении условий теоремы система становится небезопасной. Необходимость доказана.

Достаточность. Используем метод доказательства от противного. Пусть система небезопасна. В этом случае либо начальное состояние v₀ небезопасно, что противоречит условиям теоремы, либо должно существовать небезопасное состояние v', достижимое из безопасного начального состояния v₀ путем выполнения конечного числа запросов из R. В этом случае обязательно будет иметь место переход T (v, г) = v*, при котором состояние v — безопасно, a v* — нет. Однако четыре условия теоремы делают такой переход невозможным.

Несмотря на достоинства модели Белла-ЛаПадула, при ее строгой реализации в реальных АС возникает ряд проблем.

• 1. Завышение уровня секретности, связанное с одноуровневой природой объектов и правилом безопасности по записи. Если субъект с высоким уровнем доступа хочет записать что-то в объект с низким уровнем секретности, то сначала приходится повысить уровень секретности объекта, а потом осуществлять запись. Таким образом, даже один параграф, добавленный в большой документ субъектом с высоким уровнем доступа, повышает уровень секретности всего этого документа. Если по ходу работы изменения в документ вносят субъекты со все более высоким уровнем доступа, уровень секретности документа также постоянно растет.
• 2. Запись вслепую. Эта проблема возникает, когда субъект производит операцию записи в объект с более высоким уровнем безопасности, чем его собственный. В этом случае после завершения операции записи субъект не сможет проверить правильность выполнения записи при помощи контрольного чтения, так как ему это запрещено в соответствии с правилом безопасности по чтению.
• 3. Проблема удаленного чтения-записи. В распределенных системах при удаленном чтении файла создаются два потока: от субъекта к объекту (запросы на чтение, подтверждения, прочая служебная информация) и от объекта к субъекту (сами запрашиваемые данные). При этом, например, если F (s) > F (o), то первый поток будет противоречить свойству безопасности по записи. На практике для решения этой проблемы надо разделять служебные потоки (запросы, подтверждения) и собственно передачу информации.

А. Доверенные субъекты. Модель Белла-ЛаПадула не учитывает, что в реальной системе, как правило, существуют субъекты, действующие в интересах администратора, а также системные процессы, например, драйверы. Жесткое соблюдение правил запрета чтения с верхнего уровня и запрета записи на нижний уровень в ряде случаев делает невозможной работу подобных процессов. Соответственно, их также приходится выделять.