Theory IP_Address_Space_Examples_All_Small

theory IP_Address_Space_Examples_All_Small
imports
  Iptables_Semantics.Parser
begin


definition preprocess where
  "preprocess unfold closure ipassmt def fw ≡ to_simple_firewall (closure
              (optimize_matches (abstract_primitive (λr. case r of Pos a ⇒ is_Iiface a ∨ is_Oiface a ∨ is_L4_Flags a | Neg a ⇒ is_Iiface a ∨ is_Oiface a ∨ is_Prot a ∨ is_L4_Flags a))
              (closure
              (iface_try_rewrite ipassmt None
              (closure
              (packet_assume_new
              (unfold def (map_of fw))))))))"


definition preprocess_keep_ifce where
  "preprocess_keep_ifce unfold closure ipassmt def fw ≡ to_simple_firewall (closure
              (optimize_matches abstract_for_simple_firewall
              (closure
              (optimize_matches (iiface_constrain (map_of_ipassmt ipassmt))
              (closure
              (packet_assume_new
              (unfold def (map_of fw))))))))"


datatype ipt_chain = FWD | INP

fun get_unfold where
  "get_unfold FWD = unfold_ruleset_FORWARD" |
  "get_unfold INP = unfold_ruleset_INPUT"

fun ipt_chain_toSting where
  "ipt_chain_toSting FWD = ''FORWARD''" |
  "ipt_chain_toSting INPO = ''INPUT''"

definition bench where
  "bench closure f ipassmt def fw_in ≡ let fw = preprocess (get_unfold f) closure ipassmt def fw_in in
      (length ((get_unfold f) def (map_of fw_in)), length (preprocess_keep_ifce (get_unfold f) closure ipassmt def fw_in), length fw, length (getParts fw), length (build_ip_partition parts_connection_ssh fw), length (build_ip_partition parts_connection_http fw))"
definition view where
  "view closure f ipassmt def fw_in ≡ let fw = preprocess (get_unfold f) closure ipassmt def fw_in in
      (''x'',
       map (simple_rule_iptables_save_toString (ipt_chain_toSting f)) (preprocess_keep_ifce (get_unfold f) closure ipassmt def fw_in),
       map (simple_rule_iptables_save_toString (ipt_chain_toSting f)) fw,
       map ipv4addr_wordinterval_toString (getParts fw),
       (access_matrix_pretty_ipv4 parts_connection_ssh fw),
       (access_matrix_pretty_ipv4 parts_connection_http fw))"


(*Do we have code?*)
export_code bench view checking SML

context
begin
  private  parse_iptables_save fw12 = config_memphis_testbed "iptables-save"
  thm fw12_def

  value[code] "bench upper_closure FWD ipassmt_generic_ipv4 fw12_FORWARD_default_policy fw12"
  value[code] "view upper_closure FWD ipassmt_generic_ipv4 fw12_FORWARD_default_policy fw12"

  value[code] "bench lower_closure FWD ipassmt_generic_ipv4 fw12_FORWARD_default_policy fw12"
  value[code] "view lower_closure FWD ipassmt_generic_ipv4 fw12_FORWARD_default_policy fw12"
end

context
begin
  (*Firewall generated by topoS, some manual tuning, running on a docker host.*)
  private parse_iptables_save fwdocker = docker_topos "iptables-save.topos4.1"
  thm fwdocker_def

  value[code] "bench upper_closure FWD ipassmt_generic_ipv4 fwdocker_FORWARD_default_policy fwdocker"
  value[code] "view upper_closure FWD ipassmt_generic_ipv4 fwdocker_FORWARD_default_policy fwdocker"

  value[code] "bench lower_closure FWD ipassmt_generic_ipv4 fwdocker_FORWARD_default_policy fwdocker"
  value[code] "view lower_closure FWD ipassmt_generic_ipv4 fwdocker_FORWARD_default_policy fwdocker"
end

context
begin
 private parse_iptables_save fw13 = "config_random_srv" "iptables-save"

 thm fw13_def

  value[code] "bench upper_closure INP ipassmt_generic_ipv4 fw13_INPUT_default_policy fw13"
  value[code] "view upper_closure INP ipassmt_generic_ipv4 fw13_INPUT_default_policy fw13"

  value[code] "bench lower_closure INP ipassmt_generic_ipv4 fw13_INPUT_default_policy fw13"
  value[code] "view lower_closure INP ipassmt_generic_ipv4 fw13_INPUT_default_policy fw13"
