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