Библиография
Аннотация
В статье рассматривается практическая проблема проверки корректности работы средств защиты информации (СЗИ) в сложных программных системах промышленного уровня, таких как операционные системы и системы управления базами данных. Авторы исходят из того, что современные стандарты разработки ПО с высоким уровнем доверия прямо требуют подтверждать соответствие механизмов безопасности формальным моделям, в первую очередь моделям управления доступом. Однако на практике это требование оказывается трудно реализуемым из-за масштаба и сложности реальных программных систем.
Средства защиты информации в таких системах выступают как программные механизмы, встроенные в ядро ОС или СУБД и постоянно участвующими в обработке запросов доступа. Их корректность критична для общей безопасности системы, но формальные модели по требованиям стандартов описываются на высоком уровне абстракции и не отражают напрямую детали реализации. В результате между абстрактным описанием политики безопасности и реальным поведением системы возникает разрыв, обусловленный различием уровней абстракции. Преодоление этого разрыва существенно осложняется масштабом промышленных программных систем, насчитывающих миллионы строк кода, что делает применение классических методов формальной верификации на уровне реализации крайне затруднительным.
Авторы предлагают решать эту проблему с помощью динамической верификации, основанной на анализе фактического поведения системы во время выполнения. Суть подхода заключается в том, что работа всей системы наблюдается и фиксируется в виде трасс событий, после чего эти трассы сопоставляются с поведением, допускаемым формальной моделью управления доступом. Такой подход позволяет проверять соответствие модели и реализации на уровне происходящих операций доступа.
Ключевой сложностью здесь является то, что формальная модель и программная реализация описаны на разных уровнях абстракции. Одному событию в модели может соответствовать цепочка действий в системе, а некоторые системные события вообще не имеют прямого аналога в модели. Для преодоления этого разрыва вводится неклассическое отношение уточнения, реализуемое специальным компонентом-медиатором. Этот компонент преобразует системную трассу в модельную, фактически «поднимая» наблюдаемое поведение реализации до уровня формальной модели управления доступом.