Theory SimpleFw_Compliance
section‹Iptables to Simple Firewall and Vice Versa›
theory SimpleFw_Compliance
imports Simple_Firewall.SimpleFw_Semantics
"../Primitive_Matchers/Transform"
"../Primitive_Matchers/Primitive_Abstract"
begin
subsection‹Simple Match to MatchExpr›
fun simple_match_to_ipportiface_match :: "'i::len simple_match ⇒ 'i common_primitive match_expr" where
"simple_match_to_ipportiface_match ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p, sports=sps, dports=dps ⦈ =
MatchAnd (Match (IIface iif)) (MatchAnd (Match (OIface oif))
(MatchAnd (Match (Src (uncurry IpAddrNetmask sip)))
(MatchAnd (Match (Dst (uncurry IpAddrNetmask dip)))
(case p of ProtoAny ⇒ MatchAny
| Proto prim_p ⇒
(MatchAnd (Match (Prot p))
(MatchAnd (Match (Src_Ports (L4Ports prim_p [sps])))
(Match (Dst_Ports (L4Ports prim_p [dps])))
))
))))"
lemma ports_to_set_singleton_simple_match_port: "p ∈ ports_to_set [a] ⟷ simple_match_port a p"
by(cases a, simp)
theorem simple_match_to_ipportiface_match_correct:
assumes valid: "simple_match_valid sm"
shows "matches (common_matcher, α) (simple_match_to_ipportiface_match sm) a p ⟷ simple_matches sm p"
proof -
obtain iif oif sip dip pro sps dps where
sm: "sm = ⦇iiface = iif, oiface = oif, src = sip, dst = dip, proto = pro, sports = sps, dports = dps⦈" by (cases sm)
{ fix ip
have "p_src p ∈ ipt_iprange_to_set (uncurry IpAddrNetmask ip) ⟷ simple_match_ip ip (p_src p)"
and "p_dst p ∈ ipt_iprange_to_set (uncurry IpAddrNetmask ip) ⟷ simple_match_ip ip (p_dst p)"
by(simp split: uncurry_split)+
} note simple_match_ips=this
{ fix ps
have "p_sport p ∈ ports_to_set [ps] ⟷ simple_match_port ps (p_sport p)"
and "p_dport p ∈ ports_to_set [ps] ⟷ simple_match_port ps (p_dport p)"
apply(case_tac [!] ps)
by(simp_all)
} note simple_match_ports=this
from valid sm have valid':"pro = ProtoAny ⟹ simple_match_port sps (p_sport p) ∧ simple_match_port dps (p_dport p)"
apply(simp add: simple_match_valid_def)
by blast
show ?thesis unfolding sm
apply(cases pro)
subgoal
apply(simp add: bunch_of_lemmata_about_matches simple_matches.simps)
apply(simp add: match_raw_bool ternary_to_bool_bool_to_ternary simple_match_ips simple_match_ports simple_matches.simps)
using valid' by simp
apply(simp add: bunch_of_lemmata_about_matches simple_matches.simps)
apply(simp add: match_raw_bool ternary_to_bool_bool_to_ternary simple_match_ips simple_match_ports simple_matches.simps)
apply fast
done
qed
subsection‹MatchExpr to Simple Match›
fun common_primitive_match_to_simple_match :: "'i::len common_primitive match_expr ⇒ 'i simple_match option" where
"common_primitive_match_to_simple_match MatchAny = Some (simple_match_any)" |
"common_primitive_match_to_simple_match (MatchNot MatchAny) = None" |
"common_primitive_match_to_simple_match (Match (IIface iif)) = Some (simple_match_any⦇ iiface := iif ⦈)" |
"common_primitive_match_to_simple_match (Match (OIface oif)) = Some (simple_match_any⦇ oiface := oif ⦈)" |
"common_primitive_match_to_simple_match (Match (Src (IpAddrNetmask pre len))) = Some (simple_match_any⦇ src := (pre, len) ⦈)" |
"common_primitive_match_to_simple_match (Match (Dst (IpAddrNetmask pre len))) = Some (simple_match_any⦇ dst := (pre, len) ⦈)" |
"common_primitive_match_to_simple_match (Match (Prot p)) = Some (simple_match_any⦇ proto := p ⦈)" |
"common_primitive_match_to_simple_match (Match (Src_Ports (L4Ports p []))) = None" |
"common_primitive_match_to_simple_match (Match (Src_Ports (L4Ports p [(s,e)]))) = Some (simple_match_any⦇ proto := Proto p, sports := (s,e) ⦈)" |
"common_primitive_match_to_simple_match (Match (Dst_Ports (L4Ports p []))) = None" |
"common_primitive_match_to_simple_match (Match (Dst_Ports (L4Ports p [(s,e)]))) = Some (simple_match_any⦇ proto := Proto p, dports := (s,e) ⦈)" |
"common_primitive_match_to_simple_match (MatchNot (Match (Prot ProtoAny))) = None" |
"common_primitive_match_to_simple_match (MatchAnd m1 m2) = (case (common_primitive_match_to_simple_match m1, common_primitive_match_to_simple_match m2) of
(None, _) ⇒ None
| (_, None) ⇒ None
| (Some m1', Some m2') ⇒ simple_match_and m1' m2')" |
"common_primitive_match_to_simple_match (Match (Src (IpAddr _))) = undefined" |
"common_primitive_match_to_simple_match (Match (Src (IpAddrRange _ _))) = undefined" |
"common_primitive_match_to_simple_match (Match (Dst (IpAddr _))) = undefined" |
"common_primitive_match_to_simple_match (Match (Dst (IpAddrRange _ _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (Prot _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (IIface _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (OIface _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (Src _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (Dst _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (MatchAnd _ _)) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (MatchNot _)) = undefined" |
"common_primitive_match_to_simple_match (Match (Src_Ports _)) = undefined" |
"common_primitive_match_to_simple_match (Match (Dst_Ports _)) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (Src_Ports _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (Dst_Ports _))) = undefined" |
"common_primitive_match_to_simple_match (Match (CT_State _)) = undefined" |
"common_primitive_match_to_simple_match (Match (L4_Flags _)) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (L4_Flags _))) = undefined" |
"common_primitive_match_to_simple_match (Match (Extra _)) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (Extra _))) = undefined" |
"common_primitive_match_to_simple_match (MatchNot (Match (CT_State _))) = undefined"
subsubsection‹Normalizing Interfaces›
text‹As for now, negated interfaces are simply not allowed›
definition normalized_ifaces :: "'i::len common_primitive match_expr ⇒ bool" where
"normalized_ifaces m ≡ ¬ has_disc_negated (λa. is_Iiface a ∨ is_Oiface a) False m"
subsubsection‹Normalizing Protocols›
text‹As for now, negated protocols are simply not allowed›
definition normalized_protocols :: "'i::len common_primitive match_expr ⇒ bool" where
"normalized_protocols m ≡ ¬ has_disc_negated is_Prot False m"
lemma match_iface_simple_match_any_simps:
"match_iface (iiface simple_match_any) (p_iiface p)"
"match_iface (oiface simple_match_any) (p_oiface p)"
"simple_match_ip (src simple_match_any) (p_src p)"
"simple_match_ip (dst simple_match_any) (p_dst p)"
"match_proto (proto simple_match_any) (p_proto p)"
"simple_match_port (sports simple_match_any) (p_sport p)"
"simple_match_port (dports simple_match_any) (p_dport p)"
apply (simp_all add: simple_match_any_def match_ifaceAny ipset_from_cidr_0)
apply (subgoal_tac [!] "(65535::16 word) = - 1")
apply (simp_all only:)
apply simp_all
done
theorem common_primitive_match_to_simple_match:
assumes "normalized_src_ports m"
and "normalized_dst_ports m"
and "normalized_src_ips m"
and "normalized_dst_ips m"
and "normalized_ifaces m"
and "normalized_protocols m"
and "¬ has_disc is_L4_Flags m"
and "¬ has_disc is_CT_State m"
and "¬ has_disc is_MultiportPorts m"
and "¬ has_disc is_Extra m"
shows "(Some sm = common_primitive_match_to_simple_match m ⟶ matches (common_matcher, α) m a p ⟷ simple_matches sm p) ∧
(common_primitive_match_to_simple_match m = None ⟶ ¬ matches (common_matcher, α) m a p)"
proof -
show ?thesis
using assms proof(induction m arbitrary: sm rule: common_primitive_match_to_simple_match.induct)
case 1 thus ?case
by(simp add: match_iface_simple_match_any_simps bunch_of_lemmata_about_matches simple_matches.simps)
next
case (9 p s e) thus ?case
apply(simp add: match_iface_simple_match_any_simps simple_matches.simps)
apply(simp add: match_raw_bool ternary_to_bool_bool_to_ternary)
by fastforce
next
case 11 thus ?case
apply(simp add: match_iface_simple_match_any_simps simple_matches.simps)
apply(simp add: match_raw_bool ternary_to_bool_bool_to_ternary)
by fastforce
next
case (13 m1 m2)
let ?caseSome="Some sm = common_primitive_match_to_simple_match (MatchAnd m1 m2)"
let ?caseNone="common_primitive_match_to_simple_match (MatchAnd m1 m2) = None"
let ?goal="(?caseSome ⟶ matches (common_matcher, α) (MatchAnd m1 m2) a p = simple_matches sm p) ∧
(?caseNone ⟶ ¬ matches (common_matcher, α) (MatchAnd m1 m2) a p)"
from 13 have normalized:
"normalized_src_ports m1" "normalized_src_ports m2"
"normalized_dst_ports m1" "normalized_dst_ports m2"
"normalized_src_ips m1" "normalized_src_ips m2"
"normalized_dst_ips m1" "normalized_dst_ips m2"
"normalized_ifaces m1" "normalized_ifaces m2"
"¬ has_disc is_L4_Flags m1" "¬ has_disc is_L4_Flags m2"
"¬ has_disc is_CT_State m1" "¬ has_disc is_CT_State m2"
"¬ has_disc is_MultiportPorts m1" "¬ has_disc is_MultiportPorts m2"
"¬ has_disc is_Extra m1" "¬ has_disc is_Extra m2"
"normalized_protocols m1" "normalized_protocols m2"
by(simp_all add: normalized_protocols_def normalized_ifaces_def)
{ assume caseNone: ?caseNone
{ fix sm1 sm2
assume sm1: "common_primitive_match_to_simple_match m1 = Some sm1"
and sm2: "common_primitive_match_to_simple_match m2 = Some sm2"
and sma: "simple_match_and sm1 sm2 = None"
from sma have 1: "¬ (simple_matches sm1 p ∧ simple_matches sm2 p)" by (simp add: simple_match_and_correct)
from normalized sm1 sm2 "13.IH" have 2: "(matches (common_matcher, α) m1 a p ⟷ simple_matches sm1 p) ∧
(matches (common_matcher, α) m2 a p ⟷ simple_matches sm2 p)" by force
hence 2: "matches (common_matcher, α) (MatchAnd m1 m2) a p ⟷ simple_matches sm1 p ∧ simple_matches sm2 p"
by(simp add: bunch_of_lemmata_about_matches)
from 1 2 have "¬ matches (common_matcher, α) (MatchAnd m1 m2) a p" by blast
}
with caseNone have "common_primitive_match_to_simple_match m1 = None ∨
common_primitive_match_to_simple_match m2 = None ∨
¬ matches (common_matcher, α) (MatchAnd m1 m2) a p"
by(simp split:option.split_asm)
hence "¬ matches (common_matcher, α) (MatchAnd m1 m2) a p"
apply(elim disjE)
apply(simp_all)
using "13.IH" normalized by(simp add: bunch_of_lemmata_about_matches)+
}note caseNone=this
{ assume caseSome: ?caseSome
hence "∃ sm1. common_primitive_match_to_simple_match m1 = Some sm1" and
"∃ sm2. common_primitive_match_to_simple_match m2 = Some sm2"
by(simp_all split: option.split_asm)
from this obtain sm1 sm2 where sm1: "Some sm1 = common_primitive_match_to_simple_match m1"
and sm2: "Some sm2 = common_primitive_match_to_simple_match m2" by fastforce+
with "13.IH" normalized have "matches (common_matcher, α) m1 a p = simple_matches sm1 p ∧
matches (common_matcher, α) m2 a p = simple_matches sm2 p" by simp
hence 1: "matches (common_matcher, α) (MatchAnd m1 m2) a p ⟷ simple_matches sm1 p ∧ simple_matches sm2 p"
by(simp add: bunch_of_lemmata_about_matches)
from caseSome sm1 sm2 have "simple_match_and sm1 sm2 = Some sm" by(simp split: option.split_asm)
hence 2: "simple_matches sm p ⟷ simple_matches sm1 p ∧ simple_matches sm2 p" by(simp add: simple_match_and_correct)
from 1 2 have "matches (common_matcher, α) (MatchAnd m1 m2) a p = simple_matches sm p" by simp
} note caseSome=this
from caseNone caseSome show ?goal by blast
qed(simp_all add: match_iface_simple_match_any_simps simple_matches.simps normalized_protocols_def normalized_ifaces_def,
simp_all add: bunch_of_lemmata_about_matches,
simp_all add: match_raw_bool ternary_to_bool_bool_to_ternary)
qed
lemma simple_fw_remdups_Rev: "simple_fw (remdups_rev rs) p = simple_fw rs p"
apply(induction rs p rule: simple_fw.induct)
apply(simp add: remdups_rev_def)
apply(simp_all add: remdups_rev_fst remdups_rev_removeAll simple_fw_not_matches_removeAll)
done
fun action_to_simple_action :: "action ⇒ simple_action" where
"action_to_simple_action action.Accept = simple_action.Accept" |
"action_to_simple_action action.Drop = simple_action.Drop" |
"action_to_simple_action _ = undefined"
definition check_simple_fw_preconditions :: "'i::len common_primitive rule list ⇒ bool" where
"check_simple_fw_preconditions rs ≡ ∀r ∈ set rs. (case r of (Rule m a) ⇒
normalized_src_ports m ∧
normalized_dst_ports m ∧
normalized_src_ips m ∧
normalized_dst_ips m ∧
normalized_ifaces m ∧
normalized_protocols m ∧
¬ has_disc is_L4_Flags m ∧
¬ has_disc is_CT_State m ∧
¬ has_disc is_MultiportPorts m ∧
¬ has_disc is_Extra m ∧
(a = action.Accept ∨ a = action.Drop))"
lemma "normalized_src_ports m ⟹ normalized_nnf_match m"
apply(induction m rule: normalized_src_ports.induct)
apply(simp_all)[15]
oops
lemma "¬ matcheq_matchNone m ⟹ normalized_src_ports m ⟹ normalized_nnf_match m"
by(induction m rule: normalized_src_ports.induct) (simp_all)
value "check_simple_fw_preconditions [Rule (MatchNot (MatchNot (MatchNot (Match (Src a))))) action.Accept]"
definition to_simple_firewall :: "'i::len common_primitive rule list ⇒ 'i simple_rule list" where
"to_simple_firewall rs ≡ if check_simple_fw_preconditions rs then
List.map_filter (λr. case r of Rule m a ⇒
(case (common_primitive_match_to_simple_match m) of None ⇒ None |
Some sm ⇒ Some (SimpleRule sm (action_to_simple_action a)))) rs
else undefined"
lemma to_simple_firewall_simps:
"to_simple_firewall [] = []"
"check_simple_fw_preconditions ((Rule m a)#rs) ⟹ to_simple_firewall ((Rule m a)#rs) = (case common_primitive_match_to_simple_match m of
None ⇒ to_simple_firewall rs
| Some sm ⇒ (SimpleRule sm (action_to_simple_action a)) # to_simple_firewall rs)"
"¬ check_simple_fw_preconditions rs' ⟹ to_simple_firewall rs' = undefined"
by(auto simp add: to_simple_firewall_def List.map_filter_simps check_simple_fw_preconditions_def split: option.split)
lemma "check_simple_fw_preconditions
[Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Dst_Ports (L4Ports TCP [(0, 65535)])))
(Match (Src_Ports (L4Ports TCP [(0, 65535)])))))
Drop]" by eval
lemma "to_simple_firewall
[Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
(MatchAnd (Match (Dst_Ports (L4Ports TCP [(0, 65535)])))
(Match (Src_Ports (L4Ports TCP [(0, 65535)])))))
Drop] =
[SimpleRule
⦇iiface = Iface ''+'', oiface = Iface ''+'', src = (0x7F000000, 8), dst = (0, 0), proto = Proto 6, sports = (0, 0xFFFF),
dports = (0, 0xFFFF)⦈
simple_action.Drop]" by eval
lemma "check_simple_fw_preconditions [Rule (MatchAnd MatchAny MatchAny) Drop]"
by(simp add: check_simple_fw_preconditions_def normalized_ifaces_def normalized_protocols_def)
lemma "to_simple_firewall [Rule (MatchAnd MatchAny (MatchAny::32 common_primitive match_expr)) Drop] =
[SimpleRule
⦇iiface = Iface ''+'', oiface = Iface ''+'', src = (0, 0), dst = (0, 0), proto = ProtoAny, sports = (0, 0xFFFF),
dports = (0, 0xFFFF)⦈
simple_action.Drop]" by eval
lemma "to_simple_firewall [Rule (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8))) Drop] =
[SimpleRule
⦇iiface = Iface ''+'', oiface = Iface ''+'', src = (0x7F000000, 8), dst = (0, 0), proto = ProtoAny, sports = (0, 0xFFFF),
dports = (0, 0xFFFF)⦈
simple_action.Drop]" by eval
theorem to_simple_firewall: "check_simple_fw_preconditions rs ⟹ approximating_bigstep_fun (common_matcher, α) p rs Undecided = simple_fw (to_simple_firewall rs) p"
proof(induction rs)
case Nil thus ?case by(simp add: to_simple_firewall_simps)
next
case (Cons r rs)
from Cons have IH: "approximating_bigstep_fun (common_matcher, α) p rs Undecided = simple_fw (to_simple_firewall rs) p"
by(simp add: check_simple_fw_preconditions_def)
obtain m a where r: "r = Rule m a" by(cases r, simp)
from Cons.prems have "check_simple_fw_preconditions [r]" by(simp add: check_simple_fw_preconditions_def)
with r common_primitive_match_to_simple_match[where p = p]
have match: "⋀ sm. common_primitive_match_to_simple_match m = Some sm ⟹ matches (common_matcher, α) m a p = simple_matches sm p" and
nomatch: "common_primitive_match_to_simple_match m = None ⟹ ¬ matches (common_matcher, α) m a p"
unfolding check_simple_fw_preconditions_def by simp_all
from to_simple_firewall_simps r Cons.prems have to_simple_firewall_simps': "to_simple_firewall (Rule m a # rs) =
(case common_primitive_match_to_simple_match m of None ⇒ to_simple_firewall rs
| Some sm ⇒ SimpleRule sm (action_to_simple_action a) # to_simple_firewall rs)" by simp
from ‹check_simple_fw_preconditions [r]› have "a = action.Accept ∨ a = action.Drop" by(simp add: r check_simple_fw_preconditions_def)
thus ?case
by(auto simp add: r to_simple_firewall_simps' IH match nomatch split: option.split action.split)
qed
lemma ctstate_assume_new_not_has_CT_State:
"r ∈ set (ctstate_assume_new rs) ⟹ ¬ has_disc is_CT_State (get_match r)"
apply(simp add: ctstate_assume_new_def)
apply(induction rs)
apply(simp add: optimize_matches_def; fail)
apply(simp add: optimize_matches_def)
apply(rename_tac r' rs, case_tac r')
apply(safe)
apply(simp add: split:if_split_asm)
apply(elim disjE)
apply(simp_all add: not_hasdisc_ctstate_assume_state split:if_split_asm)
done
text‹The precondition for the simple firewall can be easily fulfilled.
The subset relation is due to abstracting over some primitives (e.g., negated primitives, l4 flags)›
theorem transform_simple_fw_upper:
defines "preprocess rs ≡ upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new rs)))"
and "newpkt p ≡ match_tcp_flags ipt_tcp_syn (p_tcp_flags p) ∧ p_tag_ctstate p = CT_New"
assumes simplers: "simple_ruleset (rs:: 'i::len common_primitive rule list)"
shows "check_simple_fw_preconditions (preprocess rs)"
and "{p. (common_matcher, in_doubt_allow),p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. simple_fw (to_simple_firewall (preprocess rs)) p = Decision FinalAllow ∧ newpkt p}"
unfolding check_simple_fw_preconditions_def preprocess_def
apply(clarify, rename_tac r, case_tac r, rename_tac m a, simp)
proof -
let ?rs2="upper_closure (packet_assume_new rs)"
let ?rs3="optimize_matches abstract_for_simple_firewall ?rs2"
let ?rs'="upper_closure ?rs3"
let ?γ="(common_matcher, in_doubt_allow)
:: ('i::len common_primitive, ('i, 'a) tagged_packet_scheme) match_tac"
let ?fw="λrs p. approximating_bigstep_fun ?γ p rs Undecided"
from packet_assume_new_simple_ruleset[OF simplers] have s1: "simple_ruleset (packet_assume_new rs)" .
from transform_upper_closure(2)[OF s1] have s2: "simple_ruleset ?rs2" .
from s2 have s3: "simple_ruleset ?rs3" by (simp add: optimize_matches_simple_ruleset)
from transform_upper_closure(2)[OF s3] have s4: "simple_ruleset ?rs'" .
from transform_upper_closure(3)[OF s1] have nnf2:
"∀r∈set (upper_closure (packet_assume_new rs)). normalized_nnf_match (get_match r)" by simp
{ fix m a
assume r: "Rule m a ∈ set ?rs'"
from s4 r have a: "(a = action.Accept ∨ a = action.Drop)" by(auto simp add: simple_ruleset_def)
have "r ∈ set (packet_assume_new rs) ⟹ ¬ has_disc is_CT_State (get_match r)" for r
by(simp add: packet_assume_new_def ctstate_assume_new_not_has_CT_State)
with transform_upper_closure(4)[OF s1, where disc=is_CT_State] have
"∀r∈set (upper_closure (packet_assume_new rs)). ¬ has_disc is_CT_State (get_match r)"
by simp
with abstract_primitive_preserves_nodisc[where disc'="is_CT_State"]
have "∀r∈set ?rs3. ¬ has_disc is_CT_State (get_match r)"
apply(intro optimize_matches_preserves)
by(auto simp add: abstract_for_simple_firewall_def)
with transform_upper_closure(4)[OF s3, where disc=is_CT_State] have
"∀r∈set ?rs'. ¬ has_disc is_CT_State (get_match r)" by simp
with r have no_CT: "¬ has_disc is_CT_State m" by fastforce
from abstract_for_simple_firewall_hasdisc have "∀r∈set ?rs3. ¬ has_disc is_L4_Flags (get_match r)"
by(intro optimize_matches_preserves, auto)
with transform_upper_closure(4)[OF s3, where disc=is_L4_Flags] have
"∀r∈set ?rs'. ¬ has_disc is_L4_Flags (get_match r)" by simp
with r have no_L4_Flags: "¬ has_disc is_L4_Flags m" by fastforce
from nnf2 abstract_for_simple_firewall_negated_ifaces_prots have
ifaces: "∀r∈set ?rs3. ¬ has_disc_negated (λa. is_Iiface a ∨ is_Oiface a) False (get_match r)" and
protocols_rs3: "∀r∈set ?rs3. ¬ has_disc_negated is_Prot False (get_match r)"
by(intro optimize_matches_preserves, blast)+
from ifaces have iface_in: "∀r∈set ?rs3. ¬ has_disc_negated is_Iiface False (get_match r)" and
iface_out: "∀r∈set ?rs3. ¬ has_disc_negated is_Oiface False (get_match r)"
using has_disc_negated_disj_split by blast+
from transform_upper_closure(3)[OF s3] have "∀r∈set ?rs'.
normalized_nnf_match (get_match r) ∧ normalized_src_ports (get_match r) ∧
normalized_dst_ports (get_match r) ∧ normalized_src_ips (get_match r) ∧
normalized_dst_ips (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r) ∧ ¬ has_disc is_Extra (get_match r)" .
with r have normalized:
"normalized_src_ports m ∧ normalized_dst_ports m ∧
normalized_src_ips m ∧ normalized_dst_ips m ∧
¬ has_disc is_MultiportPorts m & ¬ has_disc is_Extra m" by fastforce
from transform_upper_closure(5)[OF s3] iface_in iface_out have "∀r∈set ?rs'.
¬ has_disc_negated is_Iiface False (get_match r) ∧ ¬ has_disc_negated is_Oiface False (get_match r)" by simp
with r have abstracted_ifaces: "normalized_ifaces m"
unfolding normalized_ifaces_def has_disc_negated_disj_split by fastforce
from transform_upper_closure(3)[OF s1]
normalized_n_primitive_imp_not_disc_negated[OF wf_disc_sel_common_primitive(1)]
normalized_n_primitive_imp_not_disc_negated[OF wf_disc_sel_common_primitive(2)]
have "∀r∈ set ?rs2. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply(simp add: normalized_src_ports_def2 normalized_dst_ports_def2)
by blast
from this have "∀r∈set ?rs3. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply -
apply(rule optimize_matches_preserves)
apply(intro conjI)
apply(intro abstract_for_simple_firewall_preserves_nodisc_negated, simp_all)+
by (simp add: abstract_for_simple_firewall_def abstract_primitive_preserves_nodisc)
from this protocols_rs3 transform_upper_closure(5)[OF s3, where disc=is_Prot, simplified]
have "∀r∈set ?rs'. ¬ has_disc_negated is_Prot False (get_match r)"
by simp
with r have abstracted_prots: "normalized_protocols m"
unfolding normalized_protocols_def has_disc_negated_disj_split by fastforce
from no_CT no_L4_Flags s4 normalized a abstracted_ifaces abstracted_prots show "normalized_src_ports m ∧
normalized_dst_ports m ∧
normalized_src_ips m ∧
normalized_dst_ips m ∧
normalized_ifaces m ∧
normalized_protocols m ∧
¬ has_disc is_L4_Flags m ∧
¬ has_disc is_CT_State m ∧
¬ has_disc is_MultiportPorts m ∧
¬ has_disc is_Extra m ∧ (a = action.Accept ∨ a = action.Drop)"
by(simp)
}
hence simple_fw_preconditions: "check_simple_fw_preconditions ?rs'"
unfolding check_simple_fw_preconditions_def
by(clarify, rename_tac r, case_tac r, rename_tac m a, simp)
have 1: "{p. ?γ,p⊢ ⟨?rs', Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨?rs3, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_upper_closure(1)[OF s3])
by simp
from abstract_primitive_in_doubt_allow_generic(2)[OF primitive_matcher_generic_common_matcher nnf2 s2] have 2:
"{p. ?γ,p⊢ ⟨upper_closure (packet_assume_new rs), Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨?rs3, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
by(auto simp add: abstract_for_simple_firewall_def)
have 3: "{p. ?γ,p⊢ ⟨upper_closure (packet_assume_new rs), Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_upper_closure(1)[OF s1])
apply(subst approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF s1]])
apply(subst approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]])
using packet_assume_new newpkt_def by fastforce
have 4: "⋀p. ?γ,p⊢ ⟨?rs', Undecided⟩ ⇒⇩α Decision FinalAllow ⟷ ?fw ?rs' p = Decision FinalAllow"
using approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF s4]] by fast
have "{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨?rs', Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst 1)
apply(subst 3[symmetric])
using 2 by blast
thus "{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. simple_fw (to_simple_firewall ?rs') p = Decision FinalAllow ∧ newpkt p}"
apply safe
subgoal for p using to_simple_firewall[OF simple_fw_preconditions, where p = p] 4 by auto
done
qed
theorem transform_simple_fw_lower:
defines "preprocess rs ≡ lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new rs)))"
and "newpkt p ≡ match_tcp_flags ipt_tcp_syn (p_tcp_flags p) ∧ p_tag_ctstate p = CT_New"
assumes simplers: "simple_ruleset (rs:: 'i::len common_primitive rule list)"
shows "check_simple_fw_preconditions (preprocess rs)"
and "{p. simple_fw (to_simple_firewall (preprocess rs)) p = Decision FinalAllow ∧ newpkt p} ⊆
{p. (common_matcher, in_doubt_deny),p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
unfolding check_simple_fw_preconditions_def preprocess_def
apply(clarify, rename_tac r, case_tac r, rename_tac m a, simp)
proof -
let ?rs2="lower_closure (packet_assume_new rs)"
let ?rs3="optimize_matches abstract_for_simple_firewall ?rs2"
let ?rs'="lower_closure ?rs3"
let ?γ="(common_matcher, in_doubt_deny)
:: ('i::len common_primitive, ('i, 'a) tagged_packet_scheme) match_tac"
let ?fw="λrs p. approximating_bigstep_fun ?γ p rs Undecided"
from packet_assume_new_simple_ruleset[OF simplers] have s1: "simple_ruleset (packet_assume_new rs)" .
from transform_lower_closure(2)[OF s1] have s2: "simple_ruleset (lower_closure (packet_assume_new rs))" .
from s2 have s3: "simple_ruleset ?rs3" by (simp add: optimize_matches_simple_ruleset)
from transform_lower_closure(2)[OF s3] have s4: "simple_ruleset ?rs'" .
from transform_lower_closure(3)[OF s1] have nnf2:
"∀r∈set (lower_closure (packet_assume_new rs)). normalized_nnf_match (get_match r)" by simp
{ fix m a
assume r: "Rule m a ∈ set ?rs'"
from s4 r have a: "(a = action.Accept ∨ a = action.Drop)" by(auto simp add: simple_ruleset_def)
have "r ∈ set (packet_assume_new rs) ⟹ ¬ has_disc is_CT_State (get_match r)" for r
by(simp add: packet_assume_new_def ctstate_assume_new_not_has_CT_State)
with transform_lower_closure(4)[OF s1, where disc=is_CT_State] have
"∀r∈set (lower_closure (packet_assume_new rs)). ¬ has_disc is_CT_State (get_match r)"
by fastforce
with abstract_primitive_preserves_nodisc[where disc'="is_CT_State"] have
"∀r∈set ?rs3. ¬ has_disc is_CT_State (get_match r)"
apply(intro optimize_matches_preserves)
by(auto simp add: abstract_for_simple_firewall_def)
with transform_lower_closure(4)[OF s3, where disc=is_CT_State] have
"∀r∈set ?rs'. ¬ has_disc is_CT_State (get_match r)" by fastforce
with r have no_CT: "¬ has_disc is_CT_State m" by fastforce
from abstract_for_simple_firewall_hasdisc have "∀r∈set ?rs3. ¬ has_disc is_L4_Flags (get_match r)"
by(intro optimize_matches_preserves, blast)
with transform_lower_closure(4)[OF s3, where disc=is_L4_Flags] have
"∀r∈set ?rs'. ¬ has_disc is_L4_Flags (get_match r)" by fastforce
with r have no_L4_Flags: "¬ has_disc is_L4_Flags m" by fastforce
from nnf2 abstract_for_simple_firewall_negated_ifaces_prots have
ifaces: "∀r∈set ?rs3. ¬ has_disc_negated (λa. is_Iiface a ∨ is_Oiface a) False (get_match r)" and
protocols_rs3: "∀r∈set ?rs3. ¬ has_disc_negated is_Prot False (get_match r)"
by(intro optimize_matches_preserves, blast)+
from ifaces have iface_in: "∀r∈set ?rs3. ¬ has_disc_negated is_Iiface False (get_match r)" and
iface_out: "∀r∈set ?rs3. ¬ has_disc_negated is_Oiface False (get_match r)"
using has_disc_negated_disj_split by blast+
from transform_lower_closure(3)[OF s3] have "∀r∈set ?rs'.
normalized_nnf_match (get_match r) ∧ normalized_src_ports (get_match r) ∧
normalized_dst_ports (get_match r) ∧ normalized_src_ips (get_match r) ∧
normalized_dst_ips (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r) ∧ ¬ has_disc is_Extra (get_match r)" .
with r have normalized: "normalized_src_ports m ∧ normalized_dst_ports m ∧ normalized_src_ips m ∧
normalized_dst_ips m ∧ ¬ has_disc is_MultiportPorts m ∧ ¬ has_disc is_Extra m" by fastforce
from transform_lower_closure(5)[OF s3] iface_in iface_out have "∀r∈set ?rs'.
¬ has_disc_negated is_Iiface False (get_match r) ∧ ¬ has_disc_negated is_Oiface False (get_match r)" by simp
with r have abstracted_ifaces: "normalized_ifaces m"
unfolding normalized_ifaces_def has_disc_negated_disj_split by fastforce
from transform_lower_closure(3)[OF s1]
normalized_n_primitive_imp_not_disc_negated[OF wf_disc_sel_common_primitive(1)]
normalized_n_primitive_imp_not_disc_negated[OF wf_disc_sel_common_primitive(2)]
have "∀r∈set ?rs2. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply(simp add: normalized_src_ports_def2 normalized_dst_ports_def2)
by blast
from this have "∀r∈set ?rs3. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply -
apply(rule optimize_matches_preserves)
apply(intro conjI)
apply(intro abstract_for_simple_firewall_preserves_nodisc_negated, simp_all)+
by (simp add: abstract_for_simple_firewall_def abstract_primitive_preserves_nodisc)
from this protocols_rs3 transform_lower_closure(5)[OF s3, where disc=is_Prot, simplified]
have "∀r∈set ?rs'. ¬ has_disc_negated is_Prot False (get_match r)"
by simp
with r have abstracted_prots: "normalized_protocols m"
unfolding normalized_protocols_def has_disc_negated_disj_split by fastforce
from no_CT no_L4_Flags s4 normalized a abstracted_ifaces abstracted_prots show "normalized_src_ports m ∧
normalized_dst_ports m ∧
normalized_src_ips m ∧
normalized_dst_ips m ∧
normalized_ifaces m ∧
normalized_protocols m ∧ ¬ has_disc is_L4_Flags m ∧ ¬ has_disc is_CT_State m ∧
¬ has_disc is_MultiportPorts m ∧ ¬ has_disc is_Extra m ∧ (a = action.Accept ∨ a = action.Drop)"
by(simp)
}
hence simple_fw_preconditions: "check_simple_fw_preconditions ?rs'"
unfolding check_simple_fw_preconditions_def
by(clarify, rename_tac r, case_tac r, rename_tac m a, simp)
have 1: "{p. ?γ,p⊢ ⟨?rs', Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨?rs3, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_lower_closure(1)[OF s3])
by simp
from abstract_primitive_in_doubt_deny_generic(1)[OF primitive_matcher_generic_common_matcher nnf2 s2] have 2:
"{p. ?γ,p⊢ ⟨?rs3, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨lower_closure (packet_assume_new rs), Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
by(auto simp add: abstract_for_simple_firewall_def)
have 3: "{p. ?γ,p⊢ ⟨lower_closure (packet_assume_new rs), Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_lower_closure(1)[OF s1])
apply(subst approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF s1]])
apply(subst approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]])
using packet_assume_new newpkt_def by fastforce
have 4: "⋀p. ?γ,p⊢ ⟨?rs', Undecided⟩ ⇒⇩α Decision FinalAllow ⟷ ?fw ?rs' p = Decision FinalAllow"
using approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF s4]] by fast
have "{p. ?γ,p⊢ ⟨?rs', Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst 1)
apply(subst 3[symmetric])
using 2 by blast
thus "{p. simple_fw (to_simple_firewall ?rs') p = Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} "
apply safe
subgoal for p using to_simple_firewall[OF simple_fw_preconditions, where p = p] 4 by auto
done
qed
definition "to_simple_firewall_without_interfaces ipassmt rtblo rs ≡
to_simple_firewall
(upper_closure
(optimize_matches (abstract_primitive (λr. case r of Pos a ⇒ is_Iiface a ∨ is_Oiface a | Neg a ⇒ is_Iiface a ∨ is_Oiface a))
(optimize_matches abstract_for_simple_firewall
(upper_closure
(iface_try_rewrite ipassmt rtblo
(upper_closure
(packet_assume_new rs)))))))"
theorem to_simple_firewall_without_interfaces:
defines "newpkt p ≡ match_tcp_flags ipt_tcp_syn (p_tcp_flags p) ∧ p_tag_ctstate p = CT_New"
assumes simplers: "simple_ruleset (rs:: 'i::len common_primitive rule list)"
and wf_ipassmt1: "ipassmt_sanity_nowildcards (map_of ipassmt)" and wf_ipassmt2: "distinct (map fst ipassmt)"
and nospoofing: "∀(p::('i::len, 'a) tagged_packet_scheme).
∃ips. (map_of ipassmt) (Iface (p_iiface p)) = Some ips ∧ p_src p ∈ ipcidr_union_set (set ips)"
and routing_decided: "⋀rtbl (p::('i,'a) tagged_packet_scheme). rtblo = Some rtbl ⟹ output_iface (routing_table_semantics rtbl (p_dst p)) = p_oiface p"
and correct_routing: "⋀rtbl. rtblo = Some rtbl ⟹ correct_routing rtbl"
and routing_no_wildcards: "⋀rtbl. rtblo = Some rtbl ⟹ ipassmt_sanity_nowildcards (map_of (routing_ipassmt rtbl))"
shows "{p::('i,'a) tagged_packet_scheme. (common_matcher, in_doubt_allow),p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p::('i,'a) tagged_packet_scheme. simple_fw (to_simple_firewall_without_interfaces ipassmt rtblo rs) p = Decision FinalAllow ∧ newpkt p}"
and "∀r ∈ set (to_simple_firewall_without_interfaces ipassmt rtblo rs).
iiface (match_sel r) = ifaceAny ∧ oiface (match_sel r) = ifaceAny"
proof -
let ?rs1="packet_assume_new rs"
let ?rs2="upper_closure ?rs1"
let ?rs3="iface_try_rewrite ipassmt rtblo ?rs2"
let ?rs4="upper_closure ?rs3"
let ?rs5="optimize_matches abstract_for_simple_firewall ?rs4"
let ?rs6="optimize_matches (abstract_primitive (λr. case r of Pos a ⇒ is_Iiface a ∨ is_Oiface a | Neg a ⇒ is_Iiface a ∨ is_Oiface a)) ?rs5"
let ?rs7="upper_closure ?rs6"
let ?γ="(common_matcher, in_doubt_allow)
:: ('i::len common_primitive, ('i, 'a) tagged_packet_scheme) match_tac"
have "to_simple_firewall_without_interfaces ipassmt rtblo rs = to_simple_firewall ?rs7"
by(simp add: to_simple_firewall_without_interfaces_def)
from packet_assume_new_simple_ruleset[OF simplers] have s1: "simple_ruleset ?rs1" .
from transform_upper_closure(2)[OF s1] have s2: "simple_ruleset ?rs2" .
from iface_try_rewrite_simplers[OF s2] have s3: "simple_ruleset ?rs3" .
from transform_upper_closure(2)[OF s3] have s4: "simple_ruleset ?rs4" .
from optimize_matches_simple_ruleset[OF s4] have s5: "simple_ruleset ?rs5" .
from optimize_matches_simple_ruleset[OF s5] have s6: "simple_ruleset ?rs6" .
from transform_upper_closure(2)[OF s6] have s7: "simple_ruleset ?rs7" .
from transform_upper_closure(3)[OF s1] have nnf2: "∀r∈set ?rs2. normalized_nnf_match (get_match r)" by simp
from transform_upper_closure(3)[OF s3] have nnf4: "∀r∈set ?rs4. normalized_nnf_match (get_match r)" by simp
have nnf5: "∀r∈set ?rs5. normalized_nnf_match (get_match r)"
apply(intro optimize_matches_preserves)
apply(simp add: abstract_for_simple_firewall_def)
apply(rule abstract_primitive_preserves_normalized(5))
using nnf4 by(simp)
have nnf6: "∀r∈set ?rs6. normalized_nnf_match (get_match r)"
apply(intro optimize_matches_preserves)
apply(rule abstract_primitive_preserves_normalized(5))
using nnf5 by(simp)
from transform_upper_closure(3)[OF s6] have nnf7: "∀r∈set ?rs7. normalized_nnf_match (get_match r)" by simp
{ fix m a
assume r: "Rule m a ∈ set ?rs7"
from s7 r have a: "(a = action.Accept ∨ a = action.Drop)" by(auto simp add: simple_ruleset_def)
from abstract_for_simple_firewall_hasdisc have "∀r∈set ?rs5. ¬ has_disc is_CT_State (get_match r)"
by(intro optimize_matches_preserves, blast)
with abstract_primitive_preserves_nodisc[where disc'="is_CT_State"] have
"∀r∈set ?rs6. ¬ has_disc is_CT_State (get_match r)"
apply(intro optimize_matches_preserves)
apply(simp)
by blast
with transform_upper_closure(4)[OF s6, where disc=is_CT_State] have
"∀r∈set ?rs7. ¬ has_disc is_CT_State (get_match r)" by simp
with r have no_CT: "¬ has_disc is_CT_State m" by fastforce
from abstract_for_simple_firewall_hasdisc have "∀r∈set ?rs5. ¬ has_disc is_L4_Flags (get_match r)"
by(intro optimize_matches_preserves, blast)
with abstract_primitive_preserves_nodisc[where disc'="is_L4_Flags"] have
"∀r∈set ?rs6. ¬ has_disc is_L4_Flags (get_match r)"
by(intro optimize_matches_preserves) auto
with transform_upper_closure(4)[OF s6, where disc=is_L4_Flags] have
"∀r∈set ?rs7. ¬ has_disc is_L4_Flags (get_match r)" by simp
with r have no_L4_Flags: "¬ has_disc is_L4_Flags m" by fastforce
have "∀r∈set ?rs6. ¬ has_disc is_Iiface (get_match r)"
by(intro optimize_matches_preserves abstract_primitive_nodisc) simp+
with transform_upper_closure(4)[OF s6, where disc=is_Iiface] have
"∀r∈set ?rs7. ¬ has_disc is_Iiface (get_match r)" by simp
with r have no_Iiface: "¬ has_disc is_Iiface m" by fastforce
have "∀r∈set ?rs6. ¬ has_disc is_Oiface (get_match r)"
by(intro optimize_matches_preserves abstract_primitive_nodisc) simp+
with transform_upper_closure(4)[OF s6, where disc=is_Oiface] have
"∀r∈set ?rs7. ¬ has_disc is_Oiface (get_match r)" by simp
with r have no_Oiface: "¬ has_disc is_Oiface m" by fastforce
from no_Iiface no_Oiface have normalized_ifaces: "normalized_ifaces m"
using has_disc_negated_disj_split has_disc_negated_has_disc normalized_ifaces_def by blast
from transform_upper_closure(3)[OF s6] r have normalized:
"normalized_src_ports m ∧ normalized_dst_ports m ∧
normalized_src_ips m ∧ normalized_dst_ips m ∧
¬ has_disc is_MultiportPorts m ∧ ¬ has_disc is_Extra m" by fastforce
from transform_upper_closure(3)[OF s3, simplified]
normalized_n_primitive_imp_not_disc_negated[OF wf_disc_sel_common_primitive(1)]
normalized_n_primitive_imp_not_disc_negated[OF wf_disc_sel_common_primitive(2)]
have "∀r ∈ set ?rs4. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply(simp add: normalized_src_ports_def2 normalized_dst_ports_def2)
by blast
hence "∀r ∈ set ?rs5. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply -
apply(rule optimize_matches_preserves)
apply(intro conjI)
apply(intro abstract_for_simple_firewall_preserves_nodisc_negated, simp_all)+
by (simp add: abstract_for_simple_firewall_def abstract_primitive_preserves_nodisc)
from this have no_ports_rs6:
"∀r ∈ set ?rs6. ¬ has_disc_negated is_Src_Ports False (get_match r) ∧
¬ has_disc_negated is_Dst_Ports False (get_match r) ∧
¬ has_disc is_MultiportPorts (get_match r)"
apply -
apply(rule optimize_matches_preserves)
apply(intro conjI)
apply(intro abstract_primitive_preserves_nodisc_nedgated, simp_all)+
by (simp add: abstract_for_simple_firewall_def abstract_primitive_preserves_nodisc)
from nnf4 abstract_for_simple_firewall_negated_ifaces_prots(2) have
"∀r∈set ?rs5. ¬ has_disc_negated is_Prot False (get_match r)"
by(intro optimize_matches_preserves) blast
hence "∀r∈set ?rs6. ¬ has_disc_negated is_Prot False (get_match r)"
by(intro optimize_matches_preserves abstract_primitive_preserves_nodisc_nedgated) simp+
with no_ports_rs6 have "∀r∈set ?rs7. ¬ has_disc_negated is_Prot False (get_match r)"
by(intro transform_upper_closure(5)[OF s6]) simp+
with r have protocols: "normalized_protocols m" unfolding normalized_protocols_def by fastforce
from no_CT no_L4_Flags normalized a normalized_ifaces protocols no_Iiface no_Oiface
have "normalized_src_ports m ∧
normalized_dst_ports m ∧
normalized_src_ips m ∧
normalized_dst_ips m ∧
normalized_ifaces m ∧
normalized_protocols m ∧
¬ has_disc is_L4_Flags m ∧
¬ has_disc is_CT_State m ∧
¬ has_disc is_MultiportPorts m ∧
¬ has_disc is_Extra m ∧ (a = action.Accept ∨ a = action.Drop)"
and "¬ has_disc is_Iiface m" and "¬ has_disc is_Oiface m"
apply -
by(simp)+
}
hence simple_fw_preconditions: "check_simple_fw_preconditions ?rs7"
and no_interfaces: "Rule m a ∈ set ?rs7 ⟹ ¬ has_disc is_Iiface m ∧ ¬ has_disc is_Oiface m" for m a
apply -
subgoal unfolding check_simple_fw_preconditions_def by(clarify, rename_tac r, case_tac r, rename_tac m a, simp)
by simp
have "{p :: ('i,'a) tagged_packet_scheme. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p :: ('i,'a) tagged_packet_scheme. ?γ,p⊢ ⟨?rs1, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF s1]])
apply(subst approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF simplers]])
apply(rule Collect_cong)
subgoal for p using packet_assume_new[where p = p] newpkt_def[where p = p] by auto
done
also have "{p. ?γ,p⊢ ⟨?rs1, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨?rs2, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_upper_closure(1)[OF s1])
by simp
also have "… = {p. ?γ,p⊢ ⟨?rs3, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(cases rtblo; simp; (subst iface_try_rewrite_rtbl[OF s2 nnf2] | subst iface_try_rewrite_no_rtbl[OF s2 nnf2]))
using wf_ipassmt1 wf_ipassmt2 nospoofing wf_in_doubt_allow routing_no_wildcards correct_routing routing_decided by simp_all
also have "… = {p. ?γ,p⊢ ⟨?rs4, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_upper_closure(1)[OF s3])
by simp
finally have 1: "{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨?rs4, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}" .
from abstract_primitive_in_doubt_allow_generic(2)[OF primitive_matcher_generic_common_matcher nnf4 s4] have 2:
"{p. ?γ,p⊢ ⟨?rs4, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨?rs5, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
by(auto simp add: abstract_for_simple_firewall_def)
from abstract_primitive_in_doubt_allow_generic(2)[OF primitive_matcher_generic_common_matcher nnf5 s5] have 3:
"{p. ?γ,p⊢ ⟨?rs5, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨?rs6, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
by(auto simp add: abstract_for_simple_firewall_def)
have 4: "{p. ?γ,p⊢ ⟨?rs6, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} =
{p. ?γ,p⊢ ⟨?rs7, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}"
apply(subst transform_upper_closure(1)[OF s6])
by simp
let ?fw="λrs p. approximating_bigstep_fun ?γ p rs Undecided"
have approximating_rule: "⋀p. ?γ,p⊢ ⟨?rs7, Undecided⟩ ⇒⇩α Decision FinalAllow ⟷ ?fw ?rs7 p = Decision FinalAllow"
using approximating_semantics_iff_fun_good_ruleset[OF simple_imp_good_ruleset[OF s7]] by fast
from 1 2 3 4 have "{p. ?γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. ?γ,p⊢ ⟨?rs7, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p}" by blast
thus "{p. (common_matcher, in_doubt_allow),p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ∧ newpkt p} ⊆
{p. simple_fw (to_simple_firewall_without_interfaces ipassmt rtblo rs) p = Decision FinalAllow ∧ newpkt p}"
apply(safe)
subgoal for p
unfolding to_simple_firewall_without_interfaces_def
using to_simple_firewall[OF simple_fw_preconditions, where p = p] approximating_rule[where p = p] by auto
done
have common_primitive_match_to_simple_match_nodisc:
"Some sm = common_primitive_match_to_simple_match m' ⟹
¬ has_disc is_Iiface m' ∧ ¬ has_disc is_Oiface m' ⟹ iiface sm = ifaceAny ∧ oiface sm = ifaceAny"
if prems: "check_simple_fw_preconditions [Rule m' a']"
for m' :: "'i common_primitive match_expr" and a' sm
using prems proof(induction m' arbitrary: sm rule: common_primitive_match_to_simple_match.induct)
case 18 thus ?case
by(simp add: check_simple_fw_preconditions_def normalized_protocols_def)
next
case (13 m1 m2) thus ?case
apply(simp add: check_simple_fw_preconditions_def)
apply(case_tac "common_primitive_match_to_simple_match m1")
apply(simp; fail)
apply(case_tac "common_primitive_match_to_simple_match m2")
apply(simp; fail)
apply simp
apply(rename_tac a aa)
apply(case_tac a)
apply(case_tac aa)
apply(simp)
apply(simp split: option.split_asm)
using iface_conjunct_ifaceAny normalized_ifaces_def normalized_protocols_def
by (metis has_disc_negated.simps(4) option.inject)
qed(simp_all add: check_simple_fw_preconditions_def simple_match_any_def)
have to_simple_firewall_no_ifaces: "(⋀m a. Rule m a ∈ set rs ⟹ ¬ has_disc is_Iiface m ∧ ¬ has_disc is_Oiface m) ⟹
∀r∈set (to_simple_firewall rs). iiface (match_sel r) = ifaceAny ∧ oiface (match_sel r) = ifaceAny"
if pre1: "check_simple_fw_preconditions rs" for rs :: "'i common_primitive rule list"
using pre1 apply(induction rs)
apply(simp add: to_simple_firewall_simps; fail)
apply simp
apply(subgoal_tac "check_simple_fw_preconditions rs")
prefer 2
subgoal by(simp add: check_simple_fw_preconditions_def)
apply(rename_tac r rs, case_tac r)
apply simp
apply(simp add: to_simple_firewall_simps)
apply(simp split: option.split)
apply(intro conjI)
apply blast
apply(intro allI impI)
apply(subgoal_tac "(∀m∈set (to_simple_firewall rs). iiface (match_sel m) = ifaceAny ∧ oiface (match_sel m) = ifaceAny)")
prefer 2
subgoal by blast
apply(simp)
apply(rename_tac m' a' sm)
apply(subgoal_tac " ¬ has_disc is_Iiface m' ∧ ¬ has_disc is_Oiface m'")
prefer 2
subgoal by blast
apply(subgoal_tac "check_simple_fw_preconditions [Rule m' a']")
prefer 2
subgoal by(simp add: check_simple_fw_preconditions_def)
apply(drule common_primitive_match_to_simple_match_nodisc)
apply(simp_all)
done
from to_simple_firewall_no_ifaces[OF simple_fw_preconditions no_interfaces] show
"∀r ∈ set (to_simple_firewall_without_interfaces ipassmt rtblo rs). iiface (match_sel r) = ifaceAny ∧ oiface (match_sel r) = ifaceAny"
unfolding to_simple_firewall_without_interfaces_def
by(simp add: to_simple_firewall_def simple_fw_preconditions)
qed
end