Автоматизация проверки некорректности конфигурирования сетевых экранов

1 / 11

ВЫЧИСЛИТЕЛЬНЫЕ МАШИНЫ,
КОМПЛЕКСЫ И КОМПЬЮТЕРНЫЕ СЕТИ
УДК 004.413
АВТОМАТИЗАЦИЯ ПРОВЕРКИ НЕКОРРЕКТНОСТИ
КОНФИГУРИРОВАНИЯ СЕТЕВЫХ ЭКРАНОВ
В.В. Девятков , Мьо Тан Тун
МГТУ им. Н.Э. Баумана, Москва, Российская Федерация
e-mail: ;
Рассмотрена автоматизация поиска ошибок конфигурирования межсетевых
экранов (брандмауэров) на основе принципов логического анализа. Как прави-
ло, для описания поведения сетевых экранов использованы процессные модели,
а для формулировки требований (свойств) некорректности — язык модальной
логики. В настоящей статье детально изложена методика перехода от про-
цессных моделей описания поведения сетевых экранов и условий их некоррект-
ности, формулируемых на языке модальной логики, к конкретным логическим
программам, реализующим проверку некорректности конфигурирования сете-
вых экранов.
Ключевые слова: межсетевой экран, процесс, модальная логика, язык логиче-
ского программирования PROLOG.
AUTOMATION OF VERIFICATION OF INCORRECTNESS
FOR FIREWALL CONFIGURATIONS
V.V. Devyatkov , Myo Than Tun
Bauman Moscow State Technical University, Moscow, Russian Federation
e-mail: ;
This article is devoted to the automation of the search of firewall configuration
errors on the basis of logical analysis. As a rule, process models have been used for
a description the behavior of firewalls, and the language of modal logic has been
applied in order to formulate requirements (properties) of incorrectness. We focus
on the presentation of a detailed methodology of the transition from process models
of a description the behaviors of firewalls and conditions of their incorrectness
(which were formulated in the language of modal logic) to the specific logical
programs that allows to implement verification of incorrectness of firewall
configurations.
Keywords: firewall, process, modal logic, logic programming language PROLOG.
Введение. Сетевой экран, или брандмауэр, — широко известное
средство защиты сетей. Для того чтобы обеспечить требуемую за-
щиту, брандмауэр должен быть соответствующим образом настроен,
или конфигурирован. К сожалению, поведение сетевого экрана мо-
жет быть сопряжено с ошибками, которые допускают даже опытные
администраторы, что приводит к снижению уровня защиты сети и
прониканию в сеть нежелательных пакетов.
Для анализа корректности описания поведения сетевых экранов в
работе [1] предложено использовать процессные модели для описания
100 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 1