Theory Common_Primitive_Matcher
theory Common_Primitive_Matcher
imports Common_Primitive_Matcher_Generic
begin
subsection‹Primitive Matchers: IP Port Iface Matcher›
fun common_matcher :: "('i::len common_primitive, ('i, 'a) tagged_packet_scheme) exact_match_tac" where
"common_matcher (IIface i) p = bool_to_ternary (match_iface i (p_iiface p))" |
"common_matcher (OIface i) p = bool_to_ternary (match_iface i (p_oiface p))" |
"common_matcher (Src ip) p = bool_to_ternary (p_src p ∈ ipt_iprange_to_set ip)" |
"common_matcher (Dst ip) p = bool_to_ternary (p_dst p ∈ ipt_iprange_to_set ip)" |
"common_matcher (Prot proto) p = bool_to_ternary (match_proto proto (p_proto p))" |
"common_matcher (Src_Ports (L4Ports proto ps)) p = bool_to_ternary (proto = p_proto p ∧ p_sport p ∈ ports_to_set ps)" |
"common_matcher (Dst_Ports (L4Ports proto ps)) p = bool_to_ternary (proto = p_proto p ∧ p_dport p ∈ ports_to_set ps)" |
"common_matcher (MultiportPorts (L4Ports proto ps)) p = bool_to_ternary (proto = p_proto p ∧ (p_sport p ∈ ports_to_set ps ∨ p_dport p ∈ ports_to_set ps))" |
"common_matcher (L4_Flags flags) p = bool_to_ternary (match_tcp_flags flags (p_tcp_flags p))" |
"common_matcher (CT_State S) p = bool_to_ternary (match_ctstate S (p_tag_ctstate p))" |
"common_matcher (Extra _) p = TernaryUnknown"
lemma packet_independent_β_unknown_common_matcher: "packet_independent_β_unknown common_matcher"
apply(simp add: packet_independent_β_unknown_def)
apply(clarify)
apply(rename_tac a p1 p2)
apply(case_tac a)
apply(simp_all add: bool_to_ternary_Unknown)
apply(rename_tac l4ports, case_tac l4ports; simp add: bool_to_ternary_Unknown; fail)+
done
lemma primitive_matcher_generic_common_matcher: "primitive_matcher_generic common_matcher"
by unfold_locales simp_all
text‹Warning: beware of the sloppy term `empty' portrange›
text‹An `empty' port range means it can never match! Basically, @{term "MatchNot (Match (Src_Ports (L4Ports proto [(0,65535)])))"} is False›
lemma "¬ matches (common_matcher, α) (MatchNot (Match (Src_Ports (L4Ports TCP [(0,65535)])))) a
⦇p_iiface = ''eth0'', p_oiface = ''eth1'',
p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (173,194,112,111),
p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {},
p_payload = '''', p_tag_ctstate = CT_New⦈"
by(simp add: primitive_matcher_generic_common_matcher primitive_matcher_generic.Ports_single_not)
text‹An `empty' port range means it always matches! Basically, @{term "(MatchNot (Match (Src_Ports (L4Ports any []))))"} is True.
This corresponds to firewall behavior, but usually you cannot specify an empty portrange in firewalls, but omission of portrange means no-port-restrictions,
i.e. every port matches.›
lemma "matches (common_matcher, α) (MatchNot (Match (Src_Ports (L4Ports any [])))) a
⦇p_iiface = ''eth0'', p_oiface = ''eth1'',
p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (173,194,112,111),
p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {},
p_payload = '''', p_tag_ctstate = CT_New⦈"
by(simp add: primitive_matcher_generic_common_matcher primitive_matcher_generic.Ports_single_not)
text‹If not a corner case, portrange matching is straight forward.›
lemma "matches (common_matcher, α) (Match (Src_Ports (L4Ports TCP [(1024,4096), (9999, 65535)]))) a
⦇p_iiface = ''eth0'', p_oiface = ''eth1'',
p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (173,194,112,111),
p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {},
p_payload = '''', p_tag_ctstate = CT_New⦈"
"¬ matches (common_matcher, α) (Match (Src_Ports (L4Ports TCP [(1024,4096), (9999, 65535)]))) a
⦇p_iiface = ''eth0'', p_oiface = ''eth1'',
p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (173,194,112,111),
p_proto=TCP, p_sport=5000, p_dport=80, p_tcp_flags = {},
p_payload = '''', p_tag_ctstate = CT_New⦈"
"¬matches (common_matcher, α) (MatchNot (Match (Src_Ports (L4Ports TCP [(1024,4096), (9999, 65535)])))) a
⦇p_iiface = ''eth0'', p_oiface = ''eth1'',
p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (173,194,112,111),
p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {},
p_payload = '''', p_tag_ctstate = CT_New⦈"
by(simp_all add: primitive_matcher_generic_common_matcher primitive_matcher_generic.Ports_single_not primitive_matcher_generic.Ports_single)
text‹Lemmas when matching on @{term Src} or @{term Dst}›
lemma common_matcher_SrcDst_defined:
"common_matcher (Src m) p ≠ TernaryUnknown"
"common_matcher (Dst m) p ≠ TernaryUnknown"
"common_matcher (Src_Ports ps) p ≠ TernaryUnknown"
"common_matcher (Dst_Ports ps) p ≠ TernaryUnknown"
"common_matcher (MultiportPorts ps) p ≠ TernaryUnknown"
apply(case_tac [!] m, case_tac [!] ps)
apply(simp_all add: bool_to_ternary_Unknown)
done
lemma common_matcher_SrcDst_defined_simp:
"common_matcher (Src x) p ≠ TernaryFalse ⟷ common_matcher (Src x) p = TernaryTrue"
"common_matcher (Dst x) p ≠ TernaryFalse ⟷ common_matcher (Dst x) p = TernaryTrue"
apply (metis eval_ternary_Not.cases common_matcher_SrcDst_defined(1) ternaryvalue.distinct(1))
apply (metis eval_ternary_Not.cases common_matcher_SrcDst_defined(2) ternaryvalue.distinct(1))
done
lemma match_simplematcher_SrcDst:
"matches (common_matcher, α) (Match (Src X)) a p ⟷ p_src p ∈ ipt_iprange_to_set X"
"matches (common_matcher, α) (Match (Dst X)) a p ⟷ p_dst p ∈ ipt_iprange_to_set X"
by(simp_all add: match_raw_ternary bool_to_ternary_simps split: ternaryvalue.split)
lemma match_simplematcher_SrcDst_not:
"matches (common_matcher, α) (MatchNot (Match (Src X))) a p ⟷ p_src p ∉ ipt_iprange_to_set X"
"matches (common_matcher, α) (MatchNot (Match (Dst X))) a p ⟷ p_dst p ∉ ipt_iprange_to_set X"
apply(simp_all add: matches_case_ternaryvalue_tuple split: ternaryvalue.split)
apply(case_tac [!] X)
apply(simp_all add: bool_to_ternary_simps)
done
lemma common_matcher_SrcDst_Inter:
"(∀m∈set X. matches (common_matcher, α) (Match (Src m)) a p) ⟷ p_src p ∈ (⋂x∈set X. ipt_iprange_to_set x)"
"(∀m∈set X. matches (common_matcher, α) (Match (Dst m)) a p) ⟷ p_dst p ∈ (⋂x∈set X. ipt_iprange_to_set x)"
by(simp_all add: match_raw_ternary bool_to_ternary_simps split: ternaryvalue.split)
subsection‹Basic optimisations›
text‹Perform very basic optimization. Remove matches to primitives which are essentially @{const MatchAny}›
fun optimize_primitive_univ :: "'i::len common_primitive match_expr ⇒ 'i common_primitive match_expr" where
"optimize_primitive_univ (Match (Src (IpAddrNetmask _ 0))) = MatchAny" |
"optimize_primitive_univ (Match (Dst (IpAddrNetmask _ 0))) = MatchAny" |
"optimize_primitive_univ (Match (IIface iface)) = (if iface = ifaceAny then MatchAny else (Match (IIface iface)))" |
"optimize_primitive_univ (Match (OIface iface)) = (if iface = ifaceAny then MatchAny else (Match (OIface iface)))" |
"optimize_primitive_univ (Match (Prot ProtoAny)) = MatchAny" |
"optimize_primitive_univ (Match (L4_Flags (TCP_Flags m c))) = (if m = {} ∧ c = {} then MatchAny else (Match (L4_Flags (TCP_Flags m c))))" |
"optimize_primitive_univ (Match (CT_State ctstate)) = (if ctstate_is_UNIV ctstate then MatchAny else Match (CT_State ctstate))" |
"optimize_primitive_univ (Match m) = Match m" |
"optimize_primitive_univ (MatchNot m) = (MatchNot (optimize_primitive_univ m))" |
"optimize_primitive_univ (MatchAnd m1 m2) = MatchAnd (optimize_primitive_univ m1) (optimize_primitive_univ m2)" |
"optimize_primitive_univ MatchAny = MatchAny"
lemma optimize_primitive_univ_unchanged_primitives:
"optimize_primitive_univ (Match a) = (Match a) ∨ optimize_primitive_univ (Match a) = MatchAny"
by (induction "(Match a)" rule: optimize_primitive_univ.induct)
(auto split: if_split_asm)
lemma optimize_primitive_univ_correct_matchexpr: fixes m::"'i::len common_primitive match_expr"
shows "matches (common_matcher, α) m = matches (common_matcher, α) (optimize_primitive_univ m)"
proof(simp add: fun_eq_iff, clarify, rename_tac a p)
fix a and p :: "('i::len, 'a) tagged_packet_scheme"
have "65535 = (-1::16 word)" by simp
then have port_range: "⋀s e port. s = 0 ∧ e = 0xFFFF ⟶ (port::16 word) ≤ 0xFFFF"
by (simp only:) simp
have "ternary_ternary_eval (map_match_tac common_matcher p m) = ternary_ternary_eval (map_match_tac common_matcher p (optimize_primitive_univ m))"
apply(induction m rule: optimize_primitive_univ.induct)
by(simp_all add: port_range match_ifaceAny ipset_from_cidr_0 ctstate_is_UNIV)
thus "matches (common_matcher, α) m a p = matches (common_matcher, α) (optimize_primitive_univ m) a p"
by(rule matches_iff_apply_f)
qed
corollary optimize_primitive_univ_correct: "approximating_bigstep_fun (common_matcher, α) p (optimize_matches optimize_primitive_univ rs) s =
approximating_bigstep_fun (common_matcher, α) p rs s"
using optimize_matches optimize_primitive_univ_correct_matchexpr by metis
subsection‹Abstracting over unknowns›
text‹remove @{const Extra} (i.e. @{const TernaryUnknown}) match expressions›