Кратко

  • В работе 1976 года Dorothy E. Denning задаёт частичный порядок классов безопасности и использует их наименьшую верхнюю грань — join — для результата, зависящего от нескольких входов.
  • Учитываются явные передачи и неявные зависимости через условия, но доказательство охватывает только объявленные классы и потоки, выраженные семантикой программы.
  • Скрытые каналы, ошибочные метки, дефекты реализации и необоснованное рассекречивание требуют других доказательств. Успех решёточной проверки не является вердиктом о всей системе.

Если результат зависит от двух входов, какой класс он должен получить? В статье “A Lattice Model of Secure Information Flow” Dorothy E. Denning предлагает взять наименьший класс, которого разрешено достичь обоим входам. Это наименьшая верхняя грань, или join.

Запись A → B означает: информации класса A разрешено течь в B. Отношение рефлексивно, транзитивно и антисимметрично, то есть образует частичный порядок. Два изолированных класса могут быть несравнимы, но иметь общий верхний класс. Для c, зависящего от a и b, условие выглядит как class(a) join class(b) → class(c).

Так политика становится проверяемой. Однако формула не утверждает, что c безопасен в реальной среде. Она устанавливает разрешение при данных метках и порядке.

Влияние важнее копирования

Поток возникает, когда одна информация влияет на другую. b := a — явная передача. В конструкции if a = 0 then b := c итоговое состояние b может показать, было ли истинно условие о a. Значит, существует неявный поток от a к b, хотя значение a не копируется.

Современные системы также сообщают через ветвления, ошибки, счётчики и время. Перечня разрешений на чтение недостаточно: нужно учитывать все моделируемые причины изменения выхода.

Классы переменных, выражений и управляющих условий можно распространять до запуска программы и отклонять запрещённые назначения. Работа “Certification of Programs for Secure Information Flow” подробно развивает этот механизм.

Здесь важна точная атрибуция. Решёточная модель 1976 года — индивидуальная работа Dorothy E. Denning. Статья о сертификации написана Dorothy E. Denning вместе с Peter J. Denning и опубликована в 1977 году после Purdue Technical Report 76-181. Смешение текстов стирает соавторство и исторический переход от модели к методу проверки.

Где заканчивается доказательство

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

Метки тоже могут быть неверны. Если секрет отмечен как публичный, анализ корректно разрешит нежелательный поток. Есть и обратное давление: разрешение только восходящих потоков ведёт к чрезмерной классификации. Совместный обзор “Data Security” обсуждает санкционированное понижение класса и программы, теряющие информацию. Но для них нужны отдельные полномочия и доказательства того, что именно удалено.

Время и потребление ресурсов могут передавать сигнал без обычного присваивания. Формально разрешённый выход может попасть на слабую конечную точку или в сервис, снимающий метку. Модель не обещала закрыть эти риски; ошибка возникает при расширении её вывода.

В выступлении 1999 года “The Limits of Formal Security Models” Denning подчёркивает: формальные методы работают внутри упрощённой модели и предположений, а реальные атаки часто выходят за рамки. Это довод за точную формулировку сертификата, а не против формальных методов.

Сертификат как звено

Ответственная система связывает результат с версией политики и joins, происхождением меток, покрытием анализатора и точной цепочкой исходник–компилятор–бинарный файл–развёртывание. Рассекречивание имеет собственные полномочия и журнал. Исполнение и конечные точки сохраняют ограничения. Боковые каналы проверяются отдельно.

Bell–LaPadula относится к соседней истории многоуровневой безопасности и упомянута в ссылках Denning, но не заменяет её аргумент. Контроль доступа спрашивает, может ли субъект выполнить действие. Решётка потоков спрашивает, какой класс наследует результат от всей влияющей информации.

Поэтому модель остаётся полезной: она точно доказывает одно существенное свойство и не даёт спрятать за ним остальные вопросы.

Источники