Логический анализ корректности конфигурирования межсетевых экранов
1
УДК 004.413
Логический анализ корректности конфигурирования
межсетевых экранов
© В.В. Девятков, Мьо Тан Тун
МГТУ им Н.Э. Баумана, Москва, 105005, Россия
Статья посвящена статическому анализу поиска ошибок конфигурирования меж-
сетевых экранов (брандмауэров). В отличие от известных работ для моделирова-
ния поведения брандмауэров предлагается использовать не списки управления до-
ступом ACL (ACL – Access Control Lists), а процессные модели, выразительные
возможности которых гораздо шире, а теория более развита, что позволяет опи-
сывать гораздо более сложные модели программ конфигурирования. Статический
анализ поиска ошибок предлагается осуществлять методами логического про-
граммирования как доказательство или вывод свойств процессов конфигурирова-
ния, что является гораздо более изящным, полным и не имеющим ограничений под-
ходом проверки корректности конфигурирования брандмауэров. Требования (свой-
ства) корректности предлагается формализовать на языке модальной логики.
Переход от этого формального описания свойств предлагается алгоритмически
формировать как цель в языке ПРОЛОГ. В статье приводятся примеры логиче-
ских программ проверки корректности конфигурирования брандмауэров на языке
ПРОЛОГ и результаты их испытаний.
Ключевые слова:
межсетевой экран, брандмауэр, процесс, статический анализ
корректности, язык логического программирования ПРОЛОГ.
Введение.
Сетевой экран или брандмауэр – широко известное
средство защиты сетей. Для того чтобы обеспечить требуемую защи-
ту, брандмауэр должен быть соответствующим образом настроен,
или, как говорят, конфигурирован. К сожалению, конфигурирование
может быть сопряжено с ошибками, которые делают даже опытные
администраторы, что приводит к снижению уровня защиты сети и
проникновению в сеть нежелательных пакетов. Как отмечается в ра-
боте [1], изучение 37 брандмауэров показало, что в каждом из них
имеются ошибки, делающие сети уязвимыми для атак. В работе [2]
было проанализировано много реальных ошибок конфигурирования,
результатом которых было проникновение в защищаемую систему
вредоносных программ. Безошибочное конфигурирование брандмау-
эра является непростой задачей. Эта задача усложняется еще и тем,
что в большинстве случаев конфигурирование связано с написанием
его правил на языке низкого уровня, описание на котором трудно
анализировать на предмет соответствия уровня защиты проводимой
политике. Особенно это трудно делать при большом числе правил
конфигурирования. Более того, когда крупная организация развора-
чивает большое количество брандмауэров на множестве сетевых
