В.В. Девятков, Мьо Тан Тун
16
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))).
transition(state_action (state(b2), action(empty)), p(bit(false), protocol(tcp),
ip_source(10,1,1,0,25),
port_source(_),
ip_destination(_,_,_,_,_),
port_destination(_)), state_action (state(b8), action(empty))).
transition(state_action (state(b3), action(empty)),a(bit(truth), protocol(udp),
ip_source(_,_,_,_,_), port_source (_), ip_destination(192,168,1,0,24),
port_destination(_)), state_action (state(b9), action(accept))).
transition(state_action (state(b4), action(empty)), p(bit(false), protocol(udp),
ip_source(_,_,_,_,_), port_source (_), ip_destination(192,168,1,0,24),
port_destination(_)),state_action (state(b10), action(empty))).
transition(state_action (state(b5), action(empty)), p(bit(truth), protocol(tcp),
ip_source(10,1,1,128,25), port_source (_), ip_destination(_,_,_,_,_),
port_destination(_)), state_action (state(b11), action(deny))).
accessible(B1, [X], B2) :- transition(B1, X, B2).
accessible(B1, [X|Rest], B2) :- transition(B1, X, B3), accessible(B3, Rest, B2).
Построение по описанию на языке модальной логики раздела
GOAL.
В рамках настоящей работы не ставилось цели описания на
языке модальной логики всех свойств или требований, которым
должны удовлетворять межсетевые экраны. Они могут быть самыми
различными и достаточно подробно перечислены в литературных ис-
точниках [6,7]. Принципы использования модальной логики для опи-
сания указанных свойств также хорошо известны [8]. Например, если
после начала выполнения процесса
P
на рис. 3 не должно быть ни
одного затенения, то это требование можно выразить простой мо-
дальной формулой
[!
( ))]
[(!
( ))]
accept p
drop p
(см. раздел
3.1.1.1). Это означает, что должен существовать хотя бы один путь,
ведущий из какого-либо текущего, в котором над пакетом
p
соверша-
ется действие
accept
в другое состояниe, в котором над этим же паке-
том совершается действие
drop
. На языке ПРОЛОГ это можно выра-
зить в виде следующего раздела
goal
(цели):
goal
accessible (state_action (state(X), action(accept)), [ p(bit(truth), protocol(tcp),
ip_source(N1,N2,N3,N4,_),port_source
(_),
ip_destination(_,_,_,_,_),
port_destination(_))], state_action (state(X), action(_))),
accessible(state_action (state(Y), action(drop)),[p(bit(false), protocol(_),
ip_source(N1,N2,N3,N4,_), port_source (_), ip_destination(_,_,_,_,_),
port_destination(_)),state_action (state(Y), action(_))), X< >Y.
Проверка затенения для конфигурирования сетевого экрана.
В результате работы полученной по процессному описанию логиче-
ской программы на ПРОЛОГе при заданной цели получим результат
