Логический анализ корректности конфигурирования межсетевых экранов - page 4

В.В. Девятков, Мьо Тан Тун
4
мальное метаописание свойств корректности собственно списков
управления доступом.
Переходы между правилами различных списков требуют от вы-
зываемого списка после его выполнения возврата в ту же точку вы-
зывающего списка, откуда произошел вызов, что ограничивает воз-
можности проверок корректности и повышение уровня эффективно-
сти вычислений.
Описание на языке списков управления доступом использует
только свойства пакетов, но не содержит формализмов описания от-
дельных элементов этих пакетов и их совокупностей, что в случае
моделирования динамической проверки на корректность конфигури-
рования требует генерации этих элементов внешними по отношению
к языку средствами.
Использование процессных моделей как языков описания пове-
дения брандмауэров позволяет устранить указанные недостатки.
Процессные модели конфигурирования брандмауэров.
Каж-
дый процесс имеет алфавит восприятий и реакций
A
= {
a
1
,
a
2
,...,
a
m
}.
Каждый символ
a
этого алфавита именует некоторый объект, полу-
чаемый (воспринимаемый) процессом из внешней среды (восприятие
процесса), выдаваемый процессом во внешнюю среду (внешняя ре-
акция процесса) или объект, используемый процессом для внутрен-
них нужд (внутренняя реакция процесса). Процессы действуют, вос-
принимая, порождая для внутреннего употребления или выдавая
наружу объекты с соответствующими именами. Для того, чтобы раз-
личать типы действий, будем использовать следующие обозначения:
?
a
– для восприятий, !
a
– для внешних реакций,
b
– для внутренних
реакций.
Нитью
a
*
будем называть кортеж (конечный или бесконечный)
действий
a
*
=
a
0
a
1
a
2
a
m
–2
a
m
–1
. Выполнением нити процессом
P
называется последовательность выполнения ее действий в опреде-
ленном порядке слева направо. Символом
е
обозначается пустое дей-
ствие. Нить, состоящая из единственного пустого действия, называ-
ется пустой нитью. Процессом
P
называется множество нитей
S
,
которые он может выполнять. Поведением процесса
P
называется
порядок выполнения множества этих нитей.
Обозначим
?
A
множество всех восприятий некоторого процес-
са
P
, включая пустое восприятие
?
e
,
!
A
– конечное множество всех
внешних реакций процесса
P
, включая пустую внешнюю реакцию
!
e
,
S
– множество всех нитей, выполняемых процессом
P
, таких что
*
? !
S A A
 
, где
*
?
a
– нить, состоящая только из восприятий (нить
восприятий) процесса
P
,
*
?
A
– множество всех нитей
*
?
a
в алфави-
те
?
A
,
*
– функция на множестве
*
?
A
, которая ставит в соответ-
1,2,3 5,6,7,8,9,10,11,12,13,14,...18
Powered by FlippingBook