end



context
begin
  private parse_iptables_save fw_home_user ="config_home_user" "typical_home_user_iptables-save"
  thm fw_home_user_def

  private  definition "ipassmt_wg = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''eth1'', all_but_those_ips [
    (ipv4addr_of_dotdecimal (127,0,0,0),8),
    (ipv4addr_of_dotdecimal (192,168,0,0), 16),
    (ipv4addr_of_dotdecimal (172,16,0,0), 12),
    (ipv4addr_of_dotdecimal (10,0,0,0), 8)
    ]), ― ‹INET›
  (Iface ''tun0'', [(ipv4addr_of_dotdecimal (10,12,0,0),16)]),
  (Iface ''eth0.10'', [(ipv4addr_of_dotdecimal (192,168,10,0),24)]),
  (Iface ''eth0.11'', [(ipv4addr_of_dotdecimal (192,168,11,0),24)]),
  (Iface ''eth0.12'', [(ipv4addr_of_dotdecimal (192,168,12,0),24)]),
  (Iface ''eth0.13'', [(ipv4addr_of_dotdecimal (192,168,13,0),24)]),
  (Iface ''eth0.14'', [(ipv4addr_of_dotdecimal (192,168,14,0),24)]),
  (Iface ''eth0.19'', [(ipv4addr_of_dotdecimal (192,168,19,0),24)]),
  (Iface ''eth0.20'', [(ipv4addr_of_dotdecimal (192,168,20,0),24)]),
  (Iface ''eth0.21'', [(ipv4addr_of_dotdecimal (192,168,21,0),24)]),
  (Iface ''eth0.22'', [(ipv4addr_of_dotdecimal (192,168,22,0),24)]),
  (Iface ''eth0.23'', [(ipv4addr_of_dotdecimal (192,168,23,0),24)]),
  (Iface ''eth0.24'', [(ipv4addr_of_dotdecimal (192,168,24,0),24)])]"

  value[code] "collect_ifaces (upper_closure (unfold_ruleset_FORWARD fw_home_user_FORWARD_default_policy (map_of_string_ipv4 fw_home_user)))"

  value[code] "debug_ipassmt_ipv4 ipassmt_wg (upper_closure (unfold_ruleset_FORWARD fw_home_user_FORWARD_default_policy (map_of_string_ipv4 fw_home_user)))"

  value[code] "bench upper_closure FWD ipassmt_wg fw_home_user_FORWARD_default_policy fw_home_user"
  value[code] "view upper_closure FWD ipassmt_wg fw_home_user_FORWARD_default_policy fw_home_user"

  value[code] "bench lower_closure FWD ipassmt_wg fw_home_user_FORWARD_default_policy fw_home_user"
  value[code] "view lower_closure FWD ipassmt_wg fw_home_user_FORWARD_default_policy fw_home_user"
end



