Логический анализ корректности конфигурирования межсетевых экранов
3
торых гораздо шире, а теория более развита, что позволяет описывать
гораздо более сложные модели программ конфигурирования. Типы
ошибок в программах конфигурирования предлагается описывать, в
отличие от работы [3], формально как свойства процессных моделей
программ конфигурирования на языке временной модальной логики.
Процессные модели в дальнейшем будем называть просто процесса-
ми. Процессы позволяют гораздо более четко и полно классифициро-
вать и описывать типы ошибок. Статический анализ поиска ошибок
предлагается осуществлять методами логического программирования
как доказательство или вывод свойств процессов конфигурирования,
что является гораздо более изящным, полным и не имеющим ограни-
чений подходом проверки корректности конфигурирования бранд-
мауэров.
Межсетевые экраны или брандмауэры различных производите-
лей могут существенно различаться языками конфигурирования. Од-
нако, если не учитывать эти различия, то обычно конфигурирование
любого сетевого экрана состоит в составлении списков управления
доступом (access control lists: ACL [3]), используемых для управления
процессом доступа. Брандмауэр обычно имеет несколько интерфей-
сов. Каждый интерфейс конфигурируется различными списками
управления доступом. Каждый список управления доступом состоит
из списка правил. Отдельное правило представляется парой <
p
,
action
>,
где
p
– пакет, над которым совершается действие,
action
. Каждый пакет,
поступающий на сетевой экран обрабатывается последовательно
каждым правилом в порядке записи их сверху вниз. Если пакет
p
удовлетворяет некоторому свойству
R
(
p
), то над ним совершается
действие
action
и он к следующему правилу не направляется. Если
пакет
p
не удовлетворяет этому свойству, то действие
action
над ним
не совершается и он направляется к следующему правилу, переходя,
таким образом, от правила к правилу до тех пор, пока не достигнет
последнего правила. Свойство
R
(
p
) можно рассматривать как некото-
рый предикат, который истинен, если упоминаемое свойство имеет
место и ложен в противном случае. Списки управления доступом как
язык конфигурирования брандмауэров с точки зрения проверки кор-
ректности конфигурирования, на наш взгляд, обладают рядом следу-
ющих недостатков.
Списки управления доступом имеют недостаточно проработан-
ный формальный синтаксис, что не позволяет однозначно понимать
некоторые описания на этом языке.
Последовательная природа обработки и передачи пакетов от пра-
вила к правилу в порядке записи правил декларируется, но никак не
описывается средствами языка, что делает затруднительным фор-
