В.В. Девятков, Мьо Тан Тун
14
видно, что для выявления всех затенений примера на рис. 6 придется
отдельно подвергнуть анализу четыре процесса:
11 21
,
P P
11 22
,
P P
12 21
,
P P
12 21
,
P P
12 22
.
P P
Сетевое проникновение
. Как показано выше, в случае наличия
нескольких экранов возникает возможность прохождения пакетов по
различным путям, что может привести к проникновению запрещен-
ных пакетов в закрытые для них зоны. В этом случае нет другого вы-
хода, кроме как анализировать пути возможного перемещения паке-
тов и смотреть, нет ли среди них таких, которые не должны прони-
кать в запрещенные зоны. Для этого, как и в предыдущем случае,
придется построить все процессы, защищающие эти пути, затем за-
дать пакеты, которые не должны проникать в запретные для них зо-
ны, и проверить, нет ли для каждого из них процесса, который позво-
ляет им это сделать. Если обозначить множество пакетов, которым
запрещено проникать из некоторой зоны
S
в некоторую зону
E
как
p
(
S
,
E
), множество процессов, защищающих пути движения пакетов
из зоны
S
в зону
E
как
P
(
S
,
E
), факт поступления на процесс
P
пакета
p
как
p
.
P
, то условие отсутствия сетевого проникновения пакета
p
для всех процессов
( , ))
P P S E
и всех пакетов
( , ))
p p S E
выражает-
ся следующей формулой модальной логики:
[ .
(!
( )
(!
( )].
p P drop p
accept p
Смысл следующий: всегда, когда процесс
P
получает пакет
p
, то
в будущем этот процесс должен перейти в некоторое состояние, в ко-
тором совершается действие
drop
, запрещающее пропускать этот па-
кет и перед этим не должно быть другого состояния, в которое про-
цесс перешел из некоторого состояния в результате получения (вос-
приятия) того же пакета
p
и в котором совершается действие
accept
.
Принципы перехода от процессного описания модели конфи-
гурирования сетевого экрана к описанию на языке ПРОЛОГ и
поиск некорректностей.
Переход от процессного описания конфи-
гурирования сетевого экрана к описанию на языке ПРОЛОГ включа-
ет следующие шаги:
построение по процессному описанию модели конфигурирова-
ния логической программы на ПРОЛОГЕ (от начального раздела до
раздела GOAL);
построение по описанию на языке модальной логики раздела
GOAL;
проверка корректности.
Построение по процессному описанию модели конфигурирова-
ния логической программы на ПРОЛОГЕ до раздела GOAL.
Прин-
ципы перехода от процессного описания к программе на ПРОЛОГЕ
