«Вот тебе, казалось бы, абсолютная противоположность: одна модель говорит, что нельзя читать выше своего уровня, другая запрещает писать ниже. Но в основе обеих лежит один и тот же формальный аппарат, и их доказательства свойств, это не магия, а последовательное применение правил к математическим объектам. Я хочу показать, как переход от бытовых описаний к решёткам и свойствам *-свойства открывает путь к проектированию систем, безопасность которых можно не ‘надеяться’, а проверить».
Зачем формальные модели там, где хватает здравого смысла
Идея разграничения доступа на основе уровней доверия интуитивно понятна. Есть секретные данные, и есть люди с разным допуском. Проблема в том, что интуиция и здравый смысл — ненадёжные союзники в системах с миллионами строк кода и тысячами пользователей. Формальная модель переводит интуицию на язык математики. Она превращает «ну не должен он туда писать» в набор однозначных правил и условий, соблюдение которых можно проверить алгоритмически.
Ценность моделей Bell-LaPadula и Biba не только в самих правилах, которые часто упоминаются поверхностно, а в доказательстве того, что система, построенная по этим правилам, действительно обладает ключевыми свойствами безопасности. Без этого доказательства модель остаётся лишь красивой идеей.
Математический каркас: решётки и состояния системы
Прежде чем говорить о правилах чтения и записи, нужно определить, из чего состоит система. В основе обеих моделей лежит концепция «состояния». Состояние системы в любой момент времени, это снимок всех её компонентов.
Три ключевых множества описывают состояние:
- S — субъекты. Активные сущности: пользователи, процессы, потоки. Они инициируют операции.
- O — объекты. Пассивные сущности: файлы, записи в БД, сегменты памяти. Это то, над чем производятся операции.
- A — матрица доступа. Таблица, определяющая, какие права доступа (например, чтение, запись, исполнение) есть у каждого субъекта на каждый объект. Она динамична и может меняться в процессе работы системы.
Все субъекты и объекты получают метки безопасности — значения из упорядоченного множества, часто представляющего собой решётку. Решётка, это не просто линейная шкала «низкий-средний-высокий». Это частично упорядоченное множество, где для любых двух элементов можно однозначно определить их наименьшую верхнюю и наибольшую нижнюю границы. Это позволяет моделировать не только иерархические уровни (совершенно секретно, секретно, для служебного пользования), но и разделение на категории (финансы, НИОКР, кадры), комбинируя их.
Цель Bell-LaPadula: предотвращение утечки
Модель Bell-LaPadula (BLP) создавалась для задач сохранения государственной тайны. Её главный враг — несанкционированное распространение информации «вверх», от обладателя высокой метки к субъекту с низкой. Модель решает эту задачу двумя базовыми свойствами.
Простое свойство безопасности (ss-свойство)
Простое свойство безопасности (simple security property) — прямой запрет на чтение «сверху». Формально: субъект с меткой L может читать объект с меткой L’ только если L’ ≤ L (метка объекта доминируется меткой субъекта). Читать можно только то, что находится на своём уровне или ниже. Солдат не может прочитать приказ генерала.
Свойство * (star-property)
*-свойство (star-property) сложнее и направлено против скрытых каналов утечки через запись. Оно гласит: субъект с меткой L может записывать в объект с меткой L’ только если L’ ≥ L (метка объекта доминирует метку субъекта). Писать можно только на свой уровень или выше. Это предотвращает сценарий, когда высокопоставленный сотрудник, считав секретные данные, запишет их в файл с низкой грифованностью, откуда их сможет прочитать неавторизованное лицо.
Важное уточнение: *-свойство в классической модели применяется не ко всем субъектам, а только к тем, кто работает в «режиме доверия». В упрощённых интерпретациях это различие часто стирается.
Цель Biba: защита от компрометации данных
Если BLP защищает конфиденциальность, то модель Biba — её зеркальное отражение — защищает целостность данных. Проблема здесь иная: как не дать ненадёжному (с низкой меткой целостности) субъекту испортить важные (с высокой меткой) данные. В системах управления технологическими процессами или финансовых транзакциях это критически важно.
Простое свойство целостности
Простое свойство целостности в модели Biba: субъект с меткой целостности I может модифицировать (писать в) объект с меткой I’ только если I ≥ I’. Записывать можно только в объекты с уровнем целостности, равным или ниже своего. Высоконадёжный процесс не должен перезаписываться кодом из сомнительного источника.
Свойство целостности *
*-свойство для целостности: субъект с меткой I может читать объект с меткой I’ только если I’ ≥ I. Читать можно только данные с уровнем целостности, равным или превышающим свой собственный. Это защищает от ситуации, когда надёжный субъект, считав «грязные» данные, на их основе примет некорректное решение и испортит важный объект.
Механизм доказательства: инварианты безопасности и теоремы
Как доказать, что система, следующая этим правилам, действительно безопасна? Доказательство строится на концепции инварианта безопасности. Инвариант, это утверждение о состоянии системы, которое истинно в её начальном, безопасном состоянии и остаётся истинным после применения любого разрешённого системой перехода (операции).
Для BLP таким инвариантом является утверждение: «В системе не существует информационного потока от объекта с высокой меткой к субъекту с низкой меткой». Начальное состояние считается безопасным (потоков нет). Далее доказывается, что каждая возможная операция в системе (чтение, запись, изменение прав) не нарушает этот инвариант, если она следует правилам ss- и *-свойства.
Доказательство проводится методом от противного. Предполагается, что в безопасном состоянии инвариант выполняется, но после некой операции он нарушается. Затем анализируется, какая операция могла привести к нарушению. Например, если появился поток от высокого объекта к низкому субъекту, это могло случиться только через операцию чтения. Но операция чтения разрешена только если соблюдается ss-свойство (L’ ≤ L), что по условию не позволяет считать объект с более высокой меткой. Возникает противоречие, значит, наше предположение о нарушении инварианта ложно. Таким образом, инвариант сохраняется.
Строгость и практические ограничения моделей
Формальная строгость BLP и Biba имеет свою цену. Модели не учитывают ряд практических аспектов, что ограничивает их прямое применение в чистом виде.
| Аспект | Проблема в BLP/Biba | Следствие |
|---|---|---|
| Совмещение свойств | Модели BLP (конфиденциальность) и Biba (целостность) в чистом виде несовместимы. Если ввести единую решётку, правила чтения/записи одной модели будут нарушать правила другой. | Необходимость компромиссов, гибридных моделей или разделения политик. |
| «Благонадёжные» субъекты | Для работы системы (например, для запуска служб) нужны субъекты, которым разрешено всё. В BLP это нарушает *-свойство, что требует ослабления модели. | Модель описывает идеал, от которого приходится отступать при реализации. |
| Временные характеристики | Модели статичны, они не учитывают время. Атаки, основанные на времени выполнения или состоянию системы в определённый момент, ими не обнаруживаются. | Охват угроз ограничен классом угроз, связанных с прямым доступом. |
| Сложность управления | Жёсткие правила затрудняют совместную работу. Для передачи данных с высокого уровня на низкий требуется специальный механизм (например, «санация» данных доверенным субъектом). | Снижение гибкости и производительности труда. |
Наследие и влияние: от теории к российским стандартам
Формальные модели BLP и Biba не остались академическим курьёзом. Их принципы и, что важнее, методология доказательства свойств легли в основу современных стандартов и подходов к безопасности, включая российскую регуляторику.
Требования к системам защиты информации, обрабатывающим государственную тайну, прямо отсылают к идеям многоуровневого контроля доступа. При сертификации средств защиты информации по требованиям ФСТЭК России (в рамках 152-ФЗ и отраслевых стандартов) оценивается не только наличие механизмов разграничения, но и корректность их реализации — то есть их соответствие заявленной политике безопасности. Эта проверка по сути является эмпирической проверкой того, что система не нарушает инварианты, заложенные в её модель безопасности.
Более того, подход с формальным описанием политики, субъектов, объектов и правил перехода стал основой для таких концепций, как мандатный контроль доступа (МКД), который является обязательным для систем высоких классов защиты. Современные средства анализа защищённости и верификации кода также используют формальные методы, восходящие к той же логике: определить желаемое свойство (инвариант) и доказать, что код его не нарушает.
Вместо заключения: формальность как инструмент, а не догма
Bell-LaPadula и Biba — не инструкции по сборке. Это строгие математические конструкции, демонстрирующие, как можно рассуждать о безопасности системно. Их главный урок в том, что проектирование безопасности должно начинаться с формулировки чётких, формализуемых свойств («никаких утечек сверху вниз»), а уже потом — с поиска механизмов их обеспечения.
В реальных проектах редко реализуют «канонический» BLP. Но понимание его доказательной базы позволяет осознанно отступать от идеала, взвешивая риски. Когда архитектор решает ослабить *-свойство для служебного процесса, он должен понимать, какую именно брешь в инварианте безопасности это создаёт и какие компенсирующие меры необходимы. Формальные модели превращают безопасность из набора запретов в инженерную дисциплину, где каждое решение имеет измеримые последствия.