Логический анализ корректности конфигурирования межсетевых экранов
13
большое сомнение в том, что он сделал это сознательно. Скорее все-
го, это ошибка и ее надо выявлять.
Покажем, что затенение между сетевыми экранами можно свести
к случаю одного экрана, композируя определенным образом процес-
сы экранов.
Пусть даны два процесса
P
1
и
P
2
, причем процесс
P
1
выполняется
перед процессом
P
2
, то есть имеем процесс
1 2
P P P
. Каждый из про-
цессов
P
1
и
P
2
имеют соответственно начальные состояния
1
1
? ,
b e
2
1
?
b e
и конечные состояния.
1 1
1
? ( ),
i
i
b b not p
2 2
1
( ),
j
j
b b not p
такие
что
1
2
!
, !
.
i
j
stop b stop b
Введем операцию «
» композиции последова-
тельно работающих процессов
1 2
P P
, описывающих последовательную
работу каких-либо двух экранов. Она состоит в следующем. В процессе
P
1
заменяем выражение
1 1
1
? ( )
i
i
b b not p
на выражение
2 1
1
1
? ( )
i
b b not p
и удаляем выражение
1
!
i
stop b
. В процессе
P
2
удаляем выражение
2
1
?
b e
. В результате получим процесс
1 2
P P P
, выполнение кото-
рого эквивалентно выполнению процесса
1 2
P P P
. Например, на рис. 7
показан процесс
1 2
P P P
, а на рис. 8 – процесс
1 2
.
P P P
1
1
1
1 1
2 1
1
1 1
7 1
1
1 1
3 2
2
1 1
8 2
2
1 1
4 3
3
1 1
9 3
3
1 1
5 4
4
1
1
1 2
10 4
4
1 1
6 5
5
1 1
11 5
5
1
7
1
8
1
9
? ,
? ( ),
?( ),
? ( ),
?( ),
? ( ),
?( ),
? ( ),
,
?( ),
? ( ),
?( ),
!
,
!
,
!
,
!
P
b e
b b not p
b b p
b b not p
b b p
b b not p
b b p
b b not p
P P P b b p
b b not p
b b p
accept b
accept b
drop b
a
2
2
1
2
2
2 1
1
2
2
7 1
1
2
2
3
2
2
2
2
8
2
2
2
2
4 3
3
2
2
9
3 3
2 2
5 4
4
2
2
10 4
4
2 2
6 5
5
2 2
11 5
5
1
10
1
11
1
6
? ,
? ( ),
?( ),
? ( ),
?( ),
? ( ),
( ),
? ( ),
?( ),
( ),
?( ),
!
,
!
_
,
!
,
P
b e
b b not p
b b p
b b not p
b b p
b b not p
b b p
b b not p
b b p
b b not p
b b p
accept b
ccept b
drop all b
stop b
2
7
2
8
2
9
2
10
2
11
2
6
,
!
,
!
,
!
,
!
_
,
!
.
accept b
drop b
accept b
drop all b
stop b
1
1
1
1 1
2 1
1
1 1
7 1
1
1 1
3 2
2
1 1
8 2
2
1 1
4 3
3
1 1
9 3
3
1 1
5 4
4
1 2 1
1
10 4
4
2 1
1 5
5
1 1
11 5
5
1
7
1
8
1
9
? ,
? ( ),
?( ),
? ( ),
?( ),
? ( ),
?( ),
? ( ),
,
?( ),
? ( ),
?( ),
!
,
!
,
!
,
!
P
b e
b b not p
b b p
b b not p
b b p
b b not p
b b p
b b not p
P P P
b b p
b b not p
b b p
accept b
accept b
drop b
2
2 2
2 1
1
2 2
7 1
1
2 2
3 2
2
2 2
8 2
2
2 2
4 3
3
2 2
9 3 3
2 2
5 4
4
2
2
10 4
4
2 2
6 5
5
2 2
11 5
5
2
7
2
8
1
10
1
11
? ( ),
?( ),
? ( ),
?( ),
? ( ),
( ),
? ( ),
?( ),
( ),
?( ),
!
,
!
,
!
,
!
_
,
P
b b not p
b b p
b b not p
b b p
b b not p
b b p
b b not p
b b p
b b not p
b b p
accept b
accept b
accept b
drop all b
2
9
2
10
2
11
2
6
,
!
,
!
_
,
!
.
drop b
accept b
drop all b
stop b
Рис. 7.
Процесс
1 2
P P P
Рис. 8.
Процесс
1 2
P P P
Таким образом, анализ затенения между двумя сетевыми экранами
1 2
,
P P
сводится к анализу затенения одного процесса
1 2
P P P
. Оче-