context begin
 private definition "everything_but_private_ips = all_but_those_ips [
    (ipv4addr_of_dotdecimal (192,168,0,0), 16),
    (ipv4addr_of_dotdecimal (172,16,0,0), 12),
    (ipv4addr_of_dotdecimal (10,0,0,0), 8)
    ]"

  private definition "ipassmt = [(Iface ''ldit'', [(ipv4addr_of_dotdecimal (10,13,42,136), 29)]),
  (Iface ''lmd'', [(ipv4addr_of_dotdecimal (10,13,42,128), 29)]),
  (Iface ''loben'', [(ipv4addr_of_dotdecimal (10,13,42,144), 28)]),
  (Iface ''wg'', [(ipv4addr_of_dotdecimal (10,13,42,176), 28)]),
  (Iface ''wt'', [(ipv4addr_of_dotdecimal (10,13,42,160), 28)]),
  (Iface ''lup'', everything_but_private_ips), ― ‹INET›
  (Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''vpriv'', [(0,0)]),
  (Iface ''vshit'', [(0,0)]),
  (Iface ''vocb'', [(0,0)]),
  (Iface ''lua'', [(0,0)])
  ]"


 private parse_iptables_save fw1 = "configs_sqrl_shorewall" "2015_aug_iptables-save-spoofing-protection"

  value[code] "bench upper_closure FWD ipassmt fw1_FORWARD_default_policy fw1"
  value[code] "view upper_closure FWD ipassmt fw1_FORWARD_default_policy fw1"

  value[code] "bench lower_closure FWD ipassmt fw1_FORWARD_default_policy fw1"
  value[code] "view lower_closure FWD ipassmt fw1_FORWARD_default_policy fw1"


  value[code] "bench upper_closure INP ipassmt fw1_INPUT_default_policy fw1"
  value[code] "view upper_closure INP ipassmt fw1_INPUT_default_policy fw1"

  value[code] "bench lower_closure INP ipassmt fw1_INPUT_default_policy fw1"
  value[code] "view lower_closure INP ipassmt fw1_INPUT_default_policy fw1"

 private parse_iptables_save fw2 = "configs_sqrl_shorewall" "2014_sep_iptables-saveakachan"
  value[code] "Semantics_Goto.rewrite_Goto fw2"


  value[code] "bench upper_closure FWD ipassmt fw2_FORWARD_default_policy (Semantics_Goto.rewrite_Goto fw2)"
  value[code] "view upper_closure FWD ipassmt fw2_FORWARD_default_policy (Semantics_Goto.rewrite_Goto fw2)"


  value[code] "bench lower_closure FWD ipassmt fw2_FORWARD_default_policy (Semantics_Goto.rewrite_Goto fw2)"
  value[code] "view lower_closure FWD ipassmt fw2_FORWARD_default_policy (Semantics_Goto.rewrite_Goto fw2)"
end

context
begin
  private definition "ipassmt2 = [(Iface ''eth0'', [(ipv4addr_of_dotdecimal (192,168,1,0), 24)]),
  (Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)])
  ]"
 private parse_iptables_save fw3 = "configs_synology_diskstation_ds414" "iptables-save_jun_2015_legacyifacerules"

  value[code] "bench upper_closure INP ipassmt2 fw3_INPUT_default_policy fw3"
  value[code] "view upper_closure INP ipassmt2 fw3_INPUT_default_policy fw3"


  definition web8080 where "web8080 = ⦇pc_iiface=''1'', pc_oiface=''1'', pc_proto=TCP,
                               pc_sport=10000, pc_dport=8080⦈"

  value[code] "let fw = preprocess (get_unfold INP) upper_closure ipassmt2 fw3_INPUT_default_policy fw3 in
               map ipv4addr_wordinterval_toString (build_ip_partition web8080 fw)"

  value[code] "bench lower_closure INP ipassmt2 fw3_INPUT_default_policy fw3"
  value[code] "view lower_closure INP ipassmt2 fw3_INPUT_default_policy fw3"

end



context
begin
 private parse_iptables_save fw4 = "configs_srvs_ufw" "server2-iptables-save"
 thm fw4_def

  value[code] "bench upper_closure INP ipassmt_generic_ipv4 fw4_INPUT_default_policy fw4"
  value[code] "view upper_closure INP ipassmt_generic_ipv4 fw4_INPUT_default_policy fw4"

  definition "mysql = ⦇pc_iiface=''1'', pc_oiface=''1'', pc_proto=TCP,
                               pc_sport=10000, pc_dport=3306⦈"
  value[code] "let fw = preprocess (get_unfold INP) upper_closure ipassmt_generic_ipv4 fw4_INPUT_default_policy fw4 in
             map ipv4addr_wordinterval_toString (build_ip_partition mysql fw)"

  value[code] "bench lower_closure INP ipassmt_generic_ipv4 fw4_INPUT_default_policy fw4"
  value[code] "view lower_closure INP ipassmt_generic_ipv4 fw4_INPUT_default_policy fw4"
end

context
begin
  private parse_iptables_save fw_worst = "worst_case" "iptables-save"
  thm fw_worst_def

  value[code] "bench upper_closure FWD ipassmt_generic_ipv4 fw_worst_FORWARD_default_policy fw_worst"
  value[code] "view upper_closure FWD ipassmt_generic_ipv4 fw_worst_FORWARD_default_policy fw_worst"

  value[code] "bench lower_closure FWD ipassmt_generic_ipv4 fw_worst_FORWARD_default_policy fw_worst"
  value[code] "view lower_closure FWD ipassmt_generic_ipv4 fw_worst_FORWARD_default_policy fw_worst"
end


context
begin
  private parse_iptables_save fw5 = "linux.gda.pl" "firewallp.txt"
  thm fw5_def

  value[code] "bench upper_closure FWD ipassmt_generic_ipv4 fw5_FORWARD_default_policy fw5"
  value[code] "view upper_closure FWD ipassmt_generic_ipv4 fw5_FORWARD_default_policy fw5"

  value[code] "bench lower_closure FWD ipassmt_generic_ipv4 fw5_FORWARD_default_policy fw5"
  value[code] "view lower_closure FWD ipassmt_generic_ipv4 fw5_FORWARD_default_policy fw5"
end


context
begin
  private parse_iptables_save fw6 = "openvpn.eu" "iptables-save"
  thm fw6_def

  private  definition "ipassmt6 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''eth0'', [(ipv4addr_of_dotdecimal (192,168,0,0),24)]),
  (Iface ''eth1'', [(ipv4addr_of_dotdecimal (192,168,2,0),24)])]"


  value[code] "bench upper_closure FWD ipassmt6 fw6_FORWARD_default_policy fw6"
  value[code] "view upper_closure FWD ipassmt6 fw6_FORWARD_default_policy fw6"

  value[code] "bench lower_closure FWD ipassmt6 fw6_FORWARD_default_policy fw6"
  value[code] "view lower_closure FWD ipassmt6 fw6_FORWARD_default_policy fw6"
end



context
begin
  private parse_iptables_save fw7 = "openwrt.org" "iptables-save-AA.txt_fixed_newline"
  thm fw7_def

  private  definition "ipassmt7 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''eth0'', [(ipv4addr_of_dotdecimal (192,168,1,0),24)]),
  ⌦‹(Iface ''eth0.2'', [(ipv4addr_of_dotdecimal (192,168,2,0),24)]),› ― ‹cannot infer›
  (Iface ''tun0'', [(ipv4addr_of_dotdecimal (10,8,0,0),24)]),
  (Iface ''br-lan'', [(ipv4addr_of_dotdecimal (192,168,1,0),24)])]"


  value[code] "bench upper_closure FWD ipassmt7 fw7_FORWARD_default_policy fw7"
  value[code] "view upper_closure FWD ipassmt7 fw7_FORWARD_default_policy fw7"

  value[code] "bench lower_closure FWD ipassmt7 fw7_FORWARD_default_policy fw7"
  value[code] "view lower_closure FWD ipassmt7 fw7_FORWARD_default_policy fw7"
end




context
begin
  private parse_iptables_save fw8 = "pastebin.com_bbWXHaTn" "iptables-save"
  thm fw8_def

  value[code] "bench upper_closure FWD ipassmt_generic_ipv4 fw8_FORWARD_default_policy fw8"
  value[code] "view upper_closure FWD ipassmt_generic_ipv4 fw8_FORWARD_default_policy fw8"

  value[code] "bench lower_closure FWD ipassmt_generic_ipv4 fw8_FORWARD_default_policy fw8"
  value[code] "view lower_closure FWD ipassmt_generic_ipv4 fw8_FORWARD_default_policy fw8"
end



context
begin
  private parse_iptables_save fw9 = "rlworkman.net" "iptables-save"
  thm fw9_def

  (*I loaded the script on my local machine*)
  private definition "ipassmt9 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''eth0'', [(ipv4addr_of_dotdecimal (192,168,13,0),24)]),
  (Iface ''ppp0'', all_but_those_ips [(ipv4addr_of_dotdecimal (192,168,13,0),24), (ipv4addr_of_dotdecimal (127,0,0,0),8)])]"

  value[code] "bench upper_closure FWD ipassmt9 fw9_FORWARD_default_policy fw9"
  value[code] "view upper_closure FWD ipassmt9 fw9_FORWARD_default_policy fw9"

  (*quite good results*)
  value[code] "bench lower_closure FWD ipassmt9 fw9_FORWARD_default_policy fw9"
  value[code] "view lower_closure FWD ipassmt9 fw9_FORWARD_default_policy fw9"


  value[code] "bench upper_closure INP ipassmt9 fw9_INPUT_default_policy fw9"
  value[code] "view upper_closure INP ipassmt9 fw9_INPUT_default_policy fw9"

  value[code] "bench lower_closure INP ipassmt9 fw9_INPUT_default_policy fw9"
  value[code] "view lower_closure INP ipassmt9 fw9_INPUT_default_policy fw9"
end



context
begin
  private parse_iptables_save fw10 = "sargon" "iptables-save.txt"
  thm fw10_def

  value[code] "bench upper_closure INP ipassmt_generic_ipv4 fw10_INPUT_default_policy fw10"
  value[code] "view upper_closure INP ipassmt_generic_ipv4 fw10_INPUT_default_policy fw10"

  value[code] "bench lower_closure INP ipassmt_generic_ipv4 fw10_INPUT_default_policy fw10"
  value[code] "view lower_closure INP ipassmt_generic_ipv4 fw10_INPUT_default_policy fw10"
end


context
begin
 private parse_iptables_save fw11 = "gopherproxy.meulie.net" "iptables-save"
 thm fw11_def

  value[code] "bench upper_closure INP ipassmt_generic_ipv4 fw11_INPUT_default_policy fw11"
  value[code] "view upper_closure INP ipassmt_generic_ipv4 fw11_INPUT_default_policy fw11"

  value[code] "bench lower_closure INP ipassmt_generic_ipv4 fw11_INPUT_default_policy fw11"
  value[code] "view lower_closure INP ipassmt_generic_ipv4 fw11_INPUT_default_policy fw11"

end


context
begin
 private parse_iptables_save fw14 = "medium-sized-company" "iptables-save"
 thm fw14_def
 private definition "ipassmt14 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''eth0'', [(ipv4addr_of_dotdecimal (172,16,2,0),24)])
  ]"

  value[code] "bench upper_closure INP ipassmt14 fw14_INPUT_default_policy fw14"
  value[code] "view upper_closure INP ipassmt14 fw14_INPUT_default_policy fw14"

  value[code] "bench lower_closure INP ipassmt14 fw14_INPUT_default_policy fw14"
  value[code] "view lower_closure INP ipassmt14 fw14_INPUT_default_policy fw14"

  value[code] "bench upper_closure FWD ipassmt14 fw14_FORWARD_default_policy fw14"
  value[code] "view upper_closure FWD ipassmt14 fw14_FORWARD_default_policy fw14"

  value[code] "bench lower_closure FWD ipassmt14 fw14_FORWARD_default_policy fw14"
  value[code] "view lower_closure FWD ipassmt14 fw14_FORWARD_default_policy fw14"

end


context
begin
  private parse_iptables_save fw15 = "configs_ugent" "iptables-save.v1.4.21"
  thm fw15_def
 private definition "ipassmt15 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)]),
  (Iface ''eth0'', [(ipv4addr_of_dotdecimal (192,168,134,0),24)]),
  (Iface ''eth1'', [(ipv4addr_of_dotdecimal (192,168,16,0),24)]),
  (Iface ''eth2'', [(ipv4addr_of_dotdecimal (131,159,15,64),26)]),
  (Iface ''virbr0'', [(ipv4addr_of_dotdecimal (192,168,122,0),24)])
  ]"

  value[code] "bench upper_closure INP ipassmt15 fw15_INPUT_default_policy fw15"
  value[code] "view upper_closure INP ipassmt15 fw15_INPUT_default_policy fw15"

  value[code] "bench lower_closure INP ipassmt15 fw15_INPUT_default_policy fw15"
  value[code] "view lower_closure INP ipassmt15 fw15_INPUT_default_policy fw15"


  definition srctcp137dst137 where "srctcp137dst137 = ⦇pc_iiface=''1'', pc_oiface=''1'', pc_proto=TCP,
                               pc_sport=137, pc_dport=137⦈"
  value[code] "let fw = preprocess (get_unfold INP) upper_closure ipassmt15 fw15_INPUT_default_policy fw15 in
               map ipv4addr_wordinterval_toString (build_ip_partition srctcp137dst137 fw)"

  definition tcpdst137 where "tcpdst137 = ⦇pc_iiface=''1'', pc_oiface=''1'', pc_proto=TCP,
                               pc_sport=10000, pc_dport=137⦈"
  value[code] "let fw = preprocess (get_unfold INP) upper_closure ipassmt15 fw15_INPUT_default_policy fw15 in
               map ipv4addr_wordinterval_toString (build_ip_partition tcpdst137 fw)"
end

end