Theory Interface_Replace
theory Interface_Replace
imports
No_Spoof
Common_Primitive_toString
Output_Interface_Replace
begin
section‹Trying to connect inbound interfaces by their IP ranges›
subsection‹Constraining Interfaces›
text‹We keep the match on the interface but add the corresponding IP address range.›
definition ipassmt_iface_constrain_srcip_mexpr
:: "'i::len ipassignment ⇒ iface ⇒ 'i common_primitive match_expr"
where
"ipassmt_iface_constrain_srcip_mexpr ipassmt ifce = (case ipassmt ifce of
None ⇒ Match (IIface ifce)
| Some ips ⇒ MatchAnd
(Match (IIface ifce))
(match_list_to_match_expr (map (Match ∘ Src) (map (uncurry IpAddrNetmask) ips)))
)"
lemma matches_ipassmt_iface_constrain_srcip_mexpr:
"matches (common_matcher, α) (ipassmt_iface_constrain_srcip_mexpr ipassmt ifce) a p ⟷
(case ipassmt ifce of
None ⇒ match_iface ifce (p_iiface p)
| Some ips ⇒ match_iface ifce (p_iiface p) ∧ p_src p ∈ ipcidr_union_set (set ips)
)"
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: ipassmt_iface_constrain_srcip_mexpr_def primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher]; fail)
next
case (Some ips)
have "matches (common_matcher, α) (match_list_to_match_expr (map (Match ∘ Src ∘ (uncurry IpAddrNetmask)) ips)) a p ⟷
(∃m∈set ips. p_src p ∈ uncurry ipset_from_cidr m)"
apply(simp add: match_list_to_match_expr_disjunction[symmetric]
match_list_matches match_simplematcher_SrcDst)
by(simp add: ipt_iprange_to_set_uncurry_IpAddrNetmask)
with Some show ?thesis
apply(simp add: ipcidr_union_set_uncurry)
apply(simp add: ipassmt_iface_constrain_srcip_mexpr_def bunch_of_lemmata_about_matches)
apply(simp add: primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
done
qed
fun iiface_constrain :: "'i::len ipassignment ⇒ 'i common_primitive match_expr ⇒ 'i common_primitive match_expr" where
"iiface_constrain _ MatchAny = MatchAny" |
"iiface_constrain ipassmt (Match (IIface ifce)) = ipassmt_iface_constrain_srcip_mexpr ipassmt ifce" |
"iiface_constrain ipassmt (Match a) = Match a" |
"iiface_constrain ipassmt (MatchNot m) = MatchNot (iiface_constrain ipassmt m)" |
"iiface_constrain ipassmt (MatchAnd m1 m2) = MatchAnd (iiface_constrain ipassmt m1) (iiface_constrain ipassmt m2)"
context
begin
private lemma iiface_constrain_matches_Primitive:
"matches (common_matcher, α) (MatchNot (iiface_constrain ipassmt (Match x))) a p = matches (common_matcher, α) (MatchNot (Match x)) a p ⟷
matches (common_matcher, α) (iiface_constrain ipassmt (Match x)) a p = matches (common_matcher, α) (Match x) a p"
proof(cases x)
case (IIface ifce)
have "(matches (common_matcher, α) (MatchNot (ipassmt_iface_constrain_srcip_mexpr ipassmt ifce)) a p = (¬ match_iface ifce (p_iiface p))) ⟷
(matches (common_matcher, α) (ipassmt_iface_constrain_srcip_mexpr ipassmt ifce) a p = match_iface ifce (p_iiface p))"
proof(cases "ipassmt ifce")
case None thus ?thesis
apply(simp add: matches_ipassmt_iface_constrain_srcip_mexpr)
apply(simp add: ipassmt_iface_constrain_srcip_mexpr_def
primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
done
next
case (Some ips)
{ fix ips
have "matches (common_matcher, α)
(MatchNot (match_list_to_match_expr (map (Match ∘ Src ∘ (uncurry IpAddrNetmask)) ips))) a p ⟷
(p_src p ∉ ipcidr_union_set (set ips))"
apply(induction ips)
apply(simp add: bunch_of_lemmata_about_matches ipcidr_union_set_uncurry; fail)
apply(simp add: MatchOr_MatchNot)
apply(simp add: ipcidr_union_set_uncurry)
apply(simp add: match_simplematcher_SrcDst_not)
apply(thin_tac _)
by (simp add: ipt_iprange_to_set_uncurry_IpAddrNetmask)
} note helper=this
from Some show ?thesis
apply(simp add: matches_ipassmt_iface_constrain_srcip_mexpr)
apply(simp add: ipassmt_iface_constrain_srcip_mexpr_def primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
apply(simp add: matches_DeMorgan)
apply(simp add: helper)
apply(simp add: primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
by blast
qed
with IIface show ?thesis
by(simp add: primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
qed(simp_all)
private lemma matches_ipassmt_iface_constrain_srcip_mexpr_case_Iface:
fixes ifce::iface
assumes "ipassmt_sanity_nowildcards ipassmt"
and "⋀ips. ipassmt (Iface (p_iiface p)) = Some ips ⟹ p_src p ∈ ipcidr_union_set (set ips)"
shows "matches (common_matcher, α) (ipassmt_iface_constrain_srcip_mexpr ipassmt ifce) a p ⟷
matches (common_matcher, α) (Match (IIface ifce)) a p"
proof -
have "matches (common_matcher, α) (ipassmt_iface_constrain_srcip_mexpr ipassmt ifce) a p = match_iface ifce (p_iiface p)"
proof(cases "ipassmt (Iface (p_iiface p))")
case None
from None show ?thesis
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: matches_ipassmt_iface_constrain_srcip_mexpr)
next
case (Some a)
from assms(1) have "¬ match_iface ifce (p_iiface p)"
apply(rule ipassmt_sanity_nowildcards_match_iface)
by(simp_all add: Some None)
with Some show ?thesis by(simp add: matches_ipassmt_iface_constrain_srcip_mexpr)
qed
next
case (Some x)
with assms(2) have assms2: "p_src p ∈ ipcidr_union_set (set x)" by(simp)
show ?thesis
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: matches_ipassmt_iface_constrain_srcip_mexpr)
next
case (Some y) with assms(2) have "(match_iface ifce (p_iiface p) ∧ p_src p ∈ ipcidr_union_set (set y)) = match_iface ifce (p_iiface p)"
apply(cases ifce)
apply(rename_tac ifce_str)
apply(case_tac "ifce_str = (p_iiface p)")
apply (simp add: match_iface_refl; fail)
apply(simp)
apply(subgoal_tac "¬ match_iface (Iface ifce_str) (p_iiface p)")
apply(simp)
using assms(1) by (metis domI iface.sel iface_is_wildcard_def ipassmt_sanity_nowildcards_def match_iface_case_nowildcard)
with Some show ?thesis by(simp add: matches_ipassmt_iface_constrain_srcip_mexpr)
qed
qed
thus ?thesis by(simp add: primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
qed
lemma matches_iiface_constrain:
"normalized_nnf_match m ⟹ ipassmt_sanity_nowildcards ipassmt ⟹
(⋀ips. ipassmt (Iface (p_iiface p)) = Some ips ⟹ p_src p ∈ ipcidr_union_set (set ips)) ⟹
matches (common_matcher, α) (iiface_constrain ipassmt m) a p ⟷ matches (common_matcher, α) m a p"
proof(induction m)
case MatchAny thus ?case by simp
next
case (MatchNot m)
hence IH: "normalized_nnf_match m ⟹ matches (common_matcher, α) (iiface_constrain ipassmt m) a p = matches (common_matcher, α) m a p" by blast
with MatchNot.prems IH show ?case by(induction m) (simp_all add: iiface_constrain_matches_Primitive)
next
case(Match x) thus ?case
proof(cases x)
case (IIface ifce) with Match show ?thesis
using matches_ipassmt_iface_constrain_srcip_mexpr_case_Iface by fastforce
qed(simp_all)
next
case (MatchAnd m1 m2) thus ?case by(simp add: bunch_of_lemmata_about_matches)
qed
end
subsection‹Sanity checking the assumption›
lemma "(∃ips. ipassmt (Iface (p_iiface p)) = Some ips ∧ p_src p ∈ ipcidr_union_set (set ips)) ⟹
(case ipassmt (Iface (p_iiface p)) of Some ips ⇒ p_src p ∈ ipcidr_union_set (set ips))"
"(case ipassmt (Iface (p_iiface p)) of Some ips ⇒ p_src p ∈ ipcidr_union_set (set ips)) ⟹
(⋀ips. ipassmt (Iface (p_iiface p)) = Some ips ⟹ p_src p ∈ ipcidr_union_set (set ips))"
by(cases "ipassmt (Iface (p_iiface p))",simp_all)+
text‹Sanity check:
If we assume that there are no spoofed packets, spoofing protection is trivially fulfilled.›
lemma "∀ p:: ('i::len,'pkt_ext) tagged_packet_scheme.
Iface (p_iiface p) ∈ dom ipassmt ⟶ p_src p ∈ ipcidr_union_set (set (the (ipassmt (Iface (p_iiface p))))) ⟹
no_spoofing TYPE('pkt_ext) ipassmt rs"
apply(simp add: no_spoofing_def)
apply(clarify)
apply(rename_tac iface ips p)
apply(thin_tac "_,_⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow")
apply(erule_tac x="p⦇p_iiface := iface_sel iface⦈" in allE)
apply(auto)
done
text‹Sanity check:
If the firewall features spoofing protection and we look at a packet which was allowed by the firewall.
Then the packet's src ip must be according to ipassmt. (case Some)
We don't case about packets from an interface which are not defined in ipassmt. (case None)›
lemma
fixes p :: "('i::len,'pkt_ext) tagged_packet_scheme"
shows "no_spoofing TYPE('pkt_ext) ipassmt rs ⟹
(common_matcher, in_doubt_allow),p⊢ ⟨rs, Undecided⟩ ⇒⇩α Decision FinalAllow ⟹
case ipassmt (Iface (p_iiface p)) of Some ips ⇒ p_src p ∈ ipcidr_union_set (set ips) | None ⇒ True"
apply(simp add: no_spoofing_def)
apply(case_tac "Iface (p_iiface p) ∈ dom ipassmt")
apply(erule_tac x="Iface (p_iiface p)" in ballE)
apply(simp_all)
apply(erule_tac x="p" in allE)
apply(simp)
apply fastforce
by (simp add: domIff)
subsection‹Replacing Interfaces Completely›
text‹This is a stricter, true rewriting since it removes the interface match completely.
However, it requires @{const ipassmt_sanity_disjoint}›
thm ipassmt_sanity_disjoint_def
definition ipassmt_iface_replace_srcip_mexpr
:: "'i::len ipassignment ⇒ iface ⇒ 'i common_primitive match_expr" where
"ipassmt_iface_replace_srcip_mexpr ipassmt ifce ≡ case ipassmt ifce of
None ⇒ Match (IIface ifce)
| Some ips ⇒ (match_list_to_match_expr (map (Match ∘ Src) (map (uncurry IpAddrNetmask) ips)))"
lemma matches_ipassmt_iface_replace_srcip_mexpr:
"matches (common_matcher, α) (ipassmt_iface_replace_srcip_mexpr ipassmt ifce) a p ⟷ (case ipassmt ifce of
None ⇒ match_iface ifce (p_iiface p)
| Some ips ⇒ p_src p ∈ ipcidr_union_set (set ips)
)"
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: ipassmt_iface_replace_srcip_mexpr_def primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
next
case (Some ips)
have "matches (common_matcher, α) (match_list_to_match_expr (map (Match ∘ Src ∘ (uncurry IpAddrNetmask)) ips)) a p ⟷
(∃m∈set ips. p_src p ∈ (uncurry ipset_from_cidr m))"
by(simp add: match_list_to_match_expr_disjunction[symmetric]
match_list_matches match_simplematcher_SrcDst ipt_iprange_to_set_uncurry_IpAddrNetmask)
with Some show ?thesis
apply(simp add: ipassmt_iface_replace_srcip_mexpr_def bunch_of_lemmata_about_matches)
apply(simp add: ipcidr_union_set_uncurry)
done
qed
fun iiface_rewrite
:: "'i::len ipassignment ⇒ 'i common_primitive match_expr ⇒ 'i common_primitive match_expr"
where
"iiface_rewrite _ MatchAny = MatchAny" |
"iiface_rewrite ipassmt (Match (IIface ifce)) = ipassmt_iface_replace_srcip_mexpr ipassmt ifce" |
"iiface_rewrite ipassmt (Match a) = Match a" |
"iiface_rewrite ipassmt (MatchNot m) = MatchNot (iiface_rewrite ipassmt m)" |
"iiface_rewrite ipassmt (MatchAnd m1 m2) = MatchAnd (iiface_rewrite ipassmt m1) (iiface_rewrite ipassmt m2)"
context
begin
private lemma iiface_rewrite_matches_Primitive:
"matches (common_matcher, α) (MatchNot (iiface_rewrite ipassmt (Match x))) a p = matches (common_matcher, α) (MatchNot (Match x)) a p ⟷
matches (common_matcher, α) (iiface_rewrite ipassmt (Match x)) a p = matches (common_matcher, α) (Match x) a p"
proof(cases x)
case (IIface ifce)
have "(matches (common_matcher, α) (MatchNot (ipassmt_iface_replace_srcip_mexpr ipassmt ifce)) a p = (¬ match_iface ifce (p_iiface p))) ⟷
(matches (common_matcher, α) (ipassmt_iface_replace_srcip_mexpr ipassmt ifce) a p = match_iface ifce (p_iiface p))"
proof(cases "ipassmt ifce")
case None thus ?thesis
apply(simp add: matches_ipassmt_iface_replace_srcip_mexpr)
apply(simp add: ipassmt_iface_replace_srcip_mexpr_def primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher])
done
next
case (Some ips)
{ fix ips
have "matches (common_matcher, α)
(MatchNot (match_list_to_match_expr (map (Match ∘ Src ∘ (uncurry IpAddrNetmask)) ips))) a p ⟷
(p_src p ∉ ipcidr_union_set (set ips))"
apply(induction ips)
apply(simp add: bunch_of_lemmata_about_matches ipcidr_union_set_uncurry)
apply(simp add: MatchOr_MatchNot)
apply(simp add: ipcidr_union_set_uncurry)
apply(simp add: match_simplematcher_SrcDst_not)
apply(thin_tac _)
apply(simp add: ipt_iprange_to_set_uncurry_IpAddrNetmask)
done
} note helper=this
from Some show ?thesis
apply(simp add: matches_ipassmt_iface_replace_srcip_mexpr)
apply(simp add: ipassmt_iface_replace_srcip_mexpr_def)
apply(simp add: helper)
done
qed
with IIface show ?thesis
by(simp add: primitive_matcher_generic.Iface_single_not[OF primitive_matcher_generic_common_matcher]
primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
qed(simp_all)
private lemma matches_ipassmt_iface_replace_srcip_mexpr_case_Iface:
fixes ifce::iface
assumes "ipassmt_sanity_nowildcards ipassmt"
and "ipassmt_sanity_disjoint ipassmt"
and "ipassmt (Iface (p_iiface p)) = Some p_ips ∧ p_src p ∈ ipcidr_union_set (set p_ips)"
shows "matches (common_matcher, α) (ipassmt_iface_replace_srcip_mexpr ipassmt ifce) a p ⟷
matches (common_matcher, α) (Match (IIface ifce)) a p"
proof -
have "matches (common_matcher, α) (ipassmt_iface_replace_srcip_mexpr ipassmt ifce) a p = match_iface ifce (p_iiface p)"
proof -
show ?thesis
proof(cases "ipassmt ifce")
case None thus ?thesis by(simp add: matches_ipassmt_iface_replace_srcip_mexpr)
next
case (Some y) with assms(2) have "p_src p ∈ ipcidr_union_set (set y) = match_iface ifce (p_iiface p)"
using assms(1) assms(3) ipassmt_disjoint_matcheq_iifce_srcip by blast
with Some show ?thesis by(simp add: matches_ipassmt_iface_replace_srcip_mexpr)
qed
qed
thus ?thesis by(simp add: primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher])
qed
lemma matches_iiface_rewrite:
"normalized_nnf_match m ⟹ ipassmt_sanity_nowildcards ipassmt ⟹ ipassmt_sanity_disjoint ipassmt ⟹
(∃p_ips. ipassmt (Iface (p_iiface p)) = Some p_ips ∧ p_src p ∈ ipcidr_union_set (set p_ips)) ⟹
matches (common_matcher, α) (iiface_rewrite ipassmt m) a p ⟷ matches (common_matcher, α) m a p"
proof(induction m)
case MatchAny thus ?case by simp
next
case (MatchNot m)
hence IH: "normalized_nnf_match m ⟹
matches (common_matcher, α) (iiface_rewrite ipassmt m) a p =matches (common_matcher, α) m a p" by blast
with MatchNot.prems IH show ?case by(induction m) (simp_all add: iiface_rewrite_matches_Primitive)
next
case(Match x) thus ?case
proof(cases x)
case (IIface ifce) with Match show ?thesis
apply(cases "ipassmt (Iface (p_iiface p))")
prefer 2
apply(simp add: matches_ipassmt_iface_replace_srcip_mexpr_case_Iface; fail)
by auto
qed(simp_all)
next
case (MatchAnd m1 m2) thus ?case by(simp add: bunch_of_lemmata_about_matches)
qed
end
text‹Finally, we show that @{const ipassmt_sanity_disjoint} is really needed.›
lemma iface_replace_needs_ipassmt_disjoint:
assumes "ipassmt_sanity_nowildcards ipassmt"
and iface_replace: "⋀ ifce p:: 'i::len tagged_packet.
(matches (common_matcher, α) (ipassmt_iface_replace_srcip_mexpr ipassmt ifce) a p ⟷ matches (common_matcher, α) (Match (IIface ifce)) a p)"
shows "ipassmt_sanity_disjoint ipassmt"
unfolding ipassmt_sanity_disjoint_def
proof(intro ballI impI)
fix i1 i2
assume "i1 ∈ dom ipassmt" and "i2 ∈ dom ipassmt" and "i1 ≠ i2"
from ‹i1 ∈ dom ipassmt› obtain i1_ips where i1_ips: "ipassmt i1 = Some i1_ips" by blast
from ‹i2 ∈ dom ipassmt› obtain i2_ips where i2_ips: "ipassmt i2 = Some i2_ips" by blast
{ fix p :: "'i tagged_packet"
from iface_replace[of i1 "p⦇ p_iiface := iface_sel i2⦈"] have
"(p_src p ∈ ipcidr_union_set (set i2_ips) ⟹ (p_src p ∈ ipcidr_union_set (set i1_ips)) = match_iface i1 (iface_sel i2))"
apply(simp add: primitive_matcher_generic.Iface_single[OF primitive_matcher_generic_common_matcher] ‹i1 ∈ dom ipassmt›)
apply(simp add: matches_ipassmt_iface_replace_srcip_mexpr i1_ips)
done
with ‹i1 ≠ i2› have "¬ (p_src p ∈ ipcidr_union_set (set i2_ips) ∧ (p_src p ∈ ipcidr_union_set (set i1_ips)))"
by (metis ‹i1 ∈ dom ipassmt› assms(1) iface.exhaust_sel iface_is_wildcard_def ipassmt_sanity_nowildcards_def match_iface_case_nowildcard)
}
hence "¬ (src ∈ ipcidr_union_set (set i2_ips) ∧ (src ∈ ipcidr_union_set (set i1_ips)))"
for src
apply(simp)
by (metis simple_packet.select_convs(3))
thus "ipcidr_union_set (set (the (ipassmt i1))) ∩ ipcidr_union_set (set (the (ipassmt i2))) = {}"
apply(simp add: i1_ips i2_ips)
by blast
qed
end