diff --git a/thys/Iptables_Semantics/Examples/Code_haskell.thy b/thys/Iptables_Semantics/Code_haskell.thy rename from thys/Iptables_Semantics/Examples/Code_haskell.thy rename to thys/Iptables_Semantics/Code_haskell.thy --- a/thys/Iptables_Semantics/Examples/Code_haskell.thy +++ b/thys/Iptables_Semantics/Code_haskell.thy @@ -1,85 +1,85 @@ theory Code_haskell imports Routing.IpRoute_Parser - "../Primitive_Matchers/Parser" + "Primitive_Matchers/Parser" begin definition word_less_eq :: "('a::len) word \ ('a::len) word \ bool" where "word_less_eq a b \ a \ b" definition word_to_nat :: "('a::len) word \ nat" where "word_to_nat = Word.unat" definition mk_Set :: "'a list \ 'a set" where "mk_Set = set" text\Assumes that you call @{const fill_l4_protocol} after parsing!\ definition mk_L4Ports_pre :: "raw_ports \ ipt_l4_ports" where "mk_L4Ports_pre ports_raw = L4Ports 0 ports_raw" fun ipassmt_iprange_translate :: "'i::len ipt_iprange list negation_type \ ('i word \ nat) list" where "ipassmt_iprange_translate (Pos ips) = concat (map ipt_iprange_to_cidr ips)" | "ipassmt_iprange_translate (Neg ips) = all_but_those_ips (concat (map ipt_iprange_to_cidr ips))" definition to_ipassmt :: "(iface \ 'i::len ipt_iprange list negation_type) list \ (iface \ ('i word \ nat) list) list" where "to_ipassmt assmt = map (\(ifce, ips). (ifce, ipassmt_iprange_translate ips)) assmt" definition "zero_word \ 0 :: ('a :: len) word" export_code Rule Match MatchNot MatchAnd MatchAny Src Dst IIface OIface Prot Src_Ports Dst_Ports CT_State Extra mk_L4Ports_pre ProtoAny Proto TCP UDP ICMP L4_Protocol.IPv6ICMP L4_Protocol.SCTP L4_Protocol.GRE L4_Protocol.ESP L4_Protocol.AH Iface integer_to_16word nat_to_16word nat_of_integer integer_of_nat word_less_eq word_to_nat nat_to_8word IpAddrNetmask IpAddrRange IpAddr CT_New CT_Established CT_Related CT_Untracked CT_Invalid TCP_Flags TCP_SYN TCP_ACK TCP_FIN TCP_RST TCP_URG TCP_PSH Accept Drop Log Reject Call Return Goto Empty Unknown action_toString (*IPv4*) ipv4addr_of_dotdecimal ipt_ipv4range_toString common_primitive_ipv4_toString common_primitive_match_expr_ipv4_toString simple_rule_ipv4_toString (*IPv6*) mk_ipv6addr IPv6AddrPreferred ipv6preferred_to_int int_to_ipv6preferred ipt_ipv6range_toString common_primitive_ipv6_toString common_primitive_match_expr_ipv6_toString simple_rule_ipv6_toString (*Goto support*) Semantics_Goto.rewrite_Goto_safe (*parser helpers:*) alist_and' compress_parsed_extra fill_l4_protocol Pos Neg mk_Set unfold_ruleset_CHAIN_safe map_of_string upper_closure abstract_for_simple_firewall optimize_matches packet_assume_new to_simple_firewall to_simple_firewall_without_interfaces sanity_wf_ruleset has_default_policy (*spoofing:*) ipassmt_generic_ipv4 ipassmt_generic_ipv6 no_spoofing_iface ipassmt_sanity_defined map_of_ipassmt to_ipassmt ipassmt_diff Pos Neg (*debug*) simple_fw_valid debug_ipassmt_ipv4 debug_ipassmt_ipv6 (*ip partitioning*) access_matrix_pretty_ipv4 access_matrix_pretty_ipv6 mk_parts_connection_TCP (*parts_connection_ssh parts_connection_http*) (* routing *) PrefixMatch routing_rule_ext routing_action_ext routing_action_oiface_update metric_update routing_action_next_hop_update empty_rr_hlp sort_rtbl prefix_match_32_toString routing_rule_32_toString prefix_match_128_toString routing_rule_128_toString default_prefix sanity_ip_route ipassmt_diff routing_ipassmt checking SML Haskell? (*in Haskell module_name "Network.IPTables.Generated" file "generated_code/"*) end diff --git a/thys/Iptables_Semantics/Examples/Example_Semantics.thy b/thys/Iptables_Semantics/Example_Semantics.thy rename from thys/Iptables_Semantics/Examples/Example_Semantics.thy rename to thys/Iptables_Semantics/Example_Semantics.thy --- a/thys/Iptables_Semantics/Examples/Example_Semantics.thy +++ b/thys/Iptables_Semantics/Example_Semantics.thy @@ -1,87 +1,87 @@ theory Example_Semantics -imports "../Call_Return_Unfolding" "../Primitive_Matchers/Common_Primitive_Matcher" +imports Call_Return_Unfolding "Primitive_Matchers/Common_Primitive_Matcher" begin section\Examples Big Step Semantics\ text\We use a primitive matcher which always applies. We don't care about matching in this example.\ fun applies_Yes :: "('a, 'p) matcher" where "applies_Yes m p = True" lemma[simp]: "Semantics.matches applies_Yes MatchAny p" by simp lemma[simp]: "Semantics.matches applies_Yes (Match e) p" by simp definition "m=Match (Src (IpAddr (0::ipv4addr)))" lemma[simp]: "Semantics.matches applies_Yes m p" by (simp add: m_def) lemma "[''FORWARD'' \ [(Rule m Log), (Rule m Accept), (Rule m Drop)]],applies_Yes,p\ \[Rule MatchAny (Call ''FORWARD'')], Undecided\ \ (Decision FinalAllow)" apply(rule call_result) apply(auto) apply(rule seq_cons) apply(auto intro:Semantics.log) apply(rule seq_cons) apply(auto intro: Semantics.accept) apply(rule Semantics.decision) done lemma "[''FORWARD'' \ [(Rule m Log), (Rule m (Call ''foo'')), (Rule m Accept)], ''foo'' \ [(Rule m Log), (Rule m Return)]],applies_Yes,p\ \[Rule MatchAny (Call ''FORWARD'')], Undecided\ \ (Decision FinalAllow)" apply(rule call_result) apply(auto) apply(rule seq_cons) apply(auto intro: Semantics.log) apply(rule seq_cons) apply(rule Semantics.call_return[where rs\<^sub>1="[Rule m Log]" and rs\<^sub>2="[]"]) apply(simp)+ apply(auto intro: Semantics.log) apply(auto intro: Semantics.accept) done lemma "[''FORWARD'' \ [Rule m (Call ''foo''), Rule m Drop], ''foo'' \ []],applies_Yes,p\ \[Rule MatchAny (Call ''FORWARD'')], Undecided\ \ (Decision FinalDeny)" apply(rule call_result) apply(auto) apply(rule Semantics.seq_cons) apply(rule Semantics.call_result) apply(auto) apply(rule Semantics.skip) apply(auto intro: deny) done lemma "((\rs. process_call [''FORWARD'' \ [Rule m (Call ''foo''), Rule m Drop], ''foo'' \ []] rs)^^2) [Rule MatchAny (Call ''FORWARD'')] = [Rule (MatchAnd MatchAny m) Drop]" by eval hide_const m definition "pkt=\p_iiface=''+'', p_oiface=''+'', p_src=0, p_dst=0, p_proto=TCP, p_sport=0, p_dport=0, p_tcp_flags = {TCP_SYN}, p_payload='''',p_tag_ctstate= CT_New\" text\We tune the primitive matcher to support everything we need in the example. Note that the undefined cases cannot be handled with these exact semantics!\ fun applies_exampleMatchExact :: "(32 common_primitive, 32 tagged_packet) matcher" where "applies_exampleMatchExact (Src (IpAddr addr)) p \ p_src p = addr" | "applies_exampleMatchExact (Dst (IpAddr addr)) p \ p_dst p = addr" | "applies_exampleMatchExact (Prot ProtoAny) p \ True" | "applies_exampleMatchExact (Prot (Proto pr)) p \ p_proto p = pr" (* not exhaustive, only an example!!*) lemma "[''FORWARD'' \ [ Rule (MatchAnd (Match (Src (IpAddr 0))) (Match (Dst (IpAddr 0)))) Reject, Rule (Match (Dst (IpAddr 0))) Log, Rule (Match (Prot (Proto TCP))) Accept, Rule (Match (Prot (Proto TCP))) Drop] ],applies_exampleMatchExact, pkt\p_src:=(ipv4addr_of_dotdecimal (1,2,3,4)), p_dst:=(ipv4addr_of_dotdecimal (0,0,0,0))\\ \[Rule MatchAny (Call ''FORWARD'')], Undecided\ \ (Decision FinalAllow)" apply(rule call_result) apply(auto) apply(rule Semantics.seq_cons) apply(auto intro: Semantics.nomatch simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def) apply(rule Semantics.seq_cons) apply(auto intro: Semantics.log simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def) apply(rule Semantics.seq_cons) apply(auto simp add: pkt_def intro: Semantics.accept) apply(auto intro: Semantics.decision) done end diff --git a/thys/Iptables_Semantics/Examples/Parser_Test/Parser6_Test.thy b/thys/Iptables_Semantics/Examples/Parser_Test/Parser6_Test.thy --- a/thys/Iptables_Semantics/Examples/Parser_Test/Parser6_Test.thy +++ b/thys/Iptables_Semantics/Examples/Parser_Test/Parser6_Test.thy @@ -1,73 +1,73 @@ theory Parser6_Test -imports "../../Primitive_Matchers/Parser6" +imports Iptables_Semantics.Parser6 begin text\ Argument 1: the name of the prefix for all constants which will be defined. Argument 2: The path to the firewall (ip6tables-save). A path is represented as list. \ parse_ip6tables_save parser6_test_firewall = "data" "ip6tables-save" term parser6_test_firewall thm parser6_test_firewall_def thm parser6_test_firewall_FORWARD_default_policy_def value[code] "parser6_test_firewall" lemma "parser6_test_firewall = [(''FORWARD'', [Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv6preferred_to_int (IPv6AddrPreferred 0x2001 0xdb8 0 0 0x8d3 0 0 1)) 128))) (MatchAnd (Match (Dst (IpAddrNetmask (ipv6preferred_to_int (IPv6AddrPreferred 0x2001 0xdb8 0 0 0x8d3 0 0 0)) 128))) (MatchAnd (Match (IIface (Iface ''eth0''))) (Match (OIface (Iface ''foobar'')))))) (Call ''gh32_-2qns''), Rule (MatchAnd (Match (Extra ''-d ::ffff:127.0.0.1/128'')) \ \We do not support this IPv6 notation!\ (MatchAnd (Match (IIface (Iface ''eth0''))) (Match (OIface (Iface ''foobar''))))) (Call ''gh32_-2qns''), Rule (MatchAnd (Match (Src (IpAddrNetmask 1 128))) (MatchAnd (Match (IIface (Iface ''lo''))) (Match (OIface (Iface ''lo''))))) action.Accept, Rule (Match (Extra (''--log-prefix '' @ [char_of_nat 34] @ ''~%&/()=?'' @ [char_of_nat 34] @ '' --log-level 6''))) Log, Rule (Match (Src (IpAddrNetmask 0 128))) action.Drop]), (''INPUT'', []), (''OUTPUT'', []), (''gh32_-2qns'', [Rule (Match (Src (IpAddrNetmask (ipv6preferred_to_int (IPv6AddrPreferred 0x2001 0xdb8 0x85a3 0x8d3 0x1319 0x8a2e 0x370 0x7344)) 128))) Reject, Rule MatchAny Empty, Rule MatchAny action.Accept])]" by eval (*Broken: (IpAddr 0xFFFF0127)) (Match (Extra ''.0.0.1/128'') ! An address must have a word boundary!*) lemma "simple_fw_valid (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_FORWARD parser6_test_firewall_FORWARD_default_policy (map_of parser6_test_firewall)))))))" by eval lemma "map simple_rule_ipv6_toString (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_FORWARD parser6_test_firewall_FORWARD_default_policy (map_of parser6_test_firewall))))))) = [''ACCEPT all -- 2001:db8::8d3:0:0:1/128 2001:db8:0:0:8d3::/128 in: eth0 out: foobar '', ''ACCEPT all -- ::/0 ::/0 in: eth0 out: foobar '', ''ACCEPT all -- ::1/128 ::/0 in: lo out: lo '', ''DROP all -- ::/128 ::/0 '', ''DROP all -- ::/0 ::/0 '']" by eval (*33.224s*) end diff --git a/thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy b/thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy --- a/thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy +++ b/thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy @@ -1,465 +1,465 @@ theory Analyze_Synology_Diskstation imports iptables_Ln_tuned_parsed (*2014 firewall dump*) Iptables_Semantics.Parser - "../../Primitive_Matchers/Parser6" + Iptables_Semantics.Parser6 begin section\Example: Synology Diskstation 2014\ text\We analyze a dump of a NAS. The dump was created 2014. Unfortunately, we don't have an \iptables-save\ dump from that time and have to rely on the \iptables -L -n\ dump. This dump was translated by our legacy python importer.\ text\we removed the established,related rule\ definition "example_ruleset == firewall_chains(''INPUT'' \ remove1 (Rule (MatchAnd (Match (Src (IpAddrNetmask 0 0))) (MatchAnd (Match (Dst (IpAddrNetmask 0 0))) (MatchAnd (Match (Prot (ProtoAny))) (Match (Extra (''state RELATED,ESTABLISHED'')))))) (action.Accept)) (the (firewall_chains ''INPUT'')))" text\Infix pretty-printing for @{const MatchAnd} and @{const MatchNot}.\ abbreviation MatchAndInfix :: "'a match_expr \ 'a match_expr \ 'a match_expr" (infixr "MATCHAND" 65) where "MatchAndInfix m1 m2 \ MatchAnd m1 m2" abbreviation MatchNotPrefix :: "'a match_expr \ 'a match_expr" ("\ \_\" 66) where "MatchNotPrefix m \ MatchNot m" (*abbreviation MatchPrefix :: "'a \ 'a match_expr" ("\ _" 67) where (*This is too slow*) "MatchPrefix m \ Match m"*) (*This syntax can be pretty confusing when mixing it with other theories. Do not use outside this example!*) lemma "unfold_ruleset_INPUT action.Accept example_ruleset = [Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND \ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND \ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND \ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND \ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND \ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04'')) action.Drop, Rule (\ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND \ \Match (Extra ''Prot icmp'') MATCHAND Match (Extra ''icmptype 8 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x04 limit: avg 1/sec burst 5'')\ MATCHAND \ \Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02 limit: avg 10000/sec burst 100'')\ MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp flags:0x17/0x02'')) action.Drop, Rule (Match (Prot (Proto TCP)) MATCHAND Match (Extra ''tcp dpt:22'')) action.Drop, Rule (Match (Prot (Proto TCP)) MATCHAND Match (Extra ''multiport dports 21,873,5005,5006,80,548,111,2049,892'')) action.Drop, Rule (Match (Prot (Proto UDP)) MATCHAND Match (Extra ''multiport dports 123,111,2049,892,5353'')) action.Drop, Rule (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192, 168, 0, 0)) 16))) action.Accept, Rule MatchAny action.Drop, Rule MatchAny action.Accept, Rule MatchAny action.Accept] " by eval lemma "good_ruleset (unfold_ruleset_INPUT action.Accept example_ruleset)" by eval lemma "simple_ruleset (unfold_ruleset_INPUT action.Accept example_ruleset)" by eval text\packets from the local LAN are allowed (@{const in_doubt_allow})\ lemma "approximating_bigstep_fun (common_matcher, in_doubt_allow) \p_iiface = ''eth0'', p_oiface = ''eth1'', p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (8,8,8,8), p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {TCP_SYN}, p_payload='''', p_tag_ctstate = CT_New\ (unfold_ruleset_INPUT action.Accept example_ruleset) Undecided = Decision FinalAllow" by eval text\However, they might also be rate-limited, ... (we don't know about icmp)\ lemma "approximating_bigstep_fun (common_matcher, in_doubt_deny) \p_iiface = ''eth0'', p_oiface = ''eth1'', p_src = ipv4addr_of_dotdecimal (192,168,2,45), p_dst= ipv4addr_of_dotdecimal (8,8,8,8), p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {TCP_SYN}, p_payload='''', p_tag_ctstate = CT_New\ (unfold_ruleset_INPUT action.Accept example_ruleset) Undecided = Decision FinalDeny" by eval text\But we can guarantee that packets from the outside are blocked!\ lemma "approximating_bigstep_fun (common_matcher, in_doubt_allow) \p_iiface = ''eth0'', p_oiface = ''eth1'', p_src = ipv4addr_of_dotdecimal (8,8,8,8), p_dst= 0, p_proto=TCP, p_sport=2065, p_dport=80, p_tcp_flags = {TCP_SYN}, p_payload='''', p_tag_ctstate = CT_New\ (unfold_ruleset_INPUT action.Accept example_ruleset) Undecided = Decision FinalDeny" by eval text\in doubt allow closure\ lemma upper: "upper_closure (unfold_ruleset_INPUT action.Accept example_ruleset) = [Rule (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192, 168, 0, 0)) 16))) action.Accept, Rule MatchAny action.Drop]" by eval text\in doubt deny closure\ lemma lower: "lower_closure (unfold_ruleset_INPUT action.Accept example_ruleset) = [Rule MatchAny action.Drop]" by eval text\upper closure\ lemma "rmshadow (common_matcher, in_doubt_allow) (upper_closure (unfold_ruleset_INPUT action.Accept example_ruleset)) UNIV = [Rule (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192, 168, 0, 0)) 16))) action.Accept, Rule MatchAny action.Drop]" (*<*)apply(subst upper) apply(subst rmshadow.simps) apply(simp del: rmshadow.simps) apply(simp add: Matching_Ternary.matches_def) apply(intro conjI impI) apply(rule_tac x="undefined\p_iiface := ''eth0'', p_oiface := ''eth1'', p_src := ipv4addr_of_dotdecimal (8,8,8,8), p_dst := 0, p_proto := TCP, p_sport:=2065, p_dport:=80\" in exI) apply(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def ipset_from_cidr_alt mask_def; fail) apply(rule_tac x="undefined\p_iiface := ''eth0'', p_oiface := ''eth1'', p_src := ipv4addr_of_dotdecimal (192,168,8,8), p_dst:= 0, p_proto:=TCP, p_sport:=2065, p_dport:=80\ " in exI) apply(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def ipset_from_cidr_alt mask_def; fail) done(*>*) text\lower closure\ lemma "rmshadow (common_matcher, in_doubt_deny) (lower_closure (unfold_ruleset_INPUT action.Accept example_ruleset)) UNIV = [Rule MatchAny action.Drop]" apply(subst lower) apply(subst rmshadow.simps) apply(simp del: rmshadow.simps) apply(simp add: Matching_Ternary.matches_def) done lemma "check_simple_fw_preconditions (upper_closure (unfold_ruleset_INPUT action.Accept example_ruleset))" by eval value[code] "map simple_rule_ipv4_toString (to_simple_firewall (upper_closure (unfold_ruleset_INPUT action.Accept example_ruleset)))" lemma "map simple_rule_ipv4_toString (to_simple_firewall (upper_closure (unfold_ruleset_INPUT action.Accept example_ruleset))) = [''ACCEPT all -- 192.168.0.0/16 0.0.0.0/0 '', ''DROP all -- 0.0.0.0/0 0.0.0.0/0 '']" by eval (*will break when simple_rule_ipv4_toString is changed*) lemma "check_simple_fw_preconditions (lower_closure (unfold_ruleset_INPUT action.Accept example_ruleset))" by eval value[code] "map simple_rule_ipv4_toString (to_simple_firewall (lower_closure (unfold_ruleset_INPUT action.Accept example_ruleset)))" lemma "length (unfold_ruleset_INPUT action.Accept example_ruleset) = 19" by eval text\Wow, normalization has exponential(?) blowup here.\ lemma "length (normalize_rules_dnf (unfold_ruleset_INPUT action.Accept example_ruleset)) = 259" by eval section\Synology Diskstation 2015\ text\This is a snapshot from 2015, available as \iptables-save\ format. The firewall definition and structure has changed with various firmware updates to the device. Also, the new parser also parses ports and interfaces\ parse_iptables_save ds2015_fw="iptables-save" thm ds2015_fw_def thm ds2015_fw_INPUT_default_policy_def text\this time, we don't removed the established,related rule\ value[code] "unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw)" lemma "unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw) = [Rule (\ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8'')) action.Drop, Rule (\ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST}))) action.Drop, Rule (\ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN})) MATCHAND Match (Extra ''-m limit --limit 10000/sec --limit-burst 100'')\ MATCHAND Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN}))) action.Drop, Rule (\ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN})) MATCHAND Match (Extra ''-m limit --limit 10000/sec --limit-burst 100'')\ MATCHAND \ \Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8'')) action.Drop, Rule (\ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN})) MATCHAND Match (Extra ''-m limit --limit 10000/sec --limit-burst 100'')\ MATCHAND \ \Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST}))) action.Drop, Rule (\ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth1'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN})) MATCHAND Match (Extra ''-m limit --limit 10000/sec --limit-burst 100'')\ MATCHAND \ \Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto ICMP)) MATCHAND Match (Extra ''-m icmp --icmp-type 8 -m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_RST})) MATCHAND Match (Extra ''-m limit --limit 1/sec'')\ MATCHAND \ \Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN})) MATCHAND Match (Extra ''-m limit --limit 10000/sec --limit-burst 100'')\ MATCHAND Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (L4_Flags (TCP_Flags {TCP_FIN, TCP_SYN, TCP_RST, TCP_ACK} {TCP_SYN}))) action.Drop, Rule (Match (IIface (Iface ''lo''))) action.Accept, Rule (Match (CT_State {CT_Related, CT_Established})) action.Accept, Rule (Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Dst_Ports (L4Ports TCP [(0x16, 0x16)]))) action.Drop, Rule (Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto TCP)) MATCHAND Match (Dst_Ports (L4Ports TCP [(0x15, 0x15), (0x369, 0x369), (0x138D, 0x138D), (0x138E, 0x138E), (0x50, 0x50), (0x224, 0x224), (0x6F, 0x6F), (0x37C, 0x37C), (0x801, 0x801)]))) action.Drop, Rule (Match (IIface (Iface ''eth0'')) MATCHAND Match (Prot (Proto UDP)) MATCHAND Match (Dst_Ports (L4Ports UDP [(0x7B, 0x7B), (0x6F, 0x6F), (0x37C, 0x37C), (0x801, 0x801), (0x14E9, 0x14E9)]))) action.Drop, Rule (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192, 168, 0, 0)) 16)) MATCHAND Match (IIface (Iface ''eth0''))) action.Accept, Rule (Match (IIface (Iface ''eth0''))) action.Drop, Rule MatchAny action.Accept]" by eval value[code] "map common_primitive_rule_toString (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw))" value[code] "(upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw))))" value[code] "optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw))))" value[code] "upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw)))" lemma "check_simple_fw_preconditions (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw))))))" by eval value[code] "map simple_rule_ipv4_toString (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw)))))))" lemma "simple_fw_valid (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw)))))))" by eval lemma "simple_fw_valid (to_simple_firewall (lower_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_INPUT ds2015_fw_INPUT_default_policy (map_of ds2015_fw)))))))" by eval parse_iptables_save ds2015_2_fw="iptables-save_jun_2015_cleanup" text\In 2015 there was also an update and a cleanup of the ruleset. The following should be fulfilled: Port 80 globally blocked (fulfilled, only reachable by localhost). Port 22 globally blocked (not fulfilled, error in the ruleset). Port 8080 only reachable from 192.168.0.0/24 and localhost (fulfilled). \ value[code] "unfold_ruleset_INPUT ds2015_2_fw_INPUT_default_policy (map_of ds2015_2_fw)" lemma "access_matrix_pretty_ipv4 parts_connection_ssh (to_simple_firewall_without_interfaces ipassmt_generic_ipv4 None (unfold_ruleset_INPUT ds2015_2_fw_INPUT_default_policy (map_of ds2015_2_fw))) = ([(''0.0.0.0'', ''{0.0.0.0 .. 255.255.255.255}'') ], [(''0.0.0.0'', ''0.0.0.0'')])" by eval lemma "access_matrix_pretty_ipv4 parts_connection_http (to_simple_firewall_without_interfaces ipassmt_generic_ipv4 None (unfold_ruleset_INPUT ds2015_2_fw_INPUT_default_policy (map_of ds2015_2_fw))) = ([(''0.0.0.0'', ''{0.0.0.0 .. 126.255.255.255} u {128.0.0.0 .. 255.255.255.255}''), (''127.0.0.0'', ''{127.0.0.0 .. 127.255.255.255}'') ], [(''127.0.0.0'', ''0.0.0.0''), (''127.0.0.0'', ''127.0.0.0'')])" by eval lemma "access_matrix_pretty_ipv4 (mk_parts_connection_TCP 10000 8080) (to_simple_firewall_without_interfaces ipassmt_generic_ipv4 None (unfold_ruleset_INPUT ds2015_2_fw_INPUT_default_policy (map_of ds2015_2_fw))) = ([(''127.0.0.0'', ''{127.0.0.0 .. 127.255.255.255} u {192.168.0.0 .. 192.168.255.255}''), (''0.0.0.0'', ''{0.0.0.0 .. 126.255.255.255} u {128.0.0.0 .. 192.167.255.255} u {192.169.0.0 .. 255.255.255.255}'') ], [(''127.0.0.0'', ''127.0.0.0''), (''127.0.0.0'', ''0.0.0.0'')])" by eval text\The 2016 version with IPv6 is very interesting. Some source ports for UDP are just allowed. Is this a typo? The original structure with the @{const Return}s is very complicated. Here is what is actually dropped and accepted:\ parse_ip6tables_save ds_2016_ipv6 = "ip6tables-save_jul_2016" (*5s*) lemma "map simple_rule_ipv6_toString (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_FORWARD ds_2016_ipv6_FORWARD_default_policy (map_of ds_2016_ipv6))))))) = [ ''ACCEPT all -- ::/0 ::/0 in: lo '', ''ACCEPT ipv6-icmp -- fe80::/10 ::/0 '', ''DROP tcp -- ::/0 ::/0 dports: 21'', ''DROP tcp -- ::/0 ::/0 dports: 873'', ''DROP tcp -- ::/0 ::/0 dports: 631'', ''DROP tcp -- ::/0 ::/0 dports: 515'', ''DROP tcp -- ::/0 ::/0 dports: 3260:3262'', ''DROP tcp -- ::/0 ::/0 dports: 22:23'', ''DROP tcp -- ::/0 ::/0 dports: 548'', ''DROP tcp -- ::/0 ::/0 dports: 3493'', ''DROP tcp -- ::/0 ::/0 dports: 3306'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 67:68'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 123'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 514'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 161'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 19999'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 5353'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 67:68'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 123'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 514'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 161'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 19999'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 5353'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 67:68'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 123'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 514'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 161'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 19999'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 5353'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 67:68'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 123'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 514'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 161'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 19999'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 5353'', ''DROP tcp -- ::/0 ::/0 dports: 111'', ''DROP tcp -- ::/0 ::/0 dports: 892'', ''DROP tcp -- ::/0 ::/0 dports: 2049'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 111'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 892'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 2049'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 111'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 892'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 2049'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 111'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 892'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 2049'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 111'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 892'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 2049'', ''DROP tcp -- ::/0 ::/0 dports: 0:79'', ''DROP tcp -- ::/0 ::/0 dports: 81:442'', ''DROP tcp -- ::/0 ::/0 dports: 444:9024'', ''DROP tcp -- ::/0 ::/0 dports: 9041:50000'', ''DROP tcp -- ::/0 ::/0 dports: 50003:65535'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 5003'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 sports: 0:5001 dports: 65002:65535'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 5003'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 sports: 5003 dports: 65002:65535'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 5003'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 sports: 5005:65000 dports: 65002:65535'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 5003'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 sports: 65002:65535 dports: 65002:65535'', \ \The following eth0 rules are shadowed\ ''DROP tcp -- ::/0 ::/0 in: eth0 dports: 0:79'', ''DROP tcp -- ::/0 ::/0 in: eth0 dports: 81:442'', ''DROP tcp -- ::/0 ::/0 in: eth0 dports: 444:9024'', ''DROP tcp -- ::/0 ::/0 in: eth0 dports: 9041:50000'', ''DROP tcp -- ::/0 ::/0 in: eth0 dports: 50003:65535'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 0:5001 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 0:5001 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 0:5001 dports: 5003'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 0:5001 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 0:5001 dports: 65002:65535'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5003 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5003 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5003 dports: 5003'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5003 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5003 dports: 65002:65535'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5005:65000 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5005:65000 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5005:65000 dports: 5003'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5005:65000 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 5005:65000 dports: 65002:65535'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 65002:65535 dports: 0:1899'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 65002:65535 dports: 1901:5001'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 65002:65535 dports: 5003'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 65002:65535 dports: 5005:65000'', ''DROP udp -- ::/0 ::/0 in: eth0 sports: 65002:65535 dports: 65002:65535'', ''ACCEPT all -- ::/0 ::/0 '']" by eval (*50s*) end diff --git a/thys/Iptables_Semantics/Primitive_Matchers/Parser6.thy b/thys/Iptables_Semantics/Primitive_Matchers/Parser6.thy --- a/thys/Iptables_Semantics/Primitive_Matchers/Parser6.thy +++ b/thys/Iptables_Semantics/Primitive_Matchers/Parser6.thy @@ -1,616 +1,616 @@ section\Parser for iptables-save\ theory Parser6 -imports Iptables_Semantics.Code_Interface +imports Code_Interface keywords "parse_ip6tables_save" :: thy_decl begin (*THIS IS A VERBATIM COPY OF THE IPv4 PARSER. I JUST HAVE SEARCH/REPLACED s/32/128 and s/ipv4/ipv6 AND RENAMED THE COMMAND ! ! ! do not edit by hand ! ! !*) ML\(*my personal small library*) fun takeWhile p xs = take_prefix p xs; fun dropWhile p xs = drop_prefix p xs; fun dropWhileInclusive p xs = drop 1 (dropWhile p xs) (*split at the predicate, do NOT keep the position where it was split*) fun split_at p xs = (takeWhile p xs, dropWhileInclusive p xs); \ ML_val\ split_at (fn x => x <> " ") (raw_explode "foo bar") \ section\An SML Parser for iptables-save\ text\Work in Progress\ ML\ local fun is_start_of_table table s = s = ("*"^table); fun is_end_of_table s = s = "COMMIT"; fun load_file (thy: theory) (path: string list) = let val p = File.full_path (Resources.master_directory thy) (Path.make path); val _ = "loading file "^File.platform_path p |> writeln; in if not (File.exists p) orelse (File.is_dir p) then raise Fail "File not found" else File.read_lines p end; fun extract_table _ [] = [] | extract_table table (r::rs) = if not (is_start_of_table table r) then extract_table table rs else takeWhile (fn x => not (is_end_of_table x)) rs; fun writenumloaded table_name table = let val _ = "Loaded "^ Int.toString (length table) ^" lines of the "^table_name^" table" |> writeln; in table end; fun warn_windows_line_endings lines = let val warn = fn s => if String.isSuffix "\r" s then writeln "WARNING: windows \\r\\n line ending detected" else () val _ = map warn lines in lines end; in fun load_table table thy = load_file thy #> warn_windows_line_endings #> extract_table table #> writenumloaded table; val load_filter_table = load_table "filter"; end; \ ML\ (*keep quoted strings as one token*) local fun collapse_quotes [] = [] | collapse_quotes ("\""::ss) = let val (quoted, rest) = split_at (fn x => x <> "\"") ss in "\"" ^ implode quoted^"\"" :: rest end | collapse_quotes (s::ss) = s :: collapse_quotes ss; in val ipt_explode = raw_explode #> collapse_quotes; end \ ML_val\ ipt_explode "ad \"as das\" boo"; ipt_explode "ad \"foobar --boo boo"; ipt_explode "ent \"\\\"\" this"; ipt_explode ""; \ (* ML_val\ fun finite_scan scan = Scan.error (Scan.finite Symbol.stopper (scan)); finite_scan ((Scan.this_string "foo") --| (Scan.ahead ($$ " " || Scan.one Symbol.is_eof))) (raw_explode "foo "); \ ML\ local val errormsg = (fn (ss, _) => raise Fail ("parse error: expected word boundary near `"^implode ss^"'")) fun finite_scan scanner = (Scan.finite Symbol.stopper (Scan.error (!! errormsg scanner))); val word_boundary_or_end = Scan.ahead ($$ " " || Scan.one Symbol.is_eof) in fun look_ahead_token (scan : (string list -> 'a * string list)) s = (*TODO: why do I need to write the type?*) finite_scan (scan --| word_boundary_or_end) s; end; val _ = look_ahead_token (Scan.this_string "foo") (raw_explode "foo "); val _ = look_ahead_token (Scan.this_string "foo") (raw_explode "foo"); val _ = (look_ahead_token (Scan.this_string "foo")) (raw_explode "fo") handle Fail m => if m = "parse error: expected word boundary near `fo'" then ("", []) else raise Fail "foo"; \*) ML\ datatype parsed_action_type = TypeCall | TypeGoto datatype parsed_match_action = ParsedMatch of term | ParsedNegatedMatch of term | ParsedAction of parsed_action_type * string; local (*iptables-save parsers*) val is_whitespace = Scan.many (fn x => x = " "); local (*parser for matches*) local fun extract_int ss = case ss |> implode |> Int.fromString of SOME i => i | NONE => raise Fail "unparsable int"; fun is_iface_char x = Symbol.is_ascii x andalso (Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "+" orelse x = "*" orelse x = "." orelse x = "-") in fun mk_nat maxval i = if i < 0 orelse i > maxval then raise Fail("nat ("^Int.toString i^") must be between 0 and "^Int.toString maxval) else (HOLogic.mk_number HOLogic.natT i); fun ipNetmask_to_hol (ip,len) = @{const IpAddrNetmask (128)} $ mk_ipv6addr ip $ mk_nat 128 len; fun ipRange_to_hol (ip1,ip2) = @{const IpAddrRange (128)} $ mk_ipv6addr ip1 $ mk_ipv6addr ip2; val parser_ip_cidr = parser_ipv6 --| ($$ "/") -- (Scan.many1 Symbol.is_ascii_digit >> extract_int) >> ipNetmask_to_hol; val parser_ip_range = parser_ipv6 --| ($$ "-") -- parser_ipv6 >> ipRange_to_hol; val parser_ip_addr = parser_ipv6 >> (fn ip => @{const IpAddr (128)} $ mk_ipv6addr ip); val parser_interface = Scan.many1 is_iface_char >> (implode #> (fn x => @{const Iface} $ HOLogic.mk_string x)); (*TODO: it would be cool to check for a word boundary after all these strings*) val parser_protocol = Scan.this_string "tcp" >> K @{term "TCP :: 8 word"} || Scan.this_string "udp" >> K @{term "UDP :: 8 word"} || (Scan.this_string "icmpv6" (*before icmp*) || Scan.this_string "ipv6-icmp") >> K @{term "L4_Protocol.IPv6ICMP"} || Scan.this_string "icmp" >> K @{term "ICMP :: 8 word"} (*Moar Assigned Internet Protocol Numbers below: *) || Scan.this_string "esp" >> K @{term "L4_Protocol.ESP"} || Scan.this_string "ah" >> K @{term "L4_Protocol.AH"} || Scan.this_string "gre" >> K @{term "L4_Protocol.GRE"} val parser_ctstate = Scan.this_string "NEW" >> K @{const CT_New} || Scan.this_string "ESTABLISHED" >> K @{const CT_Established} || Scan.this_string "RELATED" >> K @{const CT_Related} || Scan.this_string "UNTRACKED" >> K @{const CT_Untracked} || Scan.this_string "INVALID" >> K @{const CT_Invalid} val parser_tcp_flag = Scan.this_string "SYN" >> K @{const TCP_SYN} || Scan.this_string "ACK" >> K @{const TCP_ACK} || Scan.this_string "FIN" >> K @{const TCP_FIN} || Scan.this_string "RST" >> K @{const TCP_RST} || Scan.this_string "URG" >> K @{const TCP_URG} || Scan.this_string "PSH" >> K @{const TCP_PSH} fun parse_comma_separated_list parser = Scan.repeat (parser --| $$ ",") @@@ (parser >> (fn p => [p])) local val mk_port_single = mk_nat 65535 #> (fn n => @{const nat_to_16word} $ n) val parse_port_raw = Scan.many1 Symbol.is_ascii_digit >> extract_int fun port_tuple_warn (p1,p2) = if p1 >= p2 then let val _= writeln ("WARNING (in ports): "^Int.toString p1^" >= "^Int.toString p2) in (p1, p2) end else (p1, p2); in val parser_port_single_tup = ( (parse_port_raw --| $$ ":" -- parse_port_raw) >> (port_tuple_warn #> (fn (p1,p2) => (mk_port_single p1, mk_port_single p2))) || (parse_port_raw >> (fn p => (mk_port_single p, mk_port_single p))) ) >> HOLogic.mk_prod end val parser_port_single_tup_term = parser_port_single_tup >> (fn x => @{term "L4Ports 0"} $ HOLogic.mk_list @{typ "16 word \ 16 word"} [x]) val parser_port_many1_tup = parse_comma_separated_list parser_port_single_tup >> (fn x => @{term "L4Ports 0"} $ HOLogic.mk_list @{typ "16 word \ 16 word"} x) val parser_ctstate_set = parse_comma_separated_list parser_ctstate >> HOLogic.mk_set @{typ "ctstate"} val parser_tcp_flag_set = parse_comma_separated_list parser_tcp_flag >> HOLogic.mk_set @{typ "tcp_flag"} val parser_tcp_flags = (parser_tcp_flag_set --| $$ " " -- parser_tcp_flag_set) >> (fn (m,c) => @{const TCP_Flags} $ m $ c) val parser_extra = Scan.many1 (fn x => x <> " " andalso Symbol.not_eof x) >> (implode #> HOLogic.mk_string); end; val eoo = Scan.ahead ($$ " " || Scan.one Symbol.is_eof); (*end of option; word boundary or eof look-ahead*) fun parse_cmd_option_generic (d: term -> parsed_match_action) s t (parser: string list -> (term * string list)) = Scan.finite Symbol.stopper (is_whitespace |-- Scan.this_string s |-- (parser >> (fn r => d (t $ r))) --| eoo) fun parse_cmd_option (s: string) (t: term) (parser: string list -> (term * string list)) = parse_cmd_option_generic ParsedMatch s t parser; (*both negated and not negated primitives*) fun parse_cmd_option_negated (s: string) (t: term) (parser: string list -> (term * string list)) = parse_cmd_option_generic ParsedNegatedMatch ("! "^s) t parser || parse_cmd_option s t parser; fun parse_cmd_option_negated_singleton s t parser = parse_cmd_option_negated s t parser >> (fn x => [x]) (*TODO: is the 'Scan.finite Symbol.stopper' correct here?*) (*TODO: eoo here?*) fun parse_with_module_prefix (module: string) (parser: (string list -> parsed_match_action * string list)) = (Scan.finite Symbol.stopper (is_whitespace |-- Scan.this_string module)) |-- (Scan.repeat parser) in val parse_ips = parse_cmd_option_negated_singleton "-s " @{const Src (128)} (parser_ip_cidr || parser_ip_addr) || parse_cmd_option_negated_singleton "-d " @{const Dst (128)} (parser_ip_cidr || parser_ip_addr); val parse_iprange = parse_with_module_prefix "-m iprange " ( parse_cmd_option_negated "--src-range " @{const Src (128)} parser_ip_range || parse_cmd_option_negated "--dst-range " @{const Dst (128)} parser_ip_range); val parse_iface = parse_cmd_option_negated_singleton "-i " @{const IIface (128)} parser_interface || parse_cmd_option_negated_singleton "-o " @{const OIface (128)} parser_interface; (*TODO type is explicit here*) val parse_protocol = parse_cmd_option_negated_singleton "-p " @{term "(Prot \ Proto) :: primitive_protocol \ 128 common_primitive"} parser_protocol; (*negated?*) (*-m tcp requires that there is already an -p tcp, iptables checks that for you, we assume valid iptables-save (otherwise the kernel would not load it) We will fill the protocols in the L4Ports later*) val parse_tcp_options = parse_with_module_prefix "-m tcp " ( parse_cmd_option_negated "--sport " @{const Src_Ports (128)} parser_port_single_tup_term || parse_cmd_option_negated "--dport " @{const Dst_Ports (128)} parser_port_single_tup_term || parse_cmd_option_negated "--tcp-flags " @{const L4_Flags (128)} parser_tcp_flags); val parse_multiports = parse_with_module_prefix "-m multiport " ( parse_cmd_option_negated "--sports " @{const Src_Ports (128)} parser_port_many1_tup || parse_cmd_option_negated "--dports " @{const Dst_Ports (128)} parser_port_many1_tup || parse_cmd_option_negated "--ports " @{const MultiportPorts (32)} parser_port_many1_tup); val parse_udp_options = parse_with_module_prefix "-m udp " ( parse_cmd_option_negated "--sport " @{const Src_Ports (128)} parser_port_single_tup_term || parse_cmd_option_negated "--dport " @{const Dst_Ports (128)} parser_port_single_tup_term); val parse_ctstate = parse_with_module_prefix "-m state " (parse_cmd_option_negated "--state " @{const CT_State (128)} parser_ctstate_set) || parse_with_module_prefix "-m conntrack " (parse_cmd_option_negated "--ctstate " @{const CT_State (128)} parser_ctstate_set); (*TODO: it would be good to fail if there is a "!" in the extra; it might be an unparsed negation*) val parse_unknown = (parse_cmd_option "" @{const Extra (128)} parser_extra) >> (fn x => [x]); end; local (*parser for target/action*) fun is_target_char x = Symbol.is_ascii x andalso (Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "-" orelse x = "_" orelse x = "~") fun parse_finite_skipwhite parser = Scan.finite Symbol.stopper (is_whitespace |-- parser); val is_icmp_type = fn x => Symbol.is_ascii_letter x orelse x = "-" orelse x = "6" in val parser_target = Scan.many1 is_target_char >> implode; (*parses: -j MY_CUSTOM_CHAIN*) (*The -j may not be the end of the line. example: -j LOG --log-prefix "[IPT_DROP]:"*) val parse_target_generic : (string list -> parsed_match_action * string list) = parse_finite_skipwhite (Scan.this_string "-j " |-- (parser_target >> (fn s => ParsedAction (TypeCall, s)))); (*parses: REJECT --reject-with type*) val parse_target_reject : (string list -> parsed_match_action * string list) = parse_finite_skipwhite (Scan.this_string "-j " |-- (Scan.this_string "REJECT" >> (fn s => ParsedAction (TypeCall, s))) --| ((Scan.this_string " --reject-with " --| Scan.many1 is_icmp_type) || Scan.this_string "")); val parse_target_goto : (string list -> parsed_match_action * string list) = parse_finite_skipwhite (Scan.this_string "-g " |-- (parser_target >> (fn s => let val _ = writeln ("WARNING: goto in `"^s^"'") in ParsedAction (TypeGoto, s) end))); val parse_target : (string list -> parsed_match_action * string list) = parse_target_reject || parse_target_goto || parse_target_generic; end; in (*parses: -A FORWARD*) val parse_table_append : (string list -> (string * string list)) = Scan.this_string "-A " |-- parser_target --| is_whitespace; (*parses: -s 0.31.123.213/88 --foo_bar -j chain --foobar First tries to parse a known field, afterwards, it parses something unknown until a blank space appears *) val option_parser : (string list -> (parsed_match_action list) * string list) = Scan.recover (parse_ips || parse_iprange || parse_iface || parse_protocol || parse_tcp_options || parse_udp_options || parse_multiports || parse_ctstate || parse_target >> (fn x => [x])) (K parse_unknown); (*parse_table_append should be called before option_parser, otherwise -A will simply be an unknown for option_parser*) local (*:DOS_PROTECT - [0:0]*) val custom_chain_decl_parser = ($$ ":") |-- parser_target --| Scan.this_string " - " #> fst; (*:INPUT ACCEPT [130:12050]*) (*TODO: PREROUTING is only valid if we are in the raw table*) val builtin_chain_decl_parser = ($$ ":") |-- (Scan.this_string "INPUT" || Scan.this_string "FORWARD" || Scan.this_string "OUTPUT" || Scan.this_string "PREROUTING") --| ($$ " ") -- (Scan.this_string "ACCEPT" || Scan.this_string "DROP") --| ($$ " ") #> fst; val wrap_builtin_chain = (fn (name, policy) => (name, SOME policy)); val wrap_custom_chain = (fn name => (name, NONE)); in val chain_decl_parser : (string list -> string * string option) = Scan.recover (builtin_chain_decl_parser #> wrap_builtin_chain) (K (custom_chain_decl_parser #> wrap_custom_chain)); end end; \ (*TODO: is there a library function for this?*) ML\ local fun concat [] = [] | concat (x :: xs) = x @ concat xs; in fun Scan_cons_repeat (parser: ('a -> 'b list * 'a)) (s: 'a) : ('b list * 'a) = let val (x, rest) = Scan.repeat parser s in (concat x, rest) end; end \ ML_val\(Scan_cons_repeat option_parser) (ipt_explode "-i lup -j net-fw")\ ML_val\(Scan_cons_repeat option_parser) (ipt_explode "")\ ML_val\(Scan_cons_repeat option_parser) (ipt_explode "-i lup foo")\ ML_val\(Scan_cons_repeat option_parser) (ipt_explode "-m tcp --dport 22 --sport 88")\ ML_val\(Scan_cons_repeat option_parser) (ipt_explode "-j LOG --log-prefix \"Shorewall:INPUT:REJECT:\" --log-level 6")\ ML_val\ val (x, rest) = (Scan_cons_repeat option_parser) (ipt_explode "-d 0.31.123.213/11. --foo_bar \"he he\" -f -i eth0+ -s 0.31.123.213/21 moreextra -j foobar --log"); map (fn p => case p of ParsedMatch t => type_of t | ParsedAction (_,_) => dummyT) x; map (fn p => case p of ParsedMatch t => Pretty.writeln (Syntax.pretty_term @{context} t) | ParsedAction (_,a) => writeln ("action: "^a)) x; \ ML\ local fun parse_rule_options (s: string list) : parsed_match_action list = let val (parsed, rest) = (case try (Scan.catch (Scan_cons_repeat option_parser)) s of SOME x => x | NONE => raise Fail "scanning") in if rest <> [] then raise Fail ("Unparsed: `"^implode rest^"'") else parsed end handle Fail m => raise Fail ("parse_rule_options: "^m^" for rule `"^implode s^"'"); fun get_target (ps : parsed_match_action list) : (parsed_action_type * string) option = let val actions = List.mapPartial (fn p => case p of ParsedAction a => SOME a | _ => NONE) ps in case actions of [] => NONE | [action] => SOME action | _ => raise Fail "there can be at most one target" end; val get_matches : (parsed_match_action list -> term) = List.mapPartial (fn p => case p of ParsedMatch m => SOME (@{const Pos ("128 common_primitive")} $ m) | ParsedNegatedMatch m => SOME (@{const Neg ("128 common_primitive")} $ m) | ParsedAction _ => NONE) #> HOLogic.mk_list @{typ "128 common_primitive negation_type"}; (*returns: (chainname the rule was appended to, target, matches)*) fun parse_rule (s: string) : (string * (parsed_action_type * string) option * term) = let val (chainname, rest) = (case try (ipt_explode #> Scan.finite Symbol.stopper parse_table_append) s of SOME x => x | NONE => raise Fail ("parse_rule: parse_table_append: "^s)); val parsed = parse_rule_options rest in (chainname, get_target parsed, get_matches parsed) end; in (*returns (parsed chain declarations, parsed appended rules*) fun rule_type_partition (rs : string list) : ((string * string option) list * (string * (parsed_action_type * string) option * term) list) = let val (chain_decl, rules) = List.partition (String.isPrefix ":") rs in if not (List.all (String.isPrefix "-A") rules) then raise Fail "could not partition rules" else let val parsed_chain_decls = (case try (map (ipt_explode #> chain_decl_parser)) chain_decl of SOME x => x | NONE => raise Fail ("could not parse chain declarations: "^implode chain_decl)); val parsed_rules = map parse_rule rules; val _ = "Parsed "^ Int.toString (length parsed_chain_decls) ^" chain declarations" |> writeln; val _ = "Parsed "^ Int.toString (length parsed_rules) ^" rules" |> writeln; in (parsed_chain_decls, parsed_rules) end end fun get_chain_decls_policy (ls: ((string * string option) list * (string * (parsed_action_type * string) option * term) list)) = fst ls fun get_parsed_rules (ls: ((string * string option) list * (string * (parsed_action_type * string) option * term) list)) = snd ls val filter_chain_decls_names_only : ((string * string option) list * (string * (parsed_action_type * string) option * term) list) -> (string list * (string * (parsed_action_type * string) option * term) list) = (fn (a,b) => (map fst a, b)) end; \ ML\(*create a table with the firewall definition*) structure FirewallTable = Table(type key = string; val ord = Library.string_ord); type firewall_table = term list FirewallTable.table; local (* Initialize the table. Create a key for every declared chain. *) fun FirewallTable_init chain_decls : firewall_table = FirewallTable.empty |> fold (fn entry => fn accu => FirewallTable.update_new (entry, []) accu) chain_decls; (* this takes like forever! *) (* apply compress_parsed_extra here?*) fun hacky_hack t = (*Code_Evaluation.dynamic_value_strict @{context} (@{const compress_extra} $ t)*) @{const alist_and' ("128 common_primitive")} $ (@{const fill_l4_protocol (128)} $ (@{const compress_parsed_extra (128)} $ t)) fun mk_MatchExpr t = if fastype_of t <> @{typ "128 common_primitive negation_type list"} then raise Fail "Type Error" else hacky_hack t; fun mk_Rule_help t a = let val r = @{const Rule ("128 common_primitive")} $ (mk_MatchExpr t) $ a in if fastype_of r <> @{typ "128 common_primitive rule"} then raise Fail "Type error in mk_Rule_help" else r end; fun append table chain rule = case FirewallTable.lookup table chain of NONE => raise Fail ("uninitialized cahin: "^chain) | SOME rules => FirewallTable.update (chain, rules@[rule]) table fun mk_Rule (tbl: firewall_table) (chain: string, target : (parsed_action_type * string) option, t : term) = if not (FirewallTable.defined tbl chain) then raise Fail ("undefined chain to be appended: "^chain) else case target of NONE => mk_Rule_help t @{const action.Empty} | SOME (TypeCall, "ACCEPT") => mk_Rule_help t @{const action.Accept} | SOME (TypeCall, "DROP") => mk_Rule_help t @{const action.Drop} | SOME (TypeCall, "REJECT") => mk_Rule_help t @{const action.Reject} | SOME (TypeCall, "LOG") => mk_Rule_help t @{const action.Log} | SOME (TypeCall, "RETURN") => mk_Rule_help t @{const action.Return} | SOME (TypeCall, custom) => if not (FirewallTable.defined tbl custom) then raise Fail ("unknown action: "^custom) else mk_Rule_help t (@{const action.Call} $ HOLogic.mk_string custom) | SOME (TypeGoto, "ACCEPT") => raise Fail "Unexpected" | SOME (TypeGoto, "DROP") => raise Fail "Unexpected" | SOME (TypeGoto, "REJECT") => raise Fail "Unexpected" | SOME (TypeGoto, "LOG") => raise Fail "Unexpected" | SOME (TypeGoto, "RETURN") => raise Fail "Unexpected" | SOME (TypeGoto, custom) => if not (FirewallTable.defined tbl custom) then raise Fail ("unknown action: "^custom) else mk_Rule_help t (@{const action.Goto} $ HOLogic.mk_string custom); (*val init = FirewallTable_init parsed_chain_decls;*) (*map type_of (map (mk_Rule init) parsed_rules);*) in local fun append_rule (tbl: firewall_table) (chain: string, target : (parsed_action_type * string) option, t : term) = append tbl chain (mk_Rule tbl (chain, target, t)) in fun make_firewall_table (parsed_chain_decls : string list, parsed_rules : (string * (parsed_action_type * string) option * term) list) = fold (fn rule => fn accu => append_rule accu rule) parsed_rules (FirewallTable_init parsed_chain_decls); end end \ ML\ fun mk_Ruleset (tbl: firewall_table) = FirewallTable.dest tbl |> map (fn (k,v) => HOLogic.mk_prod (HOLogic.mk_string k, HOLogic.mk_list @{typ "128 common_primitive rule"} v)) |> HOLogic.mk_list @{typ "string \ 128 common_primitive rule list"} \ (*default policies*) ML\ local fun default_policy_action_to_term "ACCEPT" = @{const "action.Accept"} | default_policy_action_to_term "DROP" = @{const "action.Drop"} | default_policy_action_to_term a = raise Fail ("Not a valid default policy `"^a^"'") in (*chain_name * default_policy*) fun preparedefault_policies [] = [] | preparedefault_policies ((chain_name, SOME default_policy)::ls) = (chain_name, default_policy_action_to_term default_policy) :: preparedefault_policies ls | preparedefault_policies ((_, NONE)::ls) = preparedefault_policies ls end \ ML\ fun trace_timing (printstr : string) (f : 'a -> 'b) (a : 'a) : 'b = let val t0 = Time.now(); in let val result = f a; in let val t1= Time.now(); in let val _ = writeln(String.concat [printstr^" (", Time.toString(Time.-(t1,t0)), " seconds)"]) in result end end end end; fun simplify_code ctxt = let val _ = writeln "unfolding (this may take a while) ..." in trace_timing "Simplified term" (Code_Evaluation.dynamic_value_strict ctxt) end fun certify_term ctxt t = trace_timing "Certified term" (Thm.cterm_of ctxt) t \ ML_val\(*Example: putting it all together*) fun parse_iptables_save_global thy (file: string list) : term = load_filter_table thy file |> rule_type_partition |> filter_chain_decls_names_only |> make_firewall_table |> mk_Ruleset |> simplify_code @{context} (* val example = parse_iptables_save @{theory} ["Parser_Test", "data", "iptables-save"]; Pretty.writeln (Syntax.pretty_term @{context} example);*) \ ML\ local fun define_const t name lthy = let val binding_name = Thm.def_binding name val _ = writeln ("Defining constant `" ^ Binding.name_of binding_name ^ "'"); in lthy (*without Proof_Context.set_stmt, there is an ML stack overflow for large iptables-save dumps*) (*Debugged by Makarius, Isabelle2016*) |> Proof_Context.set_stmt false (* FIXME workaround "context begin" oddity *) |> Local_Theory.define ((name, NoSyn), ((binding_name, @{attributes [code]}), t)) |> #2 end; fun print_default_policies (ps: (string * term) list) = let val _ = ps |> map (fn (name, _) => if name <> "INPUT" andalso name <> "FORWARD" andalso name <> "OUTPUT" then writeln ("WARNING: the chain `"^name^"' is not a built-in chain of the filter table") else ()) in ps end; fun sanity_check_ruleset ctxt t = let val check = Code_Evaluation.dynamic_value_strict ctxt (@{const sanity_wf_ruleset ("128 common_primitive")} $ t) in if check <> @{term "True"} then raise ERROR "sanity_wf_ruleset failed" else t end; in fun parse_iptables_save table name path lthy = let val prepared = path |> load_table table (Proof_Context.theory_of lthy) |> rule_type_partition val firewall = prepared |> filter_chain_decls_names_only |> make_firewall_table |> mk_Ruleset (*this may a while*) |> simplify_code lthy (*was: @{context} (*TODO: is this correct here?*)*) |> trace_timing "checked sanity with sanity_wf_ruleset" (sanity_check_ruleset lthy) val default_policis = prepared |> get_chain_decls_policy |> preparedefault_policies |> print_default_policies in lthy |> define_const firewall name |> fold (fn (chain_name, policy) => define_const policy (Binding.name (Binding.name_of name ^ "_" ^ chain_name ^ "_default_policy"))) default_policis end end \ ML\ Outer_Syntax.local_theory @{command_keyword parse_ip6tables_save} "load a file generated by iptables-save and make the firewall definition available as isabelle term" (Parse.binding --| @{keyword "="} -- Scan.repeat1 Parse.path >> (fn (binding, paths) => parse_iptables_save "filter" binding paths)) \ end diff --git a/thys/Iptables_Semantics/ROOT b/thys/Iptables_Semantics/ROOT --- a/thys/Iptables_Semantics/ROOT +++ b/thys/Iptables_Semantics/ROOT @@ -1,74 +1,95 @@ chapter AFP session Iptables_Semantics (AFP) = Routing + options [timeout = 1200] sessions Native_Word + directories + "Common" + "Semantics_Ternary" + "Primitive_Matchers" + "Simple_Firewall" theories [document = false] "Common/List_Misc" "Common/WordInterval_Lists" theories Semantics - "Examples/Example_Semantics" + Example_Semantics Alternative_Semantics Semantics_Stateful Semantics_Goto Call_Return_Unfolding "Common/Negation_Type_DNF" "Semantics_Ternary/Semantics_Ternary" Matching_Embeddings Semantics_Embeddings Iptables_Semantics Semantics_Stateful "Semantics_Ternary/Optimizing" "Primitive_Matchers/No_Spoof" + "Primitive_Matchers/Parser6" No_Spoof_Embeddings "Primitive_Matchers/Routing_IpAssmt" "Primitive_Matchers/Transform" "Primitive_Matchers/Primitive_Abstract" "Primitive_Matchers/Code_Interface" "Primitive_Matchers/Parser" "Simple_Firewall/SimpleFw_Compliance" - "Examples/Code_haskell" + Code_haskell Access_Matrix_Embeddings No_Spoof_Embeddings Documentation document_files "root.tex" "root.bib" "mathpartir.sty" session Iptables_Semantics_Examples (AFP) in "Examples" = Iptables_Semantics + options [timeout = 2400] + directories + "Parser_Test" + "Fail" + "Contrived" + "Synology_Diskstation_DS414" + "Ringofsaturn_com" + "SQRL_Shorewall" + "sns.ias.edu" + "medium-sized-company" theories "Parser_Test/Parser_Test" "Parser_Test/Parser6_Test" "Small_Examples" "Fail/Ports_Fail" "Contrived/Contrived_Example" "Synology_Diskstation_DS414/Analyze_Synology_Diskstation" "Ringofsaturn_com/Analyze_Ringofsaturn_com" "SQRL_Shorewall/Analyze_SQRL_Shorewall" "SQRL_Shorewall/SQRL_2015_nospoof" "sns.ias.edu/SNS_IAS_Eduroam_Spoofing" "medium-sized-company/Analyze_medium_sized_company" document_files (in "../document") "root.tex" "root.bib" "mathpartir.sty" session Iptables_Semantics_Examples_Big (AFP slow very_slow) in "Examples_Big" = Iptables_Semantics_Examples + - directories "../Examples" (overlapping) options [timeout = 60000] + directories + "../Examples/topoS_generated" + "../Examples/IPPartEval" + "../Examples/TUM_Net_Firewall" + "../Examples/containern" + "../Examples/TUM_Net_Firewall" + "../Examples/IPPartEval" theories "../Examples/topoS_generated/Analyze_topos_generated" "../Examples/IPPartEval/IP_Address_Space_Examples_All_Small" "../Examples/TUM_Net_Firewall/Analyze_TUM_Net_Firewall" "../Examples/containern/Analyze_Containern" "../Examples/TUM_Net_Firewall/TUM_Spoofing_new3" "../Examples/TUM_Net_Firewall/TUM_Simple_FW" "../Examples/IPPartEval/IP_Address_Space_Examples_All_Large" document_files (in "../document") "root.tex" "root.bib" "mathpartir.sty"