第 9 章 HOL における定理証明
9.1 パケット 通過許可条件の証明
pfm::srcnatRuleExists (sap:num*num):bool post:
nattable.natrule->
exist(nr|nr.localAP=sap)
pfm::permit(p:packet):bool post:
isActive() and
(connectionExists(p.getSrcAP(),p.getDstAP()) or isPhysicallyConnectable(p.getSrcAP()) and isValidPacket(p))
pfm::filterOut(p:packet):string*packet post:
not(#2(result)=packet_null) implies result.srcAddr=pfm.getIpAddr()
pfm
+filterOut(p:packet):string*packet +incSec(n:num):void
-connectionExists
(lap:num*num,gap:num*num):bool -srcnatRuleExists(sap:num*num):bool
-localAP:num*num connection
contable nattable
-localAP:num*num natrule
pfm
connectionExists(lap,gap) implies srcnatRuleExists(lap)
pfm::filterOut(p:packet):string*packet post:
not(#2(result)=packet_null) = permit(p)@pre
A
pfm::connectionExists
(lap:num*num,gap:num*num):bool post:
contable.connection->
exist(c|c.localAP=lap)
B
C
0.. 0..
図9.1: 検証対象のOCLによる記述
メソッド pfm_filterOutは，入力パケットpを処理し ，パケットp1として出力する．
パケットが拒否されるとき，p1はpacket_nullとなるため，結論部の左辺(2)は，パケッ トが通過許可されたことを意味する．結論部の右辺は，そのための必要十分条件である．
つまり，pが通過許可されることは，(3)pfmがアクティブ，かつ，(4)pの送信元アドレ スsap，宛先アドレスdapに対応する接続が存在する，または，(5)新しいsapからの接 続を物理的に生成可能であり，(6)pがフィルタルールを満たすパケットである，と同値で ある．前提条件(1)は，pがpfm_filterOut適用前のストアに存在することを意味する．
つまり，pfm_filterOutには，必ず生成されたパケットが入力されると仮定する．
証明
必要十分条件を⇒)と⇐)の 2つに分けて証明する．
⇒)の証明
証明対象のゴールは次のようになる．
!pfm p s.
let (msg,p1,s1) = pfm_filterOut pfm p s in let sap = packet_getSrcAP p s in
let dap = packet_getDstAP p s in packet_ex p s ==>
(~(p1 = packet_null) ==>
pfm_isActive pfm s /\
(pfm_connectionExists pfm sap dap s \/
pfm_isPhysicallyConnectable pfm sap s /\ pfm_isValidPacket pfm p s) まず，結論部の対偶をとる．
!pfm p s.
let (msg,p1,s1) = pfm_filterOut pfm p s in let sap = packet_getSrcAP p s in
let dap = packet_getDstAP p s in packet_ex p s ==>
(~pfm_isActive pfm s \/
~pfm_connectionExists pfm sap dap s /\
(~pfm_isPhysicallyConnectable pfm sap s \/
~pfm_isValidPacket pfm p s)
==> (p1 = packet_null)) ここで，トートロジー
|- !P Q R S. P \/ Q /\ (R \/ S) = P \/ ~P /\ Q /\ R \/ ~P /\ Q /\ ~R /\ S により書き換えを行うと次のようになる．
!pfm p s.
let (msg,p1,s1) = pfm_filterOut pfm p s in let sap = packet_getSrcAP p s in
let dap = packet_getDstAP p s in packet_ex p s ==>
(~pfm_isActive pfm s \/ (1) pfm_isActive pfm s /\ (2)
~pfm_connectionExists pfm sap dap s /\ (3)
~pfm_isPhysicallyConnectable pfm sap s \/ (4) pfm_isActive pfm s /\ (5)
~pfm_connectionExists pfm sap dap s /\ (6) pfm_isPhysicallyConnectable pfm sap s /\ (7)
~pfm_isValidPacket pfm p s) (8)
==> (p1 = packet_null))
ここで，論理和により結合される(1)と(2)〜(4)と(5)〜(8)の 3 つの場合はいずれも パケットを拒否する条件，つまり，p1をpacket_nullにする条件である．これは次の
pfm_filterOutの定義と照らし合わせることにより確かめることができる．
pfm_filterOut pfm p s =
if ~pfm_isActive pfm s then (A)
("drop: pf not active", packet_null, s) (B) else
let sap = packet_getSrcAP p s in let dap = packet_getDstAP p s in
if pfm_connectionExists pfm sap dap s then (C) let s = pfm_srcnat pfm p s in
let s = pfm_updateConnection pfm sap dap s in ("pass: existing connection", p, s) (D)
else if pfm_isPhysicallyConnectable pfm sap s then (E) if pfm_isValidPacket pfm p s then (F)
let s = pfm_addConnection pfm sap dap s in let s = pfm_srcnat pfm p s in
("pass: new connection", p, s) (G) else
let s = pfm_drop pfm s in
("drop: rule not match", packet_null, s) (H)
else
let s = pfm_drop pfm s in
("drop: phisically unconnectable", packet_null, s) (I)
まず，(1)の場合について，(1)は(A)を満たすため，(B)のpacket_nullが出力される．
次に，(2)〜(4)の場合について，(2)は(A)を否定し，(3)は(C)を否定し ，(4)は(E)を 否定するため，(I)にたど り着き，packet_nullが出力される．最後に，(5)〜(8)の場合 について，(5)は(A)を否定し，(6)は(C)を否定し，(7)は(E)を満たし，(8)は(F)を否 定するため，(H)にたどり着き，packet_nullが出力される．
以上3つの場合からいずれもp1=packet_nullが導出されるため，ゴールが証明される．
⇐)の証明
証明対象のゴールは次のようになる．
!pfm p s.
let (msg,p1,s1) = pfm_filterOut pfm p s in let sap = packet_getSrcAP p s in
let dap = packet_getDstAP p s in packet_ex p s ==>
(pfm_isActive pfm s /\
(pfm_connectionExists pfm sap dap s \/
pfm_isPhysicallyConnectable pfm sap s /\ pfm_isValidPacket pfm p s)
==> ~(p1 = packet_null) まず，トートロジー
|- !P Q R S. P /\ (Q \/ R /\ S) = P /\ Q \/ P /\ ~Q /\ R /\ S により書き換えを行うと次のようになる．
!pfm p s.
let (msg,p1,s1) = pfm_filterOut pfm p s in let sap = packet_getSrcAP p s in
let dap = packet_getDstAP p s in packet_ex p s ==>
(pfm_isActive pfm s /\ (1)
pfm_connectionExists pfm sap dap s \/ (2) pfm_isActive pfm s /\ (3)
~pfm_connectionExists pfm sap dap s /\ (4) pfm_isPhysicallyConnectable pfm sap s /\ (5) pfm_isValidPacket pfm p s) (6)
==> ~(p1 = packet_null)
ここで，論理和により結合される(1)(2)と(3)〜(6)の2つの場合はいずれもパケットを通 過させる条件，つまり，p1をpにする条件である．これは前の証明と同様，pfm_filterOut の定義と照らし合わせることにより確かめることができる．
まず，(1)(2)の場合について，(1)は(A)を満たし ，(2)は(C)を満たすため，(D)にた ど り着き，pが出力される．次に，(3)〜(6)の場合について，(3)は(A)を満たし，(4)は (C)を否定し ，(5)は(E)を満たし ，(6)は(F)を満たすため，(G)にたど り着き，pが出 力される．
以上 2 つの場合からいずれもp1=pが導出されるため，ゴ ールは次のように簡単化さ れる．
packet_ex p s ==> ~(p = packet_null)
オブジェクト指向理論には，「 ストアに存在するオブジェクトはNULLではない」とい う定理が存在し ，これによりゴ ールが証明される．
以上，⇒)と⇐)の2 つの証明を合わせて目的の命題が証明される．