Theory Ipassmt
theory Ipassmt
imports Common_Primitive_Syntax
"../Semantics_Ternary/Primitive_Normalization"
Simple_Firewall.Iface
Simple_Firewall.IP_Addr_WordInterval_toString
Automatic_Refinement.Misc
begin
hide_const Misc.uncurry
hide_fact Misc.uncurry_def
text‹A mapping from an interface to its assigned ip addresses in CIDR notation›
type_synonym 'i ipassignment="iface ⇀ ('i word × nat) list"
subsection‹Sanity checking for an @{typ "'i ipassignment"}.›
text‹warning if interface map has wildcards›
definition ipassmt_sanity_nowildcards :: "'i ipassignment ⇒ bool" where
"ipassmt_sanity_nowildcards ipassmt ≡ ∀ iface ∈ dom ipassmt. ¬ iface_is_wildcard iface"
text‹Executable of the @{typ "'i ipassignment"} is given as a list.›
lemma[code_unfold]: "ipassmt_sanity_nowildcards (map_of ipassmt) ⟷ (∀ iface ∈ fst` set ipassmt. ¬ iface_is_wildcard iface)"
by(simp add: ipassmt_sanity_nowildcards_def Map.dom_map_of_conv_image_fst)
lemma ipassmt_sanity_nowildcards_match_iface:
"ipassmt_sanity_nowildcards ipassmt ⟹
ipassmt (Iface ifce2) = None ⟹
ipassmt ifce = Some a ⟹
¬ match_iface ifce ifce2"
unfolding ipassmt_sanity_nowildcards_def
by (metis domIff iface.exhaust iface.sel option.distinct(1) iface_is_wildcard_def match_iface_case_nowildcard)
definition map_of_ipassmt :: "(iface × ('i word × nat) list) list ⇒ iface ⇀ ('i word × nat) list" where
"map_of_ipassmt ipassmt = (
if
distinct (map fst ipassmt) ∧ ipassmt_sanity_nowildcards (map_of ipassmt)
then
map_of ipassmt
else undefined )"
text‹some additional (optional) sanity checks›
text‹sanity check that there are no zone-spanning interfaces›
definition ipassmt_sanity_disjoint :: "'i::len ipassignment ⇒ bool" where
"ipassmt_sanity_disjoint ipassmt ≡ ∀ i1 ∈ dom ipassmt. ∀ i2 ∈ dom ipassmt. i1 ≠ i2 ⟶
ipcidr_union_set (set (the (ipassmt i1))) ∩ ipcidr_union_set (set (the (ipassmt i2))) = {}"
lemma[code_unfold]: "ipassmt_sanity_disjoint (map_of ipassmt) ⟷
(let Is = fst` set ipassmt in
(∀ i1 ∈ Is. ∀ i2 ∈ Is. i1 ≠ i2 ⟶ wordinterval_empty (wordinterval_intersection (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i1)))) (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i2)))))))"
apply(simp add: ipassmt_sanity_disjoint_def Map.dom_map_of_conv_image_fst)
apply(simp add: ipcidr_union_set_def)
apply(simp add: l2wi)
apply(simp add: ipcidr_to_interval_def)
using ipset_from_cidr_ipcidr_to_interval by blast
text‹Checking that the ipassmt covers the complete ipv4 address space.›
definition ipassmt_sanity_complete :: "(iface × ('i::len word × nat) list) list ⇒ bool" where
"ipassmt_sanity_complete ipassmt ≡ distinct (map fst ipassmt) ∧ (⋃(ipcidr_union_set ` set ` (ran (map_of ipassmt)))) = UNIV"
lemma[code_unfold]: "ipassmt_sanity_complete ipassmt ⟷ distinct (map fst ipassmt) ∧ (let range = map snd ipassmt in
wordinterval_eq (wordinterval_Union (map (l2wi ∘ (map ipcidr_to_interval)) range)) wordinterval_UNIV
)"
apply(cases "distinct (map fst ipassmt)")
apply(simp add: ipassmt_sanity_complete_def)
apply(simp add: Map.ran_distinct)
apply(simp add: wordinterval_eq_set_eq wordinterval_Union)
apply(simp add: l2wi)
apply(simp add: ipcidr_to_interval_def)
apply(simp add: ipcidr_union_set_def ipset_from_cidr_ipcidr_to_interval; fail)
apply(simp add: ipassmt_sanity_complete_def)
done
value[code] "ipassmt_sanity_nowildcards (map_of [(Iface ''eth1.1017'', [(ipv4addr_of_dotdecimal (131,159,14,240), 28)])])"
fun collect_ifaces' :: "'i::len common_primitive rule list ⇒ iface list" where
"collect_ifaces' [] = []" |
"collect_ifaces' ((Rule m a)#rs) = filter (λiface. iface ≠ ifaceAny) (
(map (λx. case x of Pos i ⇒ i | Neg i ⇒ i) (fst (primitive_extractor (is_Iiface, iiface_sel) m))) @
(map (λx. case x of Pos i ⇒ i | Neg i ⇒ i) (fst (primitive_extractor (is_Oiface, oiface_sel) m))) @ collect_ifaces' rs)"
definition collect_ifaces :: "'i::len common_primitive rule list ⇒ iface list" where
"collect_ifaces rs ≡ mergesort_remdups (collect_ifaces' rs)"
lemma "set (collect_ifaces rs) = set (collect_ifaces' rs)"
by(simp add: collect_ifaces_def mergesort_remdups_correct)
text‹sanity check that all interfaces mentioned in the ruleset are also listed in the ipassmt. May fail for wildcard interfaces in the ruleset.›
definition ipassmt_sanity_defined :: "'i::len common_primitive rule list ⇒ 'i ipassignment ⇒ bool" where
"ipassmt_sanity_defined rs ipassmt ≡ ∀ iface ∈ set (collect_ifaces rs). iface ∈ dom ipassmt"
lemma[code]: "ipassmt_sanity_defined rs ipassmt ⟷ (∀ iface ∈ set (collect_ifaces rs). ipassmt iface ≠ None)"
by(simp add: ipassmt_sanity_defined_def Map.domIff)
lemma "ipassmt_sanity_defined [
Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (Match (IIface (Iface ''eth1.1017'')))) action.Accept,
Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (Match (IIface (ifaceAny)))) action.Accept,
Rule MatchAny action.Drop]
(map_of [(Iface ''eth1.1017'', [(ipv4addr_of_dotdecimal (131,159,14,240), 28)])])" by eval
definition ipassmt_ignore_wildcard :: "'i::len ipassignment ⇒ 'i ipassignment" where
"ipassmt_ignore_wildcard ipassmt ≡ λk. case ipassmt k of None ⇒ None
| Some ips ⇒ if ipcidr_union_set (set ips) = UNIV then None else Some ips"
lemma ipassmt_ignore_wildcard_le: "ipassmt_ignore_wildcard ipassmt ⊆⇩m ipassmt"
apply(simp add: ipassmt_ignore_wildcard_def map_le_def)
apply(clarify)
apply(simp split: option.split_asm if_split_asm)
done
definition ipassmt_ignore_wildcard_list:: "(iface × ('i::len word × nat) list) list ⇒ (iface × ('i word × nat) list) list" where
"ipassmt_ignore_wildcard_list ipassmt = filter (λ(_,ips). ¬ wordinterval_eq (l2wi (map ipcidr_to_interval ips)) wordinterval_UNIV) ipassmt"
lemma "distinct (map fst ipassmt) ⟹
map_of (ipassmt_ignore_wildcard_list ipassmt) = ipassmt_ignore_wildcard (map_of ipassmt)"
apply(simp add: ipassmt_ignore_wildcard_list_def ipassmt_ignore_wildcard_def)
apply(simp add: wordinterval_eq_set_eq)
apply(simp add: l2wi)
apply(simp add: ipcidr_to_interval_def)
apply(simp add: fun_eq_iff)
apply(clarify)
apply(induction ipassmt)
apply(simp; fail)
apply(simp)
apply(simp split:option.split option.split_asm)
apply(simp add: ipcidr_union_set_def ipset_from_cidr_ipcidr_to_interval)
apply(simp add: case_prod_unfold)
by blast
text‹Debug algorithm with human-readable output›
definition debug_ipassmt_generic
:: "('i::len wordinterval ⇒ string) ⇒
(iface × ('i word × nat) list) list ⇒ 'i common_primitive rule list ⇒ string list" where
"debug_ipassmt_generic toStr ipassmt rs ≡ let ifaces = (map fst ipassmt) in [
''distinct: '' @ (if distinct ifaces then ''passed'' else ''FAIL!'')
, ''ipassmt_sanity_nowildcards: '' @
(if ipassmt_sanity_nowildcards (map_of ipassmt)
then ''passed'' else ''fail: ''@list_toString iface_sel (filter iface_is_wildcard ifaces))
, ''ipassmt_sanity_defined (interfaces defined in the ruleset are also in ipassmt): '' @
(if ipassmt_sanity_defined rs (map_of ipassmt)
then ''passed'' else ''fail: ''@list_toString iface_sel [i ← (collect_ifaces rs). i ∉ set ifaces])
, ''ipassmt_sanity_disjoint (no zone-spanning interfaces): '' @
(if ipassmt_sanity_disjoint (map_of ipassmt)
then ''passed'' else ''fail: ''@list_toString (λ(i1,i2). ''('' @ iface_sel i1 @ '','' @ iface_sel i2 @ '')'')
[(i1,i2) ← List.product ifaces ifaces. i1 ≠ i2 ∧
¬ wordinterval_empty (wordinterval_intersection
(l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i1))))
(l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i2)))))
])
, ''ipassmt_sanity_disjoint excluding UNIV interfaces: '' @
(let ipassmt = ipassmt_ignore_wildcard_list ipassmt;
ifaces = (map fst ipassmt)
in
(if ipassmt_sanity_disjoint (map_of ipassmt)
then ''passed'' else ''fail: ''@list_toString (λ(i1,i2). ''('' @ iface_sel i1 @ '','' @ iface_sel i2 @ '')'')
[(i1,i2) ← List.product ifaces ifaces. i1 ≠ i2 ∧
¬ wordinterval_empty (wordinterval_intersection
(l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i1))))
(l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i2)))))
]))
, ''ipassmt_sanity_complete: '' @
(if ipassmt_sanity_complete ipassmt
then ''passed''
else ''the following is not covered: '' @
toStr (wordinterval_setminus wordinterval_UNIV (wordinterval_Union (map (l2wi ∘ (map ipcidr_to_interval)) (map snd ipassmt)))))
, ''ipassmt_sanity_complete excluding UNIV interfaces: '' @
(let ipassmt = ipassmt_ignore_wildcard_list ipassmt
in
(if ipassmt_sanity_complete ipassmt
then ''passed''
else ''the following is not covered: '' @
toStr (wordinterval_setminus wordinterval_UNIV (wordinterval_Union (map (l2wi ∘ (map ipcidr_to_interval)) (map snd ipassmt))))))
]"
definition "debug_ipassmt_ipv4 ≡ debug_ipassmt_generic ipv4addr_wordinterval_toString"
definition "debug_ipassmt_ipv6 ≡ debug_ipassmt_generic ipv6addr_wordinterval_toString"
lemma dom_ipassmt_ignore_wildcard:
"i∈dom (ipassmt_ignore_wildcard ipassmt) ⟷ i ∈ dom ipassmt ∧ ipcidr_union_set (set (the (ipassmt i))) ≠ UNIV"
apply(simp add: ipassmt_ignore_wildcard_def)
apply(rule)
apply(clarify)
apply(simp split: option.split_asm if_split_asm)
apply blast
apply(clarify)
apply(simp)
done
lemma ipassmt_ignore_wildcard_the:
"ipassmt i = Some ips ⟹ ipcidr_union_set (set ips) ≠ UNIV ⟹ (the (ipassmt_ignore_wildcard ipassmt i)) = ips"
"ipassmt_ignore_wildcard ipassmt i = Some ips ⟹ the (ipassmt i) = ips"
"ipassmt_ignore_wildcard ipassmt i = Some ips ⟹ ipcidr_union_set (set ips) ≠ UNIV"
by (simp_all add: ipassmt_ignore_wildcard_def split: option.split_asm if_split_asm)
lemma ipassmt_sanity_disjoint_ignore_wildcards:
"ipassmt_sanity_disjoint (ipassmt_ignore_wildcard ipassmt) ⟷
(∀i1∈dom ipassmt.
∀i2∈dom ipassmt.
ipcidr_union_set (set (the (ipassmt i1))) ≠ UNIV ∧
ipcidr_union_set (set (the (ipassmt i2))) ≠ UNIV ∧
i1 ≠ i2
⟶ ipcidr_union_set (set (the (ipassmt i1))) ∩ ipcidr_union_set (set (the (ipassmt i2))) = {})"
apply(simp add: ipassmt_sanity_disjoint_def)
apply(rule)
apply(clarify)
apply(simp)
subgoal for i1 i2 ips1 ips2
apply(erule_tac x=i1 in ballE)
prefer 2
using dom_ipassmt_ignore_wildcard apply (metis domI option.sel)
apply(erule_tac x=i2 in ballE)
prefer 2
using dom_ipassmt_ignore_wildcard apply (metis domI domIff option.sel)
by(simp add: ipassmt_ignore_wildcard_the; fail)
apply(clarify)
apply(simp)
subgoal for i1 i2 ips1 ips2
apply(erule_tac x=i1 in ballE)
prefer 2
using dom_ipassmt_ignore_wildcard apply auto[1]
apply(erule_tac x=i2 in ballE)
prefer 2
using dom_ipassmt_ignore_wildcard apply auto[1]
by(simp add: ipassmt_ignore_wildcard_the)
done
text‹Confusing names: @{const ipassmt_sanity_nowildcards} refers to wildcard interfaces.
@{const ipassmt_ignore_wildcard} refers to the UNIV ip range.
›
lemma ipassmt_sanity_nowildcards_ignore_wildcardD:
"ipassmt_sanity_nowildcards ipassmt ⟹ ipassmt_sanity_nowildcards (ipassmt_ignore_wildcard ipassmt)"
by (simp add: dom_ipassmt_ignore_wildcard ipassmt_sanity_nowildcards_def)
lemma ipassmt_disjoint_nonempty_inj:
assumes ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
and ifce: "ipassmt ifce = Some i_ips"
and a: "ipcidr_union_set (set i_ips) ≠ {}"
and k: "ipassmt k = Some i_ips"
shows "k = ifce"
proof(rule ccontr)
assume "k ≠ ifce"
with ifce k ipassmt_disjoint have "ipcidr_union_set (set (the (ipassmt k))) ∩ ipcidr_union_set (set (the (ipassmt ifce))) = {}"
unfolding ipassmt_sanity_disjoint_def by fastforce
thus False using a ifce k by auto
qed
lemma ipassmt_ignore_wildcard_None_Some:
"ipassmt_ignore_wildcard ipassmt ifce = None ⟹ ipassmt ifce = Some ips ⟹ ipcidr_union_set (set ips) = UNIV"
by (metis domI domIff dom_ipassmt_ignore_wildcard option.sel)
lemma ipassmt_disjoint_ignore_wildcard_nonempty_inj:
assumes ipassmt_disjoint: "ipassmt_sanity_disjoint (ipassmt_ignore_wildcard ipassmt)"
and ifce: "ipassmt ifce = Some i_ips"
and a: "ipcidr_union_set (set i_ips) ≠ {}"
and k: "(ipassmt_ignore_wildcard ipassmt) k = Some i_ips"
shows "k = ifce"
proof(rule ccontr)
assume "k ≠ ifce"
show False
proof(cases "(ipassmt_ignore_wildcard ipassmt) ifce")
case (Some i_ips')
hence "i_ips' = i_ips" using ifce ipassmt_ignore_wildcard_the(2) by fastforce
hence "(ipassmt_ignore_wildcard ipassmt) k = Some i_ips" using Some ifce ipassmt_ignore_wildcard_def k by auto
thus False using Some ‹i_ips' = i_ips› ‹k ≠ ifce› a ipassmt_disjoint ipassmt_disjoint_nonempty_inj by blast
next
case None
with ipassmt_ignore_wildcard_None_Some have "ipcidr_union_set (set i_ips) = UNIV" using ifce by auto
thus False using ipassmt_ignore_wildcard_the(3) k by blast
qed
qed
lemma ipassmt_disjoint_inj_k:
assumes ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
and ifce: "ipassmt ifce = Some ips"
and k: "ipassmt k = Some ips'"
and a: "p ∈ ipcidr_union_set (set ips)"
and b: "p ∈ ipcidr_union_set (set ips')"
shows "k = ifce"
proof(rule ccontr)
assume "k ≠ ifce"
with ipassmt_disjoint have
"ipcidr_union_set (set (the (ipassmt k))) ∩ ipcidr_union_set (set (the (ipassmt ifce))) = {}"
unfolding ipassmt_sanity_disjoint_def using ifce k by blast
hence "ipcidr_union_set (set ips') ∩ ipcidr_union_set (set ips) = {}" by(simp add: k ifce)
thus False using a b by blast
qed
lemma ipassmt_disjoint_matcheq_iifce_srcip:
assumes ipassmt_nowild: "ipassmt_sanity_nowildcards ipassmt"
and ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
and ifce: "ipassmt ifce = Some i_ips"
and p_ifce: "ipassmt (Iface (p_iiface p)) = Some p_ips ∧ p_src p ∈ ipcidr_union_set (set p_ips)"
shows "match_iface ifce (p_iiface p) ⟷ p_src p ∈ ipcidr_union_set (set i_ips)"
proof
assume "match_iface ifce (p_iiface p)"
thus "p_src p ∈ ipcidr_union_set (set i_ips)"
apply(cases "ifce = Iface (p_iiface p)")
using ifce p_ifce apply force
by (metis domI iface.sel iface_is_wildcard_def ifce ipassmt_nowild ipassmt_sanity_nowildcards_def match_iface.elims(2) match_iface_case_nowildcard)
next
assume a: "p_src p ∈ ipcidr_union_set (set i_ips)"
from ipassmt_disjoint_nonempty_inj[OF ipassmt_disjoint ifce] a have ipassmt_inj: "∀k. ipassmt k = Some i_ips ⟶ k = ifce" by blast
from ipassmt_disjoint_inj_k[OF ipassmt_disjoint ifce _ a] have ipassmt_inj_k:
"⋀k ips'. ipassmt k = Some ips' ⟹ p_src p ∈ ipcidr_union_set (set ips') ⟹ k = ifce" by simp
have ipassmt_inj_p: "∀ips'. p_src p ∈ ipcidr_union_set (set ips') ∧ (∃k. ipassmt k = Some ips') ⟶ ips' = i_ips"
apply(clarify)
apply(rename_tac ips' k)
apply(subgoal_tac "k = ifce")
using ifce apply simp
using ipassmt_inj_k by simp
from p_ifce have "(Iface (p_iiface p)) = ifce" using ipassmt_inj_p ipassmt_inj by blast
thus "match_iface ifce (p_iiface p)" using match_iface_refl by blast
qed
definition ipassmt_generic_ipv4 :: "(iface × (32 word × nat) list) list" where
"ipassmt_generic_ipv4 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)])]"
definition ipassmt_generic_ipv6 :: "(iface × (128 word × nat) list) list" where
"ipassmt_generic_ipv6 = [(Iface ''lo'', [(1,128)])]"
subsection‹IP Assignment difference›
text‹Compare two ipassmts. Returns a list of tuples
First entry of the tuple: things which are in the left ipassmt but not in the right.
Second entry of the tupls: things which are in the right ipassmt but not in the left.›
definition ipassmt_diff
:: "(iface × ('i::len word × nat) list) list ⇒ (iface × ('i::len word × nat) list) list
⇒ (iface × ('i word × nat) list × ('i word × nat) list) list"
where
"ipassmt_diff a b ≡ let
t = λs. (case s of None ⇒ Empty_WordInterval
| Some s ⇒ wordinterval_Union (map ipcidr_tuple_to_wordinterval s));
k = λx y d. cidr_split (wordinterval_setminus (t (map_of x d)) (t (map_of y d)))
in
[(d, (k a b d, k b a d)). d ← remdups (map fst (a @ b))]"
text‹If an interface is defined in both ipassignments and there is no difference
then the two ipassignements describe the same IP range for this interface.›
lemma ipassmt_diff_ifce_equal: "(ifce, [], []) ∈ set (ipassmt_diff ipassmt1 ipassmt2) ⟹
ifce ∈ dom (map_of ipassmt1) ⟹ ifce ∈ dom (map_of ipassmt2) ⟹
ipcidr_union_set (set (the ((map_of ipassmt1) ifce))) =
ipcidr_union_set (set (the ((map_of ipassmt2) ifce)))"
proof -
have cidr_empty: "[] = cidr_split r ⟹ wordinterval_to_set r = {}" for r :: "'a wordinterval"
apply(subst cidr_split_prefix[symmetric])
by(simp)
show "(ifce, [], []) ∈ set (ipassmt_diff ipassmt1 ipassmt2) ⟹
ifce ∈ dom (map_of ipassmt1) ⟹ ifce ∈ dom (map_of ipassmt2) ⟹
ipcidr_union_set (set (the ((map_of ipassmt1) ifce))) =
ipcidr_union_set (set (the ((map_of ipassmt2) ifce)))"
apply(simp add: ipassmt_diff_def Let_def ipcidr_union_set_uncurry)
apply(simp add: Set.image_iff)
apply(elim conjE)
apply(drule cidr_empty)+
apply(simp)
apply(simp add: domIff)
apply(elim exE)
apply(simp add: wordinterval_Union wordinterval_to_set_ipcidr_tuple_to_wordinterval_uncurry)
done
qed
lemma ipcidr_union_cidr_split[simp]: "ipcidr_union_set (set (cidr_split a)) = wordinterval_to_set a"
by(simp add: ipcidr_union_set_uncurry cidr_split_prefix)
lemma
defines "assmt as ifce ≡ ipcidr_union_set (set (the ((map_of as ifce))))"
assumes diffs: "(ifce, d1, d2) ∈ set (ipassmt_diff ipassmt1 ipassmt2)"
and doms: "ifce ∈ dom (map_of ipassmt1)" "ifce ∈ dom (map_of ipassmt2)"
shows "ipcidr_union_set (set d1) = assmt ipassmt1 ifce - assmt ipassmt2 ifce"
"ipcidr_union_set (set d2) = assmt ipassmt2 ifce - assmt ipassmt1 ifce"
using assms by (clarsimp simp add: ipassmt_diff_def Let_def assmt_def wordinterval_Union; simp add: ipcidr_union_set_uncurry uncurry_def wordinterval_to_set_ipcidr_tuple_to_wordinterval_uncurry)+
text‹Explanation for interface @{term "Iface ''a''"}:
Left ipassmt: The IP range 4/30 contains the addresses 4,5,6,7
Diff: right ipassmt contains 6/32, so 4,5,7 is only in the left ipassmt.
IP addresses 4,5 correspond to subnet 4/30.›
lemma "ipassmt_diff (ipassmt_generic_ipv4 @ [(Iface ''a'', [(4,30)])])
(ipassmt_generic_ipv4 @ [(Iface ''a'', [(6,32), (0,30)]), (Iface ''b'', [(42,32)])]) =
[(Iface ''lo'', [], []),
(Iface ''a'', [(4, 31),(7, 32)],
[(0, 30)]
),
(Iface ''b'', [], [(42, 32)])]" by eval
end