Theory SimpleFw_Semantics
section‹Simple Firewall Semantics›
theory SimpleFw_Semantics
imports SimpleFw_Syntax
IP_Addresses.IP_Address
IP_Addresses.Prefix_Match
begin
fun simple_match_ip :: "('i::len word × nat) ⇒ 'i::len word ⇒ bool" where
"simple_match_ip (base, len) p_ip ⟷ p_ip ∈ ipset_from_cidr base len"
lemma wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set:
"wordinterval_to_set (ipcidr_tuple_to_wordinterval ip) = {d. simple_match_ip ip d}"
proof -
{ fix s and d :: "'a::len word × nat"
from wordinterval_to_set_ipcidr_tuple_to_wordinterval have
"s ∈ wordinterval_to_set (ipcidr_tuple_to_wordinterval d) ⟷ simple_match_ip d s"
by(cases d) auto
} thus ?thesis by blast
qed
lemma "{(253::8 word) .. 8} = {}" by simp
fun simple_match_port :: "(16 word × 16 word) ⇒ 16 word ⇒ bool" where
"simple_match_port (s,e) p_p ⟷ p_p ∈ {s..e}"
fun simple_matches :: "'i::len simple_match ⇒ ('i, 'a) simple_packet_scheme ⇒ bool" where
"simple_matches m p ⟷
(match_iface (iiface m) (p_iiface p)) ∧
(match_iface (oiface m) (p_oiface p)) ∧
(simple_match_ip (src m) (p_src p)) ∧
(simple_match_ip (dst m) (p_dst p)) ∧
(match_proto (proto m) (p_proto p)) ∧
(simple_match_port (sports m) (p_sport p)) ∧
(simple_match_port (dports m) (p_dport p))"
text‹The semantics of a simple firewall: just iterate over the rules sequentially›
fun simple_fw :: "'i::len simple_rule list ⇒ ('i, 'a) simple_packet_scheme ⇒ state" where
"simple_fw [] _ = Undecided" |
"simple_fw ((SimpleRule m Accept)#rs) p = (if simple_matches m p then Decision FinalAllow else simple_fw rs p)" |
"simple_fw ((SimpleRule m Drop)#rs) p = (if simple_matches m p then Decision FinalDeny else simple_fw rs p)"
fun simple_fw_alt where
"simple_fw_alt [] _ = Undecided" |
"simple_fw_alt (r#rs) p = (if simple_matches (match_sel r) p then
(case action_sel r of Accept ⇒ Decision FinalAllow | Drop ⇒ Decision FinalDeny) else simple_fw_alt rs p)"
lemma simple_fw_alt: "simple_fw r p = simple_fw_alt r p" by(induction rule: simple_fw.induct) simp_all
definition simple_match_any :: "'i::len simple_match" where
"simple_match_any ≡ ⦇iiface=ifaceAny, oiface=ifaceAny, src=(0,0), dst=(0,0), proto=ProtoAny, sports=(0,65535), dports=(0,65535) ⦈"
lemma simple_match_any: "simple_matches simple_match_any p"
proof -
have *: "(65535::16 word) = - 1"
by simp
show ?thesis
by (simp add: simple_match_any_def ipset_from_cidr_0 match_ifaceAny *)
qed
text‹we specify only one empty port range›
definition simple_match_none :: "'i::len simple_match" where
"simple_match_none ≡
⦇iiface=ifaceAny, oiface=ifaceAny, src=(1,0), dst=(0,0),
proto=ProtoAny, sports=(1,0), dports=(0,65535) ⦈"
lemma simple_match_none: "¬ simple_matches simple_match_none p"
proof -
show ?thesis by(simp add: simple_match_none_def)
qed
fun empty_match :: "'i::len simple_match ⇒ bool" where
"empty_match ⦇iiface=_, oiface=_, src=_, dst=_, proto=_,
sports=(sps1, sps2), dports=(dps1, dps2) ⦈ ⟷ (sps1 > sps2) ∨ (dps1 > dps2)"
lemma empty_match: "empty_match m ⟷ (∀(p::('i::len, 'a) simple_packet_scheme). ¬ simple_matches m p)"
proof
assume "empty_match m"
thus "∀p. ¬ simple_matches m p" by(cases m) fastforce
next
assume assm: "∀(p::('i::len, 'a) simple_packet_scheme). ¬ simple_matches m p"
obtain iif oif sip dip protocol sps1 sps2 dps1 dps2 where m:
"m = ⦇iiface = iif, oiface = oif, src = sip, dst = dip, proto = protocol, sports = (sps1, sps2), dports = (dps1, dps2)⦈"
by(cases m) force
show "empty_match m"
proof(simp add: m)
let ?x="λp. dps1 ≤ p_dport p ⟶ p_sport p ≤ sps2 ⟶ sps1 ≤ p_sport p ⟶
match_proto protocol (p_proto p) ⟶ simple_match_ip dip (p_dst p) ⟶ simple_match_ip sip (p_src p) ⟶
match_iface oif (p_oiface p) ⟶ match_iface iif (p_iiface p) ⟶ ¬ p_dport p ≤ dps2"
from assm have nomatch: "∀(p::('i::len, 'a) simple_packet_scheme). ?x p" by(simp add: m)
{ fix ips::"'i::len word × nat"
have "a ∈ ipset_from_cidr a n" for a::"'i::len word" and n
using ipset_from_cidr_lowest by auto
hence "simple_match_ip ips (fst ips)" by(cases ips) simp
} note ips=this
have proto: "match_proto protocol (case protocol of ProtoAny ⇒ TCP | Proto p ⇒ p)"
by(simp split: protocol.split)
{ fix ifce
have "match_iface ifce (iface_sel ifce)"
by (simp add: match_iface_eqI)
} note ifaces=this
{ fix p::"('i, 'a) simple_packet_scheme"
from nomatch have "?x p" by blast
} note pkt1=this
obtain p::"('i, 'a) simple_packet_scheme" where [simp]:
"p_iiface p = iface_sel iif"
"p_oiface p = iface_sel oif"
"p_src p = fst sip"
"p_dst p = fst dip"
"p_proto p = (case protocol of ProtoAny ⇒ TCP | Proto p ⇒ p)"
"p_sport p = sps1"
"p_dport p = dps1"
by (meson simple_packet.select_convs)
note pkt=pkt1[of p, simplified]
from pkt ips proto ifaces have " sps1 ≤ sps2 ⟶ ¬ dps1 ≤ dps2" by blast
thus "sps2 < sps1 ∨ dps2 < dps1" by fastforce
qed
qed
lemma nomatch: "¬ simple_matches m p ⟹ simple_fw (SimpleRule m a # rs) p = simple_fw rs p"
by(cases a, simp_all del: simple_matches.simps)
subsection‹Simple Ports›
fun simpl_ports_conjunct :: "(16 word × 16 word) ⇒ (16 word × 16 word) ⇒ (16 word × 16 word)" where
"simpl_ports_conjunct (p1s, p1e) (p2s, p2e) = (max p1s p2s, min p1e p2e)"
lemma "{(p1s:: 16 word) .. p1e} ∩ {p2s .. p2e} = {max p1s p2s .. min p1e p2e}" by(simp)
lemma simple_ports_conjunct_correct:
"simple_match_port p1 pkt ∧ simple_match_port p2 pkt ⟷ simple_match_port (simpl_ports_conjunct p1 p2) pkt"
apply(cases p1, cases p2, simp)
by blast
lemma simple_match_port_code[code] :"simple_match_port (s,e) p_p = (s ≤ p_p ∧ p_p ≤ e)" by simp
lemma simple_match_port_UNIV: "{p. simple_match_port (s,e) p} = UNIV ⟷ (s = 0 ∧ e = - 1)"
apply(simp)
apply(rule)
apply(case_tac "s = 0")
using antisym_conv apply blast
using word_le_0_iff apply blast
using word_zero_le by blast
subsection‹Simple IPs›
lemma simple_match_ip_conjunct:
fixes ip1 :: "'i::len word × nat"
shows "simple_match_ip ip1 p_ip ∧ simple_match_ip ip2 p_ip ⟷
(case ipcidr_conjunct ip1 ip2 of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)"
proof -
{
fix b1 m1 b2 m2
have "simple_match_ip (b1, m1) p_ip ∧ simple_match_ip (b2, m2) p_ip ⟷
p_ip ∈ ipset_from_cidr b1 m1 ∩ ipset_from_cidr b2 m2"
by simp
also have "… ⟷ p_ip ∈ (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ {} | Some (bx, mx) ⇒ ipset_from_cidr bx mx)"
using ipcidr_conjunct_correct by blast
also have "… ⟷ (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)"
by(simp split: option.split)
finally have "simple_match_ip (b1, m1) p_ip ∧ simple_match_ip (b2, m2) p_ip ⟷
(case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)" .
} thus ?thesis by(cases ip1, cases ip2, simp)
qed
declare simple_matches.simps[simp del]
subsection‹Merging Simple Matches›
text‹@{typ "'i::len simple_match"} ‹∧› @{typ "'i::len simple_match"}›
fun simple_match_and :: "'i::len simple_match ⇒ 'i simple_match ⇒ 'i simple_match option" where
"simple_match_and ⦇iiface=iif1, oiface=oif1, src=sip1, dst=dip1, proto=p1, sports=sps1, dports=dps1 ⦈
⦇iiface=iif2, oiface=oif2, src=sip2, dst=dip2, proto=p2, sports=sps2, dports=dps2 ⦈ =
(case ipcidr_conjunct sip1 sip2 of None ⇒ None | Some sip ⇒
(case ipcidr_conjunct dip1 dip2 of None ⇒ None | Some dip ⇒
(case iface_conjunct iif1 iif2 of None ⇒ None | Some iif ⇒
(case iface_conjunct oif1 oif2 of None ⇒ None | Some oif ⇒
(case simple_proto_conjunct p1 p2 of None ⇒ None | Some p ⇒
Some ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p,
sports=simpl_ports_conjunct sps1 sps2, dports=simpl_ports_conjunct dps1 dps2 ⦈)))))"
lemma simple_match_and_correct: "simple_matches m1 p ∧ simple_matches m2 p ⟷
(case simple_match_and m1 m2 of None ⇒ False | Some m ⇒ simple_matches m p)"
proof -
obtain iif1 oif1 sip1 dip1 p1 sps1 dps1 where m1:
"m1 = ⦇iiface=iif1, oiface=oif1, src=sip1, dst=dip1, proto=p1, sports=sps1, dports=dps1 ⦈" by(cases m1, blast)
obtain iif2 oif2 sip2 dip2 p2 sps2 dps2 where m2:
"m2 = ⦇iiface=iif2, oiface=oif2, src=sip2, dst=dip2, proto=p2, sports=sps2, dports=dps2 ⦈" by(cases m2, blast)
have sip_None: "ipcidr_conjunct sip1 sip2 = None ⟹ ¬ simple_match_ip sip1 (p_src p) ∨ ¬ simple_match_ip sip2 (p_src p)"
using simple_match_ip_conjunct[of sip1 "p_src p" sip2] by simp
have dip_None: "ipcidr_conjunct dip1 dip2 = None ⟹ ¬ simple_match_ip dip1 (p_dst p) ∨ ¬ simple_match_ip dip2 (p_dst p)"
using simple_match_ip_conjunct[of dip1 "p_dst p" dip2] by simp
have sip_Some: "⋀ip. ipcidr_conjunct sip1 sip2 = Some ip ⟹
simple_match_ip ip (p_src p) ⟷ simple_match_ip sip1 (p_src p) ∧ simple_match_ip sip2 (p_src p)"
using simple_match_ip_conjunct[of sip1 "p_src p" sip2] by simp
have dip_Some: "⋀ip. ipcidr_conjunct dip1 dip2 = Some ip ⟹
simple_match_ip ip (p_dst p) ⟷ simple_match_ip dip1 (p_dst p) ∧ simple_match_ip dip2 (p_dst p)"
using simple_match_ip_conjunct[of dip1 "p_dst p" dip2] by simp
have iiface_None: "iface_conjunct iif1 iif2 = None ⟹ ¬ match_iface iif1 (p_iiface p) ∨ ¬ match_iface iif2 (p_iiface p)"
using iface_conjunct[of iif1 "(p_iiface p)" iif2] by simp
have oiface_None: "iface_conjunct oif1 oif2 = None ⟹ ¬ match_iface oif1 (p_oiface p) ∨ ¬ match_iface oif2 (p_oiface p)"
using iface_conjunct[of oif1 "(p_oiface p)" oif2] by simp
have iiface_Some: "⋀iface. iface_conjunct iif1 iif2 = Some iface ⟹
match_iface iface (p_iiface p) ⟷ match_iface iif1 (p_iiface p) ∧ match_iface iif2 (p_iiface p)"
using iface_conjunct[of iif1 "(p_iiface p)" iif2] by simp
have oiface_Some: "⋀iface. iface_conjunct oif1 oif2 = Some iface ⟹
match_iface iface (p_oiface p) ⟷ match_iface oif1 (p_oiface p) ∧ match_iface oif2 (p_oiface p)"
using iface_conjunct[of oif1 "(p_oiface p)" oif2] by simp
have proto_None: "simple_proto_conjunct p1 p2 = None ⟹ ¬ match_proto p1 (p_proto p) ∨ ¬ match_proto p2 (p_proto p)"
using simple_proto_conjunct_correct[of p1 "(p_proto p)" p2] by simp
have proto_Some: "⋀proto. simple_proto_conjunct p1 p2 = Some proto ⟹
match_proto proto (p_proto p) ⟷ match_proto p1 (p_proto p) ∧ match_proto p2 (p_proto p)"
using simple_proto_conjunct_correct[of p1 "(p_proto p)" p2] by simp
have case_Some: "⋀m. Some m = simple_match_and m1 m2 ⟹
(simple_matches m1 p ∧ simple_matches m2 p) ⟷ simple_matches m p"
apply(simp add: m1 m2 simple_matches.simps split: option.split_asm)
using simple_ports_conjunct_correct by(blast dest: sip_Some dip_Some iiface_Some oiface_Some proto_Some)
have case_None: "simple_match_and m1 m2 = None ⟹ ¬ (simple_matches m1 p ∧ simple_matches m2 p)"
apply(simp add: m1 m2 simple_matches.simps split: option.split_asm)
apply(blast dest: sip_None dip_None iiface_None oiface_None proto_None)+
done
from case_Some case_None show ?thesis by(cases "simple_match_and m1 m2") simp_all
qed
lemma simple_match_and_SomeD: "simple_match_and m1 m2 = Some m ⟹
simple_matches m p ⟷ (simple_matches m1 p ∧ simple_matches m2 p)"
by(simp add: simple_match_and_correct)
lemma simple_match_and_NoneD: "simple_match_and m1 m2 = None ⟹
¬(simple_matches m1 p ∧ simple_matches m2 p)"
by(simp add: simple_match_and_correct)
lemma simple_matches_andD: "simple_matches m1 p ⟹ simple_matches m2 p ⟹
∃m. simple_match_and m1 m2 = Some m ∧ simple_matches m p"
by (meson option.exhaust_sel simple_match_and_NoneD simple_match_and_SomeD)
subsection‹Further Properties of a Simple Firewall›
fun has_default_policy :: "'i::len simple_rule list ⇒ bool" where
"has_default_policy [] = False" |
"has_default_policy [(SimpleRule m _)] = (m = simple_match_any)" |
"has_default_policy (_#rs) = has_default_policy rs"
lemma has_default_policy: "has_default_policy rs ⟹
simple_fw rs p = Decision FinalAllow ∨ simple_fw rs p = Decision FinalDeny"
proof(induction rs rule: has_default_policy.induct)
case 1 thus ?case by (simp)
next
case (2 m a) thus ?case by(cases a) (simp_all add: simple_match_any)
next
case (3 r1 r2 rs)
from 3 obtain a m where "r1 = SimpleRule m a" by (cases r1) simp
with 3 show ?case by (cases a) simp_all
qed
lemma has_default_policy_fst: "has_default_policy rs ⟹ has_default_policy (r#rs)"
apply(cases r, rename_tac m a, simp)
apply(cases rs)
by(simp_all)
text‹We can stop after a default rule (a rule which matches anything) is observed.›
fun cut_off_after_match_any :: "'i::len simple_rule list ⇒ 'i simple_rule list" where
"cut_off_after_match_any [] = []" |
"cut_off_after_match_any (SimpleRule m a # rs) =
(if m = simple_match_any then [SimpleRule m a] else SimpleRule m a # cut_off_after_match_any rs)"
lemma cut_off_after_match_any: "simple_fw (cut_off_after_match_any rs) p = simple_fw rs p"
apply(induction rs p rule: simple_fw.induct)
by(simp add: simple_match_any)+
lemma simple_fw_not_matches_removeAll: "¬ simple_matches m p ⟹
simple_fw (removeAll (SimpleRule m a) rs) p = simple_fw rs p"
apply(induction rs p rule: simple_fw.induct)
apply(simp)
apply(simp_all)
apply blast+
done
subsection‹Reality check: Validity of Simple Matches›
text‹While it is possible to construct a ‹simple_fw› expression that only matches a source
or destination port, such a match is not meaningful, as the presence of the port information is
dependent on the protocol. Thus, a match for a port should always include the match for a protocol.
Additionally, prefixes should be zero on bits beyond the prefix length.
›
definition "valid_prefix_fw m = valid_prefix (uncurry PrefixMatch m)"
lemma ipcidr_conjunct_valid:
"⟦valid_prefix_fw p1; valid_prefix_fw p2; ipcidr_conjunct p1 p2 = Some p⟧ ⟹ valid_prefix_fw p"
unfolding valid_prefix_fw_def
by(cases p; cases p1; cases p2) (simp add: ipcidr_conjunct.simps split: if_splits)
definition simple_match_valid :: "('i::len, 'a) simple_match_scheme ⇒ bool" where
"simple_match_valid m ≡
({p. simple_match_port (sports m) p} ≠ UNIV ∨ {p. simple_match_port (dports m) p} ≠ UNIV ⟶
proto m ∈ Proto `{TCP, UDP, L4_Protocol.SCTP}) ∧
valid_prefix_fw (src m) ∧ valid_prefix_fw (dst m)"
lemma simple_match_valid_alt[code_unfold]: "simple_match_valid = (λ m.
(let c = (λ(s,e). (s ≠ 0 ∨ e ≠ - 1)) in (
if c (sports m) ∨ c (dports m) then proto m = Proto TCP ∨ proto m = Proto UDP ∨ proto m = Proto L4_Protocol.SCTP else True)) ∧
valid_prefix_fw (src m) ∧ valid_prefix_fw (dst m))"
proof -
have simple_match_valid_alt_hlp1: "{p. simple_match_port x p} ≠ UNIV ⟷ (case x of (s,e) ⇒ s ≠ 0 ∨ e ≠ - 1)"
for x using simple_match_port_UNIV by auto
have simple_match_valid_alt_hlp2: "{p. simple_match_port x p} ≠ {} ⟷ (case x of (s,e) ⇒ s ≤ e)" for x by auto
show ?thesis
unfolding fun_eq_iff
unfolding simple_match_valid_def Let_def
unfolding simple_match_valid_alt_hlp1 simple_match_valid_alt_hlp2
apply(clarify, rename_tac m, case_tac "sports m"; case_tac "dports m"; case_tac "proto m")
by auto
qed
text‹Example:›
context
begin
private definition "example_simple_match1 ≡
⦇iiface = Iface ''+'', oiface = Iface ''+'', src = (0::32 word, 0), dst = (0, 0),
proto = Proto TCP, sports = (0, 1024), dports = (0, 1024)⦈"
lemma "simple_fw [SimpleRule example_simple_match1 Drop]
⦇p_iiface = '''', p_oiface = '''', p_src = (1::32 word), p_dst = 2, p_proto = TCP, p_sport = 8,
p_dport = 9, p_tcp_flags = {}, p_payload = ''''⦈ =
Decision FinalDeny" by eval
private definition "example_simple_match2 ≡ example_simple_match1⦇ proto := ProtoAny ⦈"
text‹Thus, ‹example_simple_match1› is valid, but if we set its protocol match to any, it isn't anymore›
private lemma "simple_match_valid example_simple_match1" by eval
private lemma "¬ simple_match_valid example_simple_match2" by eval
end
lemma simple_match_and_valid:
fixes m1 :: "'i::len simple_match"
assumes mv: "simple_match_valid m1" "simple_match_valid m2"
assumes mj: "simple_match_and m1 m2 = Some m"
shows "simple_match_valid m"
proof -
have simpl_ports_conjunct_not_UNIV:
"Collect (simple_match_port x) ≠ UNIV ⟹
x = simpl_ports_conjunct p1 p2 ⟹
Collect (simple_match_port p1) ≠ UNIV ∨ Collect (simple_match_port p2) ≠ UNIV"
for x p1 p2 by (metis Collect_cong mem_Collect_eq simple_ports_conjunct_correct)
have "valid_prefix_fw (src m1)" "valid_prefix_fw (src m2)" "valid_prefix_fw (dst m1)" "valid_prefix_fw (dst m2)"
using mv unfolding simple_match_valid_alt by simp_all
moreover have "ipcidr_conjunct (src m1) (src m2) = Some (src m)"
"ipcidr_conjunct (dst m1) (dst m2) = Some (dst m)"
using mj by(cases m1; cases m2; cases m; simp split: option.splits)+
ultimately have pv: "valid_prefix_fw (src m)" "valid_prefix_fw (dst m)"
using ipcidr_conjunct_valid by blast+
define nmu where "nmu ps ⟷ {p. simple_match_port ps p} ≠ UNIV" for ps
have "simpl_ports_conjunct (sports m1) (sports m2) = (sports m)" (is "?ph1 sports")
using mj by(cases m1; cases m2; cases m; simp split: option.splits)
hence sp: "nmu (sports m) ⟶ nmu (sports m1) ∨ nmu (sports m2)"
(is "?ph2 sports")
unfolding nmu_def using simpl_ports_conjunct_not_UNIV by metis
have "?ph1 dports" using mj by(cases m1; cases m2; cases m; simp split: option.splits)
hence dp: "?ph2 dports" unfolding nmu_def using simpl_ports_conjunct_not_UNIV by metis
define php where "php mr ⟷ proto mr ∈ Proto ` {TCP, UDP, L4_Protocol.SCTP}"
for mr :: "'i simple_match"
have pcj: "simple_proto_conjunct (proto m1) (proto m2) = Some (proto m)"
using mj by(cases m1; cases m2; cases m; simp split: option.splits)
hence p: "php m1 ⟹ php m"
"php m2 ⟹ php m"
using conjunctProtoD conjunctProtoD2 pcj unfolding php_def by auto
have "⋀mx. simple_match_valid mx ⟹ nmu (sports mx) ∨ nmu (dports mx) ⟹ php mx"
unfolding nmu_def php_def simple_match_valid_def by blast
hence mps: "nmu (sports m1) ⟹ php m1" "nmu (dports m1) ⟹ php m1"
"nmu (sports m2) ⟹ php m2" "nmu (dports m2) ⟹ php m2" using mv by blast+
have pa: "nmu (sports m) ∨ nmu (dports m) ⟶ php m"
using sp dp mps p by fast
show ?thesis
unfolding simple_match_valid_def
using pv pa[unfolded nmu_def php_def] by blast
qed
definition "simple_fw_valid ≡ list_all (simple_match_valid ∘ match_sel)"
text‹The simple firewall does not care about tcp flags, payload, or any other packet extensions.›
lemma simple_matches_extended_packet:
"simple_matches m
⦇p_iiface = iifce,
oiface = oifce,
p_src = s, dst = d,
p_proto = prot,
p_sport = sport, p_dport = dport,
tcp_flags = tcp_flags, p_payload = payload1⦈
⟷
simple_matches m
⦇p_iiface = iifce,
oiface = oifce,
p_src = s, p_dst = d,
p_proto = prot,
p_sport = sport, p_dport = dport,
p_tcp_flags = tcp_flags2, p_payload = payload2, … = aux⦈
"
by(simp add: simple_matches.simps)
end