Модель безопасности Белл-Ла Падула

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

Рассмотрим систему из двух файлов и двух процессов (рис.2). Один файл и один процесс являются несекретными, другой файл и процесс - секретными.

Простое правило безопасности предотвращает чтение секретного файла несекретным процессом. Оба процесса могут читать и записывать данные в несекретный файл. Однако, легко может произойти нарушение правил управления доступом, если секретныйпроцесс считает информацию из секретного файла и запишет ее в несекретный файл. Это эквивалентно неавторизованному уменьшению класса доступа информации, хотя при этом не изменяется класс доступа ни одного файла.

Рис.2

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

Таким образом, модель многоуровневой безопасности имеет два основных свойства:

· простая безопасность: субъект может только читать объект, если класс доступа субъекта доминирует над классом доступа объекта. Другими словами, субъект может читать "вниз", но не может читать "вверх";

· свойство ограничения: субъект может только записать в объект, если класс доступа субъекта превосходит класс доступа объекта. Субъект может записывать "вверх", но не может записать "вниз".

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

При формализации многоуровневого управления безопасностью, модель Белл-Ла Падула определяет структуру класса доступа и устанавливает упорядочивание отношений между классами доступа (доминирование). Кроме того определяются два уникальных класса доступа: SYSTEM HIGH, который превосходит все остальные классы доступа, и SYSTEM LOW, который превосходят все другие классами. Изменения классов доступа в рамках модели Белл-Ла Падула не допускаются.

		Нарушение свойства ограничения

Рис.3.

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

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

Управление при помощи меток безопасности усиливает ограничение предоставляемого доступа на основе сравнения атрибутов класса доступа субъектов и объектов.

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

Разработка и доказательство модели управления доступом системы является важным этапом в формальном методе разработки системы. Сам формальный метод разработки можно ограничить этапом формального моделирования, после которого следует практическая реализация системы.

В более полном варианте метод формальной разработки включает также этап создания формальной спецификации. Спецификация отличается от модели тем, что помимо переменных и функций, относящихся к обеспечению безопасности, описывает переменные и функции, реализующие в системе иные задачи. При этом следует отметить, что соответствие формальной спецификации разработанной ранее модели безопасности строго доказывается. (18)