Логический анализ корректности конфигурирования межсетевых экранов
15
рассмотрим на примере простой процессной модели, приведенной на
рис. 3. В соответствии с форматом описания пакетов (см. раздел 3) в
процессных моделях будем полагать, что для рис. 3 заданы следую-
щие пакеты:
p1= accept tcp 10.0.0.0/8 any
p2= accept tcp any any
p3= deny tcp 192.168.1.1/32 any
p4= deny udp 10.1.1.64/26 any
p5= accept udp 10.1.1.26/32 any
p6= accept http 192.168.1.25/16 any
p7= deny ftp 192.168.3.1/15 any
p8= drop tcp 10.0.0./8 any
В соответствии с рис. 3 для каждого процессного выражения в
разделе
clauses
формируется факт. Например, для процессного вы-
ражения
?
b7 b1 ( p1)
формируется факт
transition(state_action
(state(b1), action(empty)), p(bit(truth), protocol(tcp), ip_source(10,1,1,0,25),
port_source(_), ip_destination(_,_,_,_,_), port_destination(_)), state_action
(state(b7), action(accept)))
, означающий, что из состояния
b1
осу-
ществляется переход в состояние
b
7 в результате поступления пакета
p
1
, над которым осуществляется действие accept. Аналогично форми-
руются остальные факты и сопутствующие им описания в разделах
domain и predicates. В результате получаем логическую программу
p=p(bit, protocol, ip_source, port_source, ip_destination, port_destination)
bit=bit(symbol)
protocol= protocol(symbol)
ip_source= ip_source(n,n,n,n,n)
port_source= port_source (n)
ip_destination = ip_destination(n,n,n,n,n)
port_destination= port_destination (n)
n=integer
state_action= state_action(state, action)
state= state(symbol)
action= action(symbol)
Среди каждой области правил фильтра следующим образом:
protocol – Имя протоколов
ip_source – ip-адрес источника
port_source – порт-источника
ip_destination – ip-адрес назначения
port_destination – порт- назначения
predicates
nondeterm transition(state_action, p, state_action)
clauses
