П.Н. Девянин - д.т.н., доцент, председатель УМС, УМО по информационной безопасности. E-mail: peter_devyanin@hotmail.com

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