В.В. Девятков, Мьо Тан Тун
10
Некорректности сетевых экранов.
Некорректности в описаниях
сетевых экранов могут встречаться во всех трех рассмотренных ти-
пах процессных моделей: простых, сложных и сетевых. Настоящий
раздел посвящен принципам формального описания этих некоррект-
ностей.
Некорректности однопроцессных моделей
. Простейший случай
затенения возникает, когда действия двух правил в списке, одно из
которых предшествует другому правилу, являются противополож-
ными по смыслу, но применяются к одному и тому же пакету
p
. Яс-
но, что если предшествующее правило разрешает принять этот пакет,
а последующее запрещает его прием, то пакет будет принят. И
наоборот, если предшествующее правило запрещает принимать этот
пакет, а последующее разрешает его прием, то пакет не будет принят.
Понятно, что такая ситуация, хотя и разрешается однозначно, являет-
ся ошибкой, поскольку неизвестно, чем руководствовался автор тако-
го конфигурирования. Возникает большое сомнение в том, что он
сделал это сознательно. Скорее всего, это ошибка и ее надо выявлять.
Используя временную модальную логику и канонические процесс-
ные выражения, одно из правил корректности выглядит следующим
образом:
[!
( ))]
[(!
( ))].
accept p
drop p
Смысл этого правила следующий: всегда, когда в некотором те-
кущем состоянии совершается действие !
accept
, в которое процесс
перешел из некоторого состояния в результате получения (восприя-
тия) пакета
p
, то никогда в будущем не должно быть другого состо-
яния, в которое процесс перешел из некоторого состояния в резуль-
тате получения (восприятия) того же пакета
p
и в котором соверша-
ется действие
drop
.
Исключение возникает, когда действия двух правил в списке, од-
но из которых предшествует другому правилу, являются противопо-
ложными по смыслу, но пакет предшествующего правила является
подмножеством последующего. Ясно, что если предшествующее
правило разрешает принять этот пакет, а последующее запрещает его
прием, то предшествующий пакет, входящий в последующий, будет
принят. И наоборот, если предшествующее правило запрещает при-
нимать пакет, а последующее разрешает его прием, то пакет, входя-
щий в последующий, не будет принят. Понятно, что такая ситуация,
разрешается однозначно, но непонятно, является ли она ошибкой или
допущена сознательно, но найти эту ситуацию всегда имеет смысл.
Используя временную модальную логику и канонические процесс-
ные выражения, правило корректности, истинность которого гаран-
тирует наличие исключения, выглядит следующим образом:
