Верификация правил фильтрации с временными характеристиками методом “проверки на модели”

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