Логический анализ корректности конфигурирования межсетевых экранов
9
Internet
П
1
П
2
P
11
Сетевой экран
P
12
Сетевой экран
D
Демилитаризованная зона
P
21
Сетевой экран
P
22
Сетевой экран
N
Внутренняя сеть предприятия
Рис 6.
Пример сетевой среды с сетевыми экранами
следовать классификации этих некорректностей, предложенной в ра-
боте [3]. Главное, чему будем уделять внимание при рассмотрении не-
корректностей – это их формальное описание на языке временной мо-
дальной логики условий (свойств) некорректности, для того чтобы
можно было использовать эти описания для формальной проверки не-
корректностей в процессных моделях. Для этого введем следующий
формат описания пакетов, используемый в процессных моделях.
,
_
,
_
,
_
;
;
.
.
.
/
1 ;
пакет протокол
IP адрес источника
порт источника
IP адрес назначения
порт назаначения
протокол tcp udp ftp
IP адрес источника
число число число число число
IP адрес назназначения
.
.
.
/
1 ;
01....... 255;
1 01....... 32;
_
2 ;
_
2 ;
2 01....... 65536;
число число число число число
число
число
порт источника any число
порт назаначения any число
число
