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

  ― ‹by the way, the words do not wrap around›
  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)
  
    (* prefix validity. That's simple. *)
    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+
  
    (* now for the source ports… *)
    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
  
    (* dst ports: mutatis mutandem *)
    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
  
    (* And an argument for the protocol. *)
    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
  
    (* Since I'm trying to trick the simplifier with these defs, I need these as explicit statements: *)
    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"
    (*  apply(intro impI)
      apply(elim disjE)
      apply(drule sp[THEN mp])
      apply(elim disjE)
      apply(drule mps)
      apply(elim p; fail) *)
      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