From 1c8a80b10f7661c33018112a534499e5401a4d4f Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:18:47 -0400 Subject: [PATCH 01/87] spelling: absence Signed-off-by: Josh Soref --- thy/LOFT/OpenFlow_Documentation.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/OpenFlow_Documentation.thy b/thy/LOFT/OpenFlow_Documentation.thy index ea00a6b6..3d3a2c10 100644 --- a/thy/LOFT/OpenFlow_Documentation.thy +++ b/thy/LOFT/OpenFlow_Documentation.thy @@ -314,7 +314,7 @@ We could have made this definition on sets but chose not to for consistency.}: The use of @{term Undefined} immediately raises the question in which condition it cannot occur. We give the following definition:\ lemma "check_no_overlap \ ft = (\a \ set ft. \b \ set ft. (a \ b \ ofe_prio a = ofe_prio b) \ \(\p. \ (ofe_fields a) p \ \ (ofe_fields b) p))" unfolding check_no_overlap_alt check_no_overlap2_def by force -text\Together with distinctness of the flow table, this provides the abscence of @{term Undefined}\footnote{It is slightly stronger than necessary, overlapping rules might be shadowed and thus never influence the behavior.}:\ +text\Together with distinctness of the flow table, this provides the absence of @{term Undefined}\footnote{It is slightly stronger than necessary, overlapping rules might be shadowed and thus never influence the behavior.}:\ lemma "\check_no_overlap \ ft; distinct ft\ \ OF_priority_match \ ft p \ Undefined" by (simp add: no_overlapsI no_overlaps_not_unefined) From 3fec7634715cad2cad206b8ff6adee957302ae4a Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:18:49 -0400 Subject: [PATCH 02/87] spelling: accidentally Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy b/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy index 607dd79b..9d7b0651 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy @@ -717,7 +717,7 @@ text\Examples\ \ lemma "\ no_spoofing TYPE('pkt_ext) [Iface ''eth0'' \ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]] - [Rule (MatchNot (Match (IIface (Iface ''wlan+'')))) action.Accept, (*accidently allow everything for eth0*) + [Rule (MatchNot (Match (IIface (Iface ''wlan+'')))) action.Accept, (*accidentally allow everything for eth0*) Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0'')))) action.Drop, Rule MatchAny action.Accept] " @@ -739,7 +739,7 @@ text\Examples\ lemma "\ no_spoofing_iface (Iface ''eth0'') [Iface ''eth0'' \ [(ipv4addr_of_dotdecimal (192,168,0,0), 24)]] - [Rule (MatchNot (Match (IIface (Iface ''wlan+'')))) action.Accept, (*accidently allow everything for eth0*) + [Rule (MatchNot (Match (IIface (Iface ''wlan+'')))) action.Accept, (*accidentally allow everything for eth0*) Rule (MatchAnd (MatchNot (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24)))) (Match (IIface (Iface ''eth0'')))) action.Drop, Rule MatchAny action.Accept] " by eval From c4a4c2855059bafaf47752002b277c33526b28aa Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:18:51 -0400 Subject: [PATCH 03/87] spelling: according Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Semantics_Stateful.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Semantics_Stateful.thy b/thy/Iptables_Semantics/Semantics_Stateful.thy index f7f9e715..1a873a0a 100644 --- a/thy/Iptables_Semantics/Semantics_Stateful.thy +++ b/thy/Iptables_Semantics/Semantics_Stateful.thy @@ -58,7 +58,7 @@ text\In this model, the matcher is completely stateless but packets are pr inductive semantics_stateful_packet_tagging :: "'a ruleset \ ('a, 'ptagged) matcher \ - ('\ \ 'p \ 'ptagged) \ (*taggs the packet accordig to the current state before processing by firewall*) + ('\ \ 'p \ 'ptagged) \ (*taggs the packet according to the current state before processing by firewall*) ('\ \ final_decision \ 'p \ '\) \ (*state updater*) '\ \ (*Starting state. constant*) (string \ action) \ From e4315feffb9423af9711b44eef02a815fee0536c Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:18:54 -0400 Subject: [PATCH 04/87] spelling: address Signed-off-by: Josh Soref --- thy/IP_Addresses/IPv4.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/IP_Addresses/IPv4.thy b/thy/IP_Addresses/IPv4.thy index db3875e1..210870e6 100644 --- a/thy/IP_Addresses/IPv4.thy +++ b/thy/IP_Addresses/IPv4.thy @@ -18,7 +18,7 @@ section \IPv4 Adresses\ definition ipv4addr_of_nat :: "nat \ ipv4addr" where "ipv4addr_of_nat n = of_nat n" - text\The maximum IPv4 addres\ + text\The maximum IPv4 address\ definition max_ipv4_addr :: "ipv4addr" where "max_ipv4_addr \ ipv4addr_of_nat ((2^32) - 1)" From 73dfffc6bb23c699662605de35d58379653a3ee4 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:18:57 -0400 Subject: [PATCH 05/87] spelling: addresses Signed-off-by: Josh Soref --- thy/IP_Addresses/IP_Address.thy | 2 +- thy/IP_Addresses/IPv4.thy | 6 +++--- thy/IP_Addresses/IPv6.thy | 4 ++-- thy/LOFT/OpenFlow_Documentation.thy | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/thy/IP_Addresses/IP_Address.thy b/thy/IP_Addresses/IP_Address.thy index 9bd21a89..3f810cbe 100644 --- a/thy/IP_Addresses/IP_Address.thy +++ b/thy/IP_Addresses/IP_Address.thy @@ -7,7 +7,7 @@ imports Word_More WordInterval begin -section \Modelling IP Adresses\ +section \Modelling IP Addresses\ text\An IP address is basically an unsigned integer. We model IP addresses of arbitrary lengths. diff --git a/thy/IP_Addresses/IPv4.thy b/thy/IP_Addresses/IPv4.thy index 210870e6..6fd4c244 100644 --- a/thy/IP_Addresses/IPv4.thy +++ b/thy/IP_Addresses/IPv4.thy @@ -8,11 +8,11 @@ imports IP_Address begin -section \IPv4 Adresses\ +section \IPv4 Addresses\ text\An IPv4 address is basically a 32 bit unsigned integer.\ type_synonym ipv4addr = "32 word" - text\Conversion between natural numbers and IPv4 adresses\ + text\Conversion between natural numbers and IPv4 addresses\ definition nat_of_ipv4addr :: "ipv4addr \ nat" where "nat_of_ipv4addr a = unat a" definition ipv4addr_of_nat :: "nat \ ipv4addr" where @@ -42,7 +42,7 @@ section \IPv4 Adresses\ lemma ipv4addr_of_nat_nat_of_ipv4addr: "ipv4addr_of_nat (nat_of_ipv4addr addr) = addr" by(simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def) -subsection\Representing IPv4 Adresses (Syntax)\ +subsection\Representing IPv4 Addresses (Syntax)\ fun ipv4addr_of_dotdecimal :: "nat \ nat \ nat \ nat \ ipv4addr" where "ipv4addr_of_dotdecimal (a,b,c,d) = ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a )" diff --git a/thy/IP_Addresses/IPv6.thy b/thy/IP_Addresses/IPv6.thy index 5189e4fe..ab756ab3 100644 --- a/thy/IP_Addresses/IPv6.thy +++ b/thy/IP_Addresses/IPv6.thy @@ -12,7 +12,7 @@ section \IPv6 Addresses\ text\An IPv6 address is basically a 128 bit unsigned integer. RFC 4291, Section 2.\ type_synonym ipv6addr = "128 word" - text\Conversion between natural numbers and IPv6 adresses\ + text\Conversion between natural numbers and IPv6 addresses\ definition nat_of_ipv6addr :: "ipv6addr \ nat" where "nat_of_ipv6addr a = unat a" definition ipv6addr_of_nat :: "nat \ ipv6addr" where @@ -45,7 +45,7 @@ section \IPv6 Addresses\ lemma ipv6addr_of_nat_nat_of_ipv6addr: "ipv6addr_of_nat (nat_of_ipv6addr addr) = addr" by(simp add: ipv6addr_of_nat_def nat_of_ipv6addr_def) -subsection\Syntax of IPv6 Adresses\ +subsection\Syntax of IPv6 Addresses\ text\RFC 4291, Section 2.2.: Text Representation of Addresses\ text\Quoting the RFC (note: errata exists):\ diff --git a/thy/LOFT/OpenFlow_Documentation.thy b/thy/LOFT/OpenFlow_Documentation.thy index 3d3a2c10..747d0a7f 100644 --- a/thy/LOFT/OpenFlow_Documentation.thy +++ b/thy/LOFT/OpenFlow_Documentation.thy @@ -211,7 +211,7 @@ schematic_goal "(field_match :: of_match_field) \ { L4Dst (?pd :: 16 word) (?md :: 16 word) }" by(fact of_match_field_typeset) text\ -Two things are worth additional mention: L3 and L4 ``addressess''. +Two things are worth additional mention: L3 and L4 ``addresses''. The @{term IPv4Src} and @{term IPv4Dst} matches are specified as ``can be subnet masked'' in~\cite{specification10}, whereras~\cite{specification15} states clearly that arbitrary bitmasks can be used. We took the conservative approach here. Our alteration of @{term L4Src} and @{term L4Dst} is more grave. While~\cite{specification10} does not state anything about layer 4 ports and masks, From e8c6a198c648cd3a9c36955bbe826e4120d0212b Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:19:07 -0400 Subject: [PATCH 06/87] spelling: algorithm Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy b/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy index 9d7b0651..d18427ec 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy @@ -692,7 +692,7 @@ text\Examples\ Rule MatchAny action.Drop]" apply(rule no_spoofing_iface) apply(simp_all add: simple_ruleset_def) (*simple and nnf*) - by eval (*executable spoofing alogorithm*) + by eval (*executable spoofing algorithm*) text\Example 2: From 30556895b0d0cf7d47d5194115627fe32dbf92a1 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:19:12 -0400 Subject: [PATCH 07/87] spelling: alleviate Signed-off-by: Josh Soref --- thy/LOFT/document/chap3.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/document/chap3.tex b/thy/LOFT/document/chap3.tex index f3289b41..504dd3d6 100644 --- a/thy/LOFT/document/chap3.tex +++ b/thy/LOFT/document/chap3.tex @@ -1,7 +1,7 @@ \section{Evaluation}\label{sec:eval} In Section~\ref{sec:conv}, we have made lots of definitions and created lots of models. How far these models are in accordance with the real world has been up to the vigilance of the reader. -This section attemts to leviate this burden by providing some examples. +This section attemts to alleviate this burden by providing some examples. \subsection{Mininet Examples} \label{sec:mnex} From 6780140f98805921d17ff4a8c438085c8469d975 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:19:21 -0400 Subject: [PATCH 08/87] spelling: allowed Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy b/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy index d18427ec..318d6fa0 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy @@ -365,7 +365,7 @@ begin text\The following algorithm sound but not complete.\ - (*alowed: set ip ips potentially allowed for iface + (*allowed: set ip ips potentially allowed for iface denied: set of ips definitely dropped for iface*) private fun no_spoofing_algorithm :: "iface \ 'i::len ipassignment \ 'i common_primitive rule list \ 'i word set \ 'i word set \ bool" where From e8e92d3d9b6c9c7ac01cd17eac4b6079b4c877d3 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:19:33 -0400 Subject: [PATCH 09/87] spelling: analysis Signed-off-by: Josh Soref --- haskell_tool/lib/Network/IPTables/Main.hs | 2 +- haskell_tool/test/Suites/GoldenFiles/help | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/haskell_tool/lib/Network/IPTables/Main.hs b/haskell_tool/lib/Network/IPTables/Main.hs index 40194fb9..47d5b42a 100644 --- a/haskell_tool/lib/Network/IPTables/Main.hs +++ b/haskell_tool/lib/Network/IPTables/Main.hs @@ -133,7 +133,7 @@ main' ops = do \It abstracts over unknown matches. \ \By default, it does an overapproximation, i.e. it loads a more permissive version of the ruleset. \ \Then it runs a number of analysis. \ - \Overapproximation means: if the anaylsis concludes that the packets you want to be dropped are dropped in the loaded overapproximation, then they are also dropped for your real firewall (without approximation)." + \Overapproximation means: if the analysis concludes that the packets you want to be dropped are dropped in the loaded overapproximation, then they are also dropped for your real firewall (without approximation)." --print (cmdArgs::CommandLineArgs) (verbose, ipassmt, rtbl, table, chain, smOptions, (srcname, src)) <- readArgs ops cmdArgs diff --git a/haskell_tool/test/Suites/GoldenFiles/help b/haskell_tool/test/Suites/GoldenFiles/help index 5b9468b5..5667e92e 100644 --- a/haskell_tool/test/Suites/GoldenFiles/help +++ b/haskell_tool/test/Suites/GoldenFiles/help @@ -4,7 +4,7 @@ and loads one table and chain. By default, it loads the `filter` table and the where only `ACCEPT` and `DROP` actions remain. It abstracts over unknown matches. By default, it does an overapproximation, i.e. it loads a more permissive version of the ruleset. Then it runs a number of analysis. -Overapproximation means: if the anaylsis concludes that the packets you want to +Overapproximation means: if the analysis concludes that the packets you want to be dropped are dropped in the loaded overapproximation, then they are also dropped for your real firewall (without approximation). From 65150b5fa38066ed2c4106aae28a93b5cc95e540 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:19:46 -0400 Subject: [PATCH 10/87] spelling: arithmetic Signed-off-by: Josh Soref --- thy/Word_Lib/Word_Lemmas.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Word_Lib/Word_Lemmas.thy b/thy/Word_Lib/Word_Lemmas.thy index b715bf52..5acc6a29 100644 --- a/thy/Word_Lib/Word_Lemmas.thy +++ b/thy/Word_Lib/Word_Lemmas.thy @@ -3007,7 +3007,7 @@ lemma word_le_plus:"\(a::('a::len) word) < a + b; c < b\ \ Date: Thu, 21 Oct 2021 22:19:58 -0400 Subject: [PATCH 11/87] spelling: assignments Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy index 135cb28f..8e67d38c 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy @@ -365,7 +365,7 @@ subsection\IP Assignment difference\ [(d, (k a b d, k b a d)). d \ remdups (map fst (a @ b))]" - text\If an interface is defined in both ipassignments and there is no difference + text\If an interface is defined in both ip and there is no difference then the two ipassignements describe the same IP range for this interface.\ lemma ipassmt_diff_ifce_equal: "(ifce, [], []) \ set (ipassmt_diff ipassmt1 ipassmt2) \ ifce \ dom (map_of ipassmt1) \ ifce \ dom (map_of ipassmt2) \ From 2727888ed42ef60f9e90714942eb8a169db56be7 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:09 -0400 Subject: [PATCH 12/87] spelling: attempts Signed-off-by: Josh Soref --- thy/LOFT/document/chap3.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/document/chap3.tex b/thy/LOFT/document/chap3.tex index 504dd3d6..9bad3512 100644 --- a/thy/LOFT/document/chap3.tex +++ b/thy/LOFT/document/chap3.tex @@ -1,7 +1,7 @@ \section{Evaluation}\label{sec:eval} In Section~\ref{sec:conv}, we have made lots of definitions and created lots of models. How far these models are in accordance with the real world has been up to the vigilance of the reader. -This section attemts to alleviate this burden by providing some examples. +This section attempts to alleviate this burden by providing some examples. \subsection{Mininet Examples} \label{sec:mnex} From d9c8013eba6c8a52240263d7c0e27ba2babaae39 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:15 -0400 Subject: [PATCH 13/87] spelling: automatically Signed-off-by: Josh Soref --- haskell_tool/lib/Data_Bits.README | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/haskell_tool/lib/Data_Bits.README b/haskell_tool/lib/Data_Bits.README index f8fde8c1..2294078a 100644 --- a/haskell_tool/lib/Data_Bits.README +++ b/haskell_tool/lib/Data_Bits.README @@ -1,3 +1,3 @@ -Automaticalyy generated by AFP Native_Word entry!! +Automatically generated by AFP Native_Word entry!! Do not edit! Regenerate each time! From 8024f5cd43b68ed5449e243159138af7d69591e1 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:20 -0400 Subject: [PATCH 14/87] spelling: boolean Signed-off-by: Josh Soref --- thy/Iptables_Semantics/No_Spoof_Embeddings.thy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/thy/Iptables_Semantics/No_Spoof_Embeddings.thy b/thy/Iptables_Semantics/No_Spoof_Embeddings.thy index 5dada3eb..87cd9d9a 100644 --- a/thy/Iptables_Semantics/No_Spoof_Embeddings.thy +++ b/thy/Iptables_Semantics/No_Spoof_Embeddings.thy @@ -8,7 +8,7 @@ section\Spoofing protection in Ternary Semantics implies Spoofing protecti text\If @{const no_spoofing} is shown in the ternary semantics, it implies that no spoofing is possible in the Boolean semantics with magic oracle. We only assume that the oracle agrees with the @{const common_matcher} on the not-unknown parts.\ - lemma approximating_imp_booloan_semantics_nospoofing: + lemma approximating_imp_boolean_semantics_nospoofing: assumes "matcher_agree_on_exact_matches \ common_matcher" and "simple_ruleset rs" and no_spoofing: "no_spoofing TYPE('pkt_ext) ipassmt rs" @@ -38,7 +38,7 @@ text\If @{const no_spoofing} is shown in the ternary semantics, it implies and no_spoofing: "no_spoofing TYPE('pkt_ext) ipassmt rs" and "iface \ dom ipassmt" shows "{p_src p | p :: ('i::len,'pkt_ext) tagged_packet_scheme. (\,\,p\p_iiface:=iface_sel iface\\ \rs, Undecided\ \ Decision FinalAllow)} \ ipcidr_union_set (set (the (ipassmt iface)))" - using approximating_imp_booloan_semantics_nospoofing[OF assms(1) assms(2) assms(3), where \=\] + using approximating_imp_boolean_semantics_nospoofing[OF assms(1) assms(2) assms(3), where \=\] using assms(4) by blast @@ -55,7 +55,7 @@ text\If @{const no_spoofing} is shown in the ternary semantics, it implies { assume no_spoofing: "no_spoofing TYPE('pkt_ext) ipassmt rs" have "{p_src p | p :: ('i,'pkt_ext) tagged_packet_scheme. (\,\,p\p_iiface:=iface_sel iface\\ \rs, Undecided\ \ Decision FinalAllow)} \ ipcidr_union_set (set (the (ipassmt iface)))" - using approximating_imp_booloan_semantics_nospoofing[OF assms(1) assms(2) no_spoofing, where \=\] + using approximating_imp_boolean_semantics_nospoofing[OF assms(1) assms(2) no_spoofing, where \=\] using assms(5) by blast } with no_spoofing_iface[OF assms(2) assms(3) no_spoofing_executable] show ?thesis by blast From 27e26e6e549147b20b0a8ffbf66f8711e8825f08 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:24 -0400 Subject: [PATCH 15/87] spelling: chain Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Parser.thy | 2 +- thy/Iptables_Semantics/Primitive_Matchers/Parser6.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Parser.thy b/thy/Iptables_Semantics/Primitive_Matchers/Parser.thy index c6a42ed0..b00e6098 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Parser.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Parser.thy @@ -447,7 +447,7 @@ local else r end; fun append table chain rule = case FirewallTable.lookup table chain - of NONE => raise Fail ("uninitialized cahin: "^chain) + of NONE => raise Fail ("uninitialized chain: "^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) = diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Parser6.thy b/thy/Iptables_Semantics/Primitive_Matchers/Parser6.thy index f8bb4f93..3b9f6dcc 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Parser6.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Parser6.thy @@ -451,7 +451,7 @@ local else r end; fun append table chain rule = case FirewallTable.lookup table chain - of NONE => raise Fail ("uninitialized cahin: "^chain) + of NONE => raise Fail ("uninitialized chain: "^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) = From 540d8385bb5453eee07877829c4a453d19661cb8 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:29 -0400 Subject: [PATCH 16/87] spelling: coincide Signed-off-by: Josh Soref --- thy/LOFT/document/chap3.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/document/chap3.tex b/thy/LOFT/document/chap3.tex index 9bad3512..c556d94e 100644 --- a/thy/LOFT/document/chap3.tex +++ b/thy/LOFT/document/chap3.tex @@ -148,7 +148,7 @@ \subsection{Performance Evaluation} \item Some combinations of matches from the firewall and the routing table cannot be ruled out, since the firewall match might only contain an output port and the rule can thus only apply for the packets matching a few routing table entries. However, the translation is not aware of that and can thus not remove the combination of the firewall rule and other routing table entries. \end{itemize} -In some rules, the conditions above coincede, resulting in $416\ (=16 \cdot 26)$ rules. +In some rules, the conditions above coincide, resulting in $416\ (=16 \cdot 26)$ rules. To avoid the high number of rules resulting from the port matches, rules that forbids packets with source or destination port 0 could be added to the start of the firewall and the $1$-$65535$ could be removed; dealing with the firewall / routing table problem is part of the future work on output interfaces. From 9400986d453bbceee9a07eb6b144cca9c6f0b9a1 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:33 -0400 Subject: [PATCH 17/87] spelling: comparisons Signed-off-by: Josh Soref --- thy/Native_Word/Uint_Userguide.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Native_Word/Uint_Userguide.thy b/thy/Native_Word/Uint_Userguide.thy index e3aa53b7..dd83a48e 100644 --- a/thy/Native_Word/Uint_Userguide.thy +++ b/thy/Native_Word/Uint_Userguide.thy @@ -155,7 +155,7 @@ text {* subsection {* Example: expressions and two semantics *} text {* - As the running example, we consider a language of expressions (literal values, less-than comparisions and conditional) where values are either booleans or 32-bit words. + As the running example, we consider a language of expressions (literal values, less-than comparisons and conditional) where values are either booleans or 32-bit words. The original specification uses the type @{typ "32 word"}. *} From 50f7cb06605ff0e2f6fd5b1ef24b23a550455f09 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:37 -0400 Subject: [PATCH 18/87] spelling: compressed Signed-off-by: Josh Soref --- thy/IP_Addresses/IPv6.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/IP_Addresses/IPv6.thy b/thy/IP_Addresses/IPv6.thy index ab756ab3..5030a1ff 100644 --- a/thy/IP_Addresses/IPv6.thy +++ b/thy/IP_Addresses/IPv6.thy @@ -210,7 +210,7 @@ subsection\Syntax of IPv6 Addresses\ | [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g] \ Some (IPv6AddrCompressed7_7 a b c d e f () g) | [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None] \ Some (IPv6AddrCompressed8_7 a b c d e f g ()) - | _ \ None (*invalid ipv6 copressed address.*) + | _ \ None (*invalid ipv6 compressed address.*) )" fun ipv6addr_syntax_compressed_to_list :: "ipv6addr_syntax_compressed \ ((16 word) option) list" From 1c3a91da8e5ceab99acefe6db1000e3a321769fe Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:41 -0400 Subject: [PATCH 19/87] spelling: conditions Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Tool/Autoref_Tool.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Automatic_Refinement/Tool/Autoref_Tool.thy b/thy/Automatic_Refinement/Tool/Autoref_Tool.thy index b220c793..c724450a 100644 --- a/thy/Automatic_Refinement/Tool/Autoref_Tool.thy +++ b/thy/Automatic_Refinement/Tool/Autoref_Tool.thy @@ -107,13 +107,13 @@ method_setup autoref_trans_step = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' ( Autoref_Translate.trans_dbg_step_tac (Autoref_Phases.init_data ctxt) )) - *} "Single translation step, leaving unsolved side-coditions" + *} "Single translation step, leaving unsolved side-conditions" method_setup autoref_trans_step_only = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' ( Autoref_Translate.trans_step_only_tac (Autoref_Phases.init_data ctxt) )) - *} "Single translation step, not attempting to solve side-coditions" + *} "Single translation step, not attempting to solve side-conditions" method_setup autoref_side = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' ( From 0b880b3ac32e0877fae5b5a8af5d3400ef060dfa Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:45 -0400 Subject: [PATCH 20/87] spelling: debugging Signed-off-by: Josh Soref --- haskell_tool/lib/Network/IPTables/Ruleset.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/haskell_tool/lib/Network/IPTables/Ruleset.hs b/haskell_tool/lib/Network/IPTables/Ruleset.hs index 7d991964..1336abd1 100644 --- a/haskell_tool/lib/Network/IPTables/Ruleset.hs +++ b/haskell_tool/lib/Network/IPTables/Ruleset.hs @@ -156,7 +156,7 @@ filter_Isabelle_Action ps = case fAction ps of [] -> Isabelle.Empty --- this is just DEBUGING +-- this is just DEBUGGING -- tries to catch errors of rulesetLookup checkParsedTables :: Isabelle.Len a => Ruleset a -> IO () checkParsedTables res = mapM_ check tables From 5cdf46cef16fa8a08567fdb327fe38e45b266f26 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:49 -0400 Subject: [PATCH 21/87] spelling: deferred Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Tool/Autoref_Translate.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Automatic_Refinement/Tool/Autoref_Translate.thy b/thy/Automatic_Refinement/Tool/Autoref_Translate.thy index 04374bca..57567601 100644 --- a/thy/Automatic_Refinement/Tool/Autoref_Translate.thy +++ b/thy/Automatic_Refinement/Tool/Autoref_Translate.thy @@ -269,7 +269,7 @@ ML {* val msg = case concl of @{mpat "Trueprop (DEFER_tag _)"} - => Pretty.str "Could not solve defered side condition" + => Pretty.str "Could not solve deferred side condition" | @{mpat "Trueprop ((_,_)\_)"} => Pretty.str "Could not refine subterm" | _ => Pretty.str "Internal: Unexpected goal" From a5a3374db36bb8acc32705f233cdce3e69a7309c Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:20:54 -0400 Subject: [PATCH 22/87] spelling: dependency Signed-off-by: Josh Soref --- thy/IP_Addresses/WordInterval_Sorted.thy | 2 +- thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/IP_Addresses/WordInterval_Sorted.thy b/thy/IP_Addresses/WordInterval_Sorted.thy index 6efccc35..ab24aa49 100644 --- a/thy/IP_Addresses/WordInterval_Sorted.thy +++ b/thy/IP_Addresses/WordInterval_Sorted.thy @@ -1,6 +1,6 @@ theory WordInterval_Sorted imports WordInterval - "../Automatic_Refinement/Lib/Misc" (*Mergesort. TODO: dependnecy! we need a mergesort afp entry!!*) + "../Automatic_Refinement/Lib/Misc" (*Mergesort. TODO: dependency! we need a mergesort afp entry!!*) "~~/src/HOL/Library/Product_Lexorder" begin diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy index 8e67d38c..7120b7f1 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy @@ -3,7 +3,7 @@ imports Common_Primitive_Syntax "../Semantics_Ternary/Primitive_Normalization" "../../Simple_Firewall/Primitives/Iface" "../../Simple_Firewall/Common/IP_Addr_WordInterval_toString" (*for debug pretty-printing*) - "../../Automatic_Refinement/Lib/Misc" (*dependnecy!*) + "../../Automatic_Refinement/Lib/Misc" (*dependency!*) begin text\A mapping from an interface to its assigned ip addresses in CIDR notation\ From b202e0b98cfcbd4bdb93e684117f8710e39d63eb Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:01 -0400 Subject: [PATCH 23/87] spelling: destroy Signed-off-by: Josh Soref --- thy/Iptables_Semantics/ROOT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/ROOT b/thy/Iptables_Semantics/ROOT index 40a72222..f531ea6d 100644 --- a/thy/Iptables_Semantics/ROOT +++ b/thy/Iptables_Semantics/ROOT @@ -19,7 +19,7 @@ session "Bitmagic" = IP_Addresses + session "Iptables_Semantics" = Routing + theories[document=false] "~~/src/HOL/Library/LaTeXsugar" - (*The Native_Word things destory the latex document! Does not compile, ...*) + (*The Native_Word things destroy the latex document! Does not compile, ...*) "../Native_Word/More_Bits_Int" "../Native_Word/Code_Target_Bits_Int" "~~/src/HOL/Library/Code_Target_Nat" From 731ae2abddbdcd5f38653027868b1ec2b5dbe97a Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:08 -0400 Subject: [PATCH 24/87] spelling: different Signed-off-by: Josh Soref --- thy/LOFT/OpenFlow_Matches.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/OpenFlow_Matches.thy b/thy/LOFT/OpenFlow_Matches.thy index 71c04369..df0ff839 100644 --- a/thy/LOFT/OpenFlow_Matches.thy +++ b/thy/LOFT/OpenFlow_Matches.thy @@ -80,7 +80,7 @@ function prerequisites :: "of_match_field \ of_match_field set \ m \ prerequisites v m)" | (* OF_IPV4_DST ETH_TYPE=0x0800 *) "prerequisites (IPv4Dst _) m = (let v = EtherType 0x0800 in v \ m \ prerequisites v m)" | -(* Now here goes a bit of fuzz: OF specifies differen OXM_OF_(TCP,UDP,L4_Protocol.SCTP,\)_(SRC,DST). I only have L4Src. So gotta make do with that. *) +(* Now here goes a bit of fuzz: OF specifies different OXM_OF_(TCP,UDP,L4_Protocol.SCTP,\)_(SRC,DST). I only have L4Src. So gotta make do with that. *) "prerequisites (L4Src _ _) m = (\proto \ {TCP,UDP,L4_Protocol.SCTP}. let v = IPv4Proto proto in v \ m \ prerequisites v m)" | "prerequisites (L4Dst _ _) m = prerequisites (L4Src undefined undefined) m" by pat_completeness auto From 21e4a1a03aedef7058811ed83407bc7f3f5fca0c Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:16 -0400 Subject: [PATCH 25/87] spelling: disjunction Signed-off-by: Josh Soref --- .../Primitive_Matchers/Common_Primitive_Matcher_Generic.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher_Generic.thy b/thy/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher_Generic.thy index 2a7ab1bf..5efe08b2 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher_Generic.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher_Generic.thy @@ -68,7 +68,7 @@ begin by(auto simp add: Ports_single_not Ports_single Prot_single_not Prot_single) - lemma multiports_disjuction: + lemma multiports_disjunction: "(\rg\set spts. matches (\, \) (Match (Src_Ports (L4Ports proto [rg]))) a p) \ matches (\, \) (Match (Src_Ports (L4Ports proto spts))) a p" "(\rg\set dpts. matches (\, \) (Match (Dst_Ports (L4Ports proto [rg]))) a p) \ matches (\, \) (Match (Dst_Ports (L4Ports proto dpts))) a p" by(auto simp add: Src_Ports Dst_Ports match_raw_ternary bool_to_ternary_simps ports_to_set From a5da55fc8c3a7b572504983a312c934325a66b78 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:22 -0400 Subject: [PATCH 26/87] spelling: don't Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy b/thy/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy index 47e82c49..ef94b60b 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy @@ -8,7 +8,7 @@ begin --"Misc" -(*we dont't have an empty ip space, but a space which only contains the 0 address. We will use the option type to denote the empty space in some functions.*) +(*we don't have an empty ip space, but a space which only contains the 0 address. We will use the option type to denote the empty space in some functions.*) lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 33 = {0}" by(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def ipset_from_cidr_large_pfxlen) From a68b1286193c60e695642b60f96db75eb6226d19 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:27 -0400 Subject: [PATCH 27/87] spelling: empty Signed-off-by: Josh Soref --- thy/IP_Addresses/WordInterval.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/IP_Addresses/WordInterval.thy b/thy/IP_Addresses/WordInterval.thy index 84ad46ed..8916dfa8 100644 --- a/thy/IP_Addresses/WordInterval.thy +++ b/thy/IP_Addresses/WordInterval.thy @@ -595,7 +595,7 @@ lemma wordinterval_to_set_alt: "wordinterval_to_set r = {x. wordinterval_element lemma wordinterval_un_empty: "wordinterval_empty r1 \ wordinterval_eq (wordinterval_union r1 r2) r2" by(subst wordinterval_eq_set_eq, simp) -lemma wordinterval_un_emty_b: +lemma wordinterval_un_empty_b: "wordinterval_empty r2 \ wordinterval_eq (wordinterval_union r1 r2) r1" by(subst wordinterval_eq_set_eq, simp) From 8d279b7d47151c5e436666ec6bf8ecac73e5a69c Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:35 -0400 Subject: [PATCH 28/87] spelling: entry-s Signed-off-by: Josh Soref --- thy/LOFT/Semantics_OpenFlow.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/Semantics_OpenFlow.thy b/thy/LOFT/Semantics_OpenFlow.thy index bc9e4a9c..7fc59987 100644 --- a/thy/LOFT/Semantics_OpenFlow.thy +++ b/thy/LOFT/Semantics_OpenFlow.thy @@ -37,7 +37,7 @@ datatype ('m, 'a) flow_entry_match = OFEntry (ofe_prio: "16 word") (ofe_fields: find_consts "(('a \ 'b) \ 'c) \ 'a \ 'b \ 'c" (* but no "uncurry" *) find_consts "('a \ 'b \ 'c) \ ('a \ 'b) \ 'c" -(* Anyway, we want this to easily construct OFEntrys from tuples *) +(* Anyway, we want this to easily construct OFEntry-s from tuples *) definition "split3 f p \ case p of (a,b,c) \ f a b c" find_consts "('a \ 'b \ 'c \ 'd) \ ('a \ 'b \ 'c) \ 'd" From 4774fe82594e44599734fdea852c8ba444990b35 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:43 -0400 Subject: [PATCH 29/87] spelling: environment Signed-off-by: Josh Soref --- thy/Iptables_Semantics/document/mathpartir.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/document/mathpartir.sty b/thy/Iptables_Semantics/document/mathpartir.sty index a3ac05cf..569eca1b 100644 --- a/thy/Iptables_Semantics/document/mathpartir.sty +++ b/thy/Iptables_Semantics/document/mathpartir.sty @@ -430,7 +430,7 @@ %%% Exports -% Envirnonment mathpar +% Environment mathpar \let \inferrule \mpr@infer From 76b363a64de6dfbe39d81dd61dd71707b0dd6fc3 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:51 -0400 Subject: [PATCH 30/87] spelling: equality Signed-off-by: Josh Soref --- .../Semantics_Ternary/Primitive_Normalization.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy b/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy index b8efa18e..20fdb8ff 100644 --- a/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy +++ b/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy @@ -380,7 +380,7 @@ lemma primitive_extractor_reassemble_preserves: normalized_nnf_match m \ P m \ P MatchAny \ - primitive_extractor (disc, sel) m = (as, ms) \ (*turn eqality around to simplify proof*) + primitive_extractor (disc, sel) m = (as, ms) \ (*turn equality around to simplify proof*) (\m1 m2. P (MatchAnd m1 m2) \ P m1 \ P m2) \ (\ls1 ls2. P (alist_and' (ls1 @ ls2)) \ P (alist_and' ls1) \ P (alist_and' ls2)) \ P (alist_and' (NegPos_map C as))" From 5c4c3ff853a560cfd3e6747ac33348c7ef97f86b Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:21:57 -0400 Subject: [PATCH 31/87] spelling: evaluated Signed-off-by: Josh Soref --- thy/LOFT/OpenFlow_Documentation.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/OpenFlow_Documentation.thy b/thy/LOFT/OpenFlow_Documentation.thy index 747d0a7f..80b99de1 100644 --- a/thy/LOFT/OpenFlow_Documentation.thy +++ b/thy/LOFT/OpenFlow_Documentation.thy @@ -228,7 +228,7 @@ Guha \emph{et al.} decided to use the fact that the preconditions can be arrange They evaluated match conditions in a manner following that graph: first, all field matches without preconditions are evaluated. Upon evaluating a field match (e.g., @{term "EtherType 0x0800"}), the matches that had their precondition fulfilled by it - (e.g., @{term IPv4Src} and @{term IPv4Src} in this example) are evalutated. + (e.g., @{term IPv4Src} and @{term IPv4Src} in this example) are evaluated. This mirrors the faulty behavior of some implementations (see \cite{guha2013machine}). Adopting that behavior into our model would mean that any packet matches against the field match set @{term "{IPv4Dst (PrefixMatch 134744072 32)}"} instead of just those destined for 8.8.8.8 or causing an error. We found this to be unsatisfactory.\ From dc951fb2a04dd32d06cf582a11786040151bf079 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:22:07 -0400 Subject: [PATCH 32/87] spelling: existing Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Examples/sns.ias.edu/test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Examples/sns.ias.edu/test.sh b/thy/Iptables_Semantics/Examples/sns.ias.edu/test.sh index 57340092..ae07d299 100755 --- a/thy/Iptables_Semantics/Examples/sns.ias.edu/test.sh +++ b/thy/Iptables_Semantics/Examples/sns.ias.edu/test.sh @@ -12,7 +12,7 @@ modprobe ip_conntrack modprobe ip_conntrack_ftp # These lines are here in case rules are already in place and the script is ever rerun on the fly. -# We want to remove all rules and pre-exisiting user defined chains and zero the counters +# We want to remove all rules and pre-existing user defined chains and zero the counters # before we implement new rules. iptables -F iptables -X From 89ffdcc6c07775e7aae8ce998651f89326170e32 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:22:13 -0400 Subject: [PATCH 33/87] spelling: expressions Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy b/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy index d6b6bc99..b5cfdec6 100644 --- a/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy +++ b/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy @@ -4,7 +4,7 @@ begin section\Normalized (DNF) matches\ -text\simplify a match expression. The output is a list of match exprissions, the semantics is @{text "\"} of the list elements.\ +text\simplify a match expression. The output is a list of match expressions, the semantics is @{text "\"} of the list elements.\ fun normalize_match :: "'a match_expr \ 'a match_expr list" where "normalize_match (MatchAny) = [MatchAny]" | "normalize_match (Match m) = [Match m]" | From 694b35fc5f983aa32deaf0816e28f127c8035bfe Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:22:19 -0400 Subject: [PATCH 34/87] spelling: extractor Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy b/thy/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy index 1d875c5f..fdf3d72b 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy @@ -541,7 +541,7 @@ subsection\Normalizing Positive Matches on Ports\ shows "m' \ set (normalize_positive_ports_step (disc,sel) C m) \ normalized_nnf_match m'" apply(simp add: normalize_positive_ports_step_def) apply(elim exE conjE, rename_tac rst spts) - apply(drule sym) (*switch primitive_extrartor = *) + apply(drule sym) (*switch primitive_extractor = *) apply(frule primitive_extractor_correct(2)[OF n wf_disc_sel]) apply(subgoal_tac "getNeg spts = []") (*duplication above*) prefer 2 subgoal @@ -559,7 +559,7 @@ subsection\Normalizing Positive Matches on Ports\ apply(intro ballI, rename_tac m') apply(simp) apply(elim exE conjE, rename_tac rst spts) - apply(drule sym) (*switch primitive_extrartor = *) + apply(drule sym) (*switch primitive_extractor = *) apply(frule primitive_extractor_correct(2)[OF n wf_disc_sel]) apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel]) apply(subgoal_tac "getNeg spts = []") (*duplication above*) From ec64777e015f92b434b208dbf5508f897fdd4d7b Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:22:23 -0400 Subject: [PATCH 35/87] spelling: flag Signed-off-by: Josh Soref --- .../Primitive_Matchers/L4_Protocol_Flags.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/L4_Protocol_Flags.thy b/thy/Iptables_Semantics/Primitive_Matchers/L4_Protocol_Flags.thy index 3c12ac7e..a3df201f 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/L4_Protocol_Flags.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/L4_Protocol_Flags.thy @@ -75,7 +75,7 @@ section\Matching TCP Flags\ else (\ c1 \ fmask1) \ (\ c2 \ fmask2))" context begin - private lemma funny_set_falg_fmask_helper: "c2 \ fmask2 \ (c1 = c2 \ fmask1 = fmask2) = (\pkt. (pkt \ fmask1 = c1) = (pkt \ fmask2 = c2))" + private lemma funny_set_flag_fmask_helper: "c2 \ fmask2 \ (c1 = c2 \ fmask1 = fmask2) = (\pkt. (pkt \ fmask1 = c1) = (pkt \ fmask2 = c2))" apply rule apply presburger apply(subgoal_tac "fmask1 = fmask2") @@ -127,7 +127,7 @@ section\Matching TCP Flags\ apply(cases f1, cases f2, simp) apply(rename_tac fmask1 c1 fmask2 c2) apply(intro conjI impI) - using funny_set_falg_fmask_helper apply metis + using funny_set_flag_fmask_helper apply metis apply blast done end From 5b7f37e6cc20934b5221e55ec10640983e588a1f Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:22:28 -0400 Subject: [PATCH 36/87] spelling: following Signed-off-by: Josh Soref --- thy/Iptables_Semantics/document/mathpartir.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/document/mathpartir.sty b/thy/Iptables_Semantics/document/mathpartir.sty index 569eca1b..f9278dd0 100644 --- a/thy/Iptables_Semantics/document/mathpartir.sty +++ b/thy/Iptables_Semantics/document/mathpartir.sty @@ -335,7 +335,7 @@ % line of its conclusion % % The second form can be parameterized, using the key=val interface. The -% folloiwng keys are recognized: +% following keys are recognized: % % width set the width of the rule to val % narrower set the width of the rule to val\hsize From adff6fabede157203d91c2a51dcc4edc8b397619 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:23:47 -0400 Subject: [PATCH 37/87] spelling: haven't Signed-off-by: Josh Soref --- haskell_tool/test/Suites/Parser.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/haskell_tool/test/Suites/Parser.hs b/haskell_tool/test/Suites/Parser.hs index 78f39e70..9e4accae 100644 --- a/haskell_tool/test/Suites/Parser.hs +++ b/haskell_tool/test/Suites/Parser.hs @@ -10,7 +10,7 @@ import Test.Tasty import Test.Tasty.HUnit as HU --- we always have "-m protocolid:0" (note the 0) because we havn't filled the protocol yet +-- we always have "-m protocolid:0" (note the 0) because we haven't filled the protocol yet expected_result = "*filter\n\ \:DOS~Pro-t_ect - [0:0]\n\ \:FORWARD DROP [0:0]\n\ From 38f49e5648eda94b90ff48df19a7f78ab06f5153 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:23:50 -0400 Subject: [PATCH 38/87] spelling: homogeneity Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy | 6 +++--- thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy b/thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy index 8f769240..0505d11a 100644 --- a/thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy +++ b/thy/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy @@ -10,7 +10,7 @@ text {* Priority tags are used to influence the ordering of refinement theorems. A priority tag defines two numeric priorities, a major and a minor priority. The major priority is considered first, the minor priority last, i.e., after - the homogenity and relator-priority criteria. + the homogeneity and relator-priority criteria. The default value for both priorities is 0. *} definition PRIO_TAG :: "int \ int \ bool" @@ -459,12 +459,12 @@ ML {* structure hom_rules = Named_Sorted_Thms ( val name = @{binding autoref_hom} - val description = "Autoref: Homogenity rules" + val description = "Autoref: Homogeneity rules" val sort = K I val transform = K ( fn thm => case Thm.concl_of thm of @{mpat "Trueprop (CONSTRAINT _ _)"} => [thm] - | _ => raise THM ("Invalid homogenity rule",~1,[thm]) + | _ => raise THM ("Invalid homogeneity rule",~1,[thm]) ) ) diff --git a/thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy b/thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy index 81714d7b..09cb3179 100644 --- a/thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy +++ b/thy/Automatic_Refinement/Tool/Autoref_Gen_Algo.thy @@ -4,7 +4,7 @@ imports Autoref_Translate begin (* TODO/FIXME: The priority ordering is not yet suited for generic - algorithms! If a refinement rule is generic, the homogenity and relator + algorithms! If a refinement rule is generic, the homogeneity and relator measures make no sense, as they are applied to schematic variables. However, currently generic algorithms seem to have lower priority than specific ones, so we can probably live with this problem for a while. From f3a2842d403f9a8c78477af74ee3b5ee65edc335 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:00 -0400 Subject: [PATCH 39/87] spelling: identity Signed-off-by: Josh Soref --- haskell_tool/test/Suites/ParserHelper.hs | 32 ++++++++++++------------ 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/haskell_tool/test/Suites/ParserHelper.hs b/haskell_tool/test/Suites/ParserHelper.hs index 4a735bff..a223da9a 100644 --- a/haskell_tool/test/Suites/ParserHelper.hs +++ b/haskell_tool/test/Suites/ParserHelper.hs @@ -13,7 +13,7 @@ import Test.Tasty.HUnit as HU -test_parse_show_identiy parser str = HU.testCase ("ParserHelper: parse show identity ("++str++")") $ do +test_parse_show_identity parser str = HU.testCase ("ParserHelper: parse show identity ("++str++")") $ do let result = case runParser eofParser () "" str of Left err -> do error $ show err Right result -> show result @@ -36,21 +36,21 @@ test_parse_quotedstring str = HU.testCase ("ParserHelper: quoted string (`"++str --TODO negative tests! tests = testGroup "ParserHelper Unit tests" $ - [ test_parse_show_identiy Network.IPTables.ParserHelper.ipv4addr "192.168.0.1" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv4cidr "192.168.0.1/24" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv4range "192.168.0.1-192.168.0.255" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6cidr "::/64" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6range "::-::" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "2001:db8::8:800:200c:417a" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "ff01::101" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::8:800:200c:417a" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "2001:db8::" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "ff00::" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "fe80::" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "::1" - , test_parse_show_identiy Network.IPTables.ParserHelper.ipv6addr "2001:db8::1" + [ test_parse_show_identity Network.IPTables.ParserHelper.ipv4addr "192.168.0.1" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv4cidr "192.168.0.1/24" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv4range "192.168.0.1-192.168.0.255" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6cidr "::/64" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6range "::-::" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "2001:db8::8:800:200c:417a" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "ff01::101" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::8:800:200c:417a" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "2001:db8::" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "ff00::" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "fe80::" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "::1" + , test_parse_show_identity Network.IPTables.ParserHelper.ipv6addr "2001:db8::1" , test_parse_quotedstring "\"foo\"" , test_parse_quotedstring "\"foo with some \\\" escaped quote \"" , test_parse_quotedstring "\"foo with some escaped escape (\\\\) and proper ending quote \\\\\"" From d9f78f23daac9b167fc3de63f5a3927ce1a60224 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:05 -0400 Subject: [PATCH 40/87] spelling: ignore Signed-off-by: Josh Soref --- thy/IP_Addresses/IPv6.thy | 4 ++-- thy/Word_Lib/Word_Lemmas.thy | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/thy/IP_Addresses/IPv6.thy b/thy/IP_Addresses/IPv6.thy index 5030a1ff..f6503eed 100644 --- a/thy/IP_Addresses/IPv6.thy +++ b/thy/IP_Addresses/IPv6.thy @@ -479,7 +479,7 @@ subsection\Semantics\ have ucast_ipv6_piece_rule: "length (dropWhile Not (to_bl w)) \ 16 \ (ucast::16 word \ 128 word) ((ucast::128 word \ 16 word) w) = w" for w::ipv6addr - by(rule ucast_short_ucast_long_ingoreLeadingZero) (simp_all) + by(rule ucast_short_ucast_long_ignoreLeadingZero) (simp_all) have ucast_ipv6_piece: "16 \ 128 - n \ (ucast::16 word \ 128 word) ((ucast::128 word \ 16 word) (w AND (mask 16 << n) >> n)) << n = w AND (mask 16 << n)" for w::ipv6addr and n::nat @@ -510,7 +510,7 @@ subsection\Semantics\ have ucast16_ucast128_masks_highest_bits0: "(ucast ((ucast::ipv6addr \ 16 word) (ip AND 0xFFFF))) = ip AND 0xFFFF" apply(subst word128_masks_ipv6pieces)+ - apply(subst ucast_short_ucast_long_ingoreLeadingZero) + apply(subst ucast_short_ucast_long_ignoreLeadingZero) apply simp_all by (simp add: length_drop_mask) diff --git a/thy/Word_Lib/Word_Lemmas.thy b/thy/Word_Lib/Word_Lemmas.thy index 5acc6a29..1a1e0430 100644 --- a/thy/Word_Lib/Word_Lemmas.thy +++ b/thy/Word_Lib/Word_Lemmas.thy @@ -4635,7 +4635,7 @@ qed 'l is the longer word. 's is the shorter word. *) -lemma bl_cast_long_short_long_ingoreLeadingZero_generic: +lemma bl_cast_long_short_long_ignoreLeadingZero_generic: "length (dropWhile Not (to_bl w)) \ len_of TYPE('s) \ len_of TYPE('s) \ len_of TYPE('l) \ (of_bl:: bool list \ 'l::len word) (to_bl ((of_bl:: bool list \ 's::len word) (to_bl w))) = w" @@ -4655,12 +4655,12 @@ lemma bl_cast_long_short_long_ingoreLeadingZero_generic: For example: 'l::len word is 128 word (full ipv6 address) 's::len word is 16 word (address piece of ipv6 address in colon-text-representation) *) -corollary ucast_short_ucast_long_ingoreLeadingZero: +corollary ucast_short_ucast_long_ignoreLeadingZero: "length (dropWhile Not (to_bl w)) \ len_of TYPE('s) \ len_of TYPE('s) \ len_of TYPE('l) \ (ucast:: 's::len word \ 'l::len word) ((ucast:: 'l::len word \ 's::len word) w) = w" apply(subst Word.ucast_bl)+ - apply(rule bl_cast_long_short_long_ingoreLeadingZero_generic) + apply(rule bl_cast_long_short_long_ignoreLeadingZero_generic) apply(simp_all) done From b10ad90ce0b0fe0778a268385f1afe04d9f1ff28 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:09 -0400 Subject: [PATCH 41/87] spelling: ignored Signed-off-by: Josh Soref --- thy/LOFT/OpenFlow_Matches.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/OpenFlow_Matches.thy b/thy/LOFT/OpenFlow_Matches.thy index df0ff839..0c374e7a 100644 --- a/thy/LOFT/OpenFlow_Matches.thy +++ b/thy/LOFT/OpenFlow_Matches.thy @@ -84,7 +84,7 @@ function prerequisites :: "of_match_field \ of_match_field set \proto \ {TCP,UDP,L4_Protocol.SCTP}. let v = IPv4Proto proto in v \ m \ prerequisites v m)" | "prerequisites (L4Dst _ _) m = prerequisites (L4Src undefined undefined) m" by pat_completeness auto -(* Ignoredd PACKET_TYPE=foo *) +(* Ignored PACKET_TYPE=foo *) fun match_sorter :: "of_match_field \ nat" where "match_sorter (IngressPort _) = 1" | From 804221276ebbfa9088288e3bf45c6c08c2e3a3a8 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:14 -0400 Subject: [PATCH 42/87] spelling: imaginary Signed-off-by: Josh Soref --- haskell_tool/test/Suites/Parser.hs | 2 +- .../Examples/topoS_generated/Analyze_topos_generated.thy | 2 +- ...rk.iptables-save => imaginary_factory_network.iptables-save} | 0 ... => imaginary_factory_network.iptables-save.by-linux-kernel} | 0 4 files changed, 2 insertions(+), 2 deletions(-) rename thy/Iptables_Semantics/Examples/topoS_generated/{imaginray_factory_network.iptables-save => imaginary_factory_network.iptables-save} (100%) rename thy/Iptables_Semantics/Examples/topoS_generated/{imaginray_factory_network.iptables-save.by-linux-kernel => imaginary_factory_network.iptables-save.by-linux-kernel} (100%) diff --git a/haskell_tool/test/Suites/Parser.hs b/haskell_tool/test/Suites/Parser.hs index 9e4accae..aa66debc 100644 --- a/haskell_tool/test/Suites/Parser.hs +++ b/haskell_tool/test/Suites/Parser.hs @@ -323,7 +323,7 @@ test_service_matrix ipassmtMaybeString fileName expected_result errormsg = do test_topoS_generated_service_matrix = HU.testCase "test_topoS_generated_service_matrix" $ test_service_matrix Nothing rulesetFile expected_result errormsg - where rulesetFile = "../thy/Iptables_Semantics/Examples/topoS_generated/imaginray_factory_network.iptables-save.by-linux-kernel" + where rulesetFile = "../thy/Iptables_Semantics/Examples/topoS_generated/imaginary_factory_network.iptables-save.by-linux-kernel" errormsg = "service marix topoS_generated differs" expected_result = ([ ("10.8.8.1","10.8.8.1") diff --git a/thy/Iptables_Semantics/Examples/topoS_generated/Analyze_topos_generated.thy b/thy/Iptables_Semantics/Examples/topoS_generated/Analyze_topos_generated.thy index 2e2414e3..e05344b8 100644 --- a/thy/Iptables_Semantics/Examples/topoS_generated/Analyze_topos_generated.thy +++ b/thy/Iptables_Semantics/Examples/topoS_generated/Analyze_topos_generated.thy @@ -5,7 +5,7 @@ begin -parse_iptables_save factory_fw="imaginray_factory_network.iptables-save.by-linux-kernel" +parse_iptables_save factory_fw="imaginary_factory_network.iptables-save.by-linux-kernel" thm factory_fw_def thm factory_fw_FORWARD_default_policy_def diff --git a/thy/Iptables_Semantics/Examples/topoS_generated/imaginray_factory_network.iptables-save b/thy/Iptables_Semantics/Examples/topoS_generated/imaginary_factory_network.iptables-save similarity index 100% rename from thy/Iptables_Semantics/Examples/topoS_generated/imaginray_factory_network.iptables-save rename to thy/Iptables_Semantics/Examples/topoS_generated/imaginary_factory_network.iptables-save diff --git a/thy/Iptables_Semantics/Examples/topoS_generated/imaginray_factory_network.iptables-save.by-linux-kernel b/thy/Iptables_Semantics/Examples/topoS_generated/imaginary_factory_network.iptables-save.by-linux-kernel similarity index 100% rename from thy/Iptables_Semantics/Examples/topoS_generated/imaginray_factory_network.iptables-save.by-linux-kernel rename to thy/Iptables_Semantics/Examples/topoS_generated/imaginary_factory_network.iptables-save.by-linux-kernel From aa7452ae35077db8ad5dd12e67f2478946d477c6 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:18 -0400 Subject: [PATCH 43/87] spelling: inferred Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Autoref_Bindings_HOL.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Automatic_Refinement/Autoref_Bindings_HOL.thy b/thy/Automatic_Refinement/Autoref_Bindings_HOL.thy index 2ff6528e..9917fcdb 100644 --- a/thy/Automatic_Refinement/Autoref_Bindings_HOL.thy +++ b/thy/Automatic_Refinement/Autoref_Bindings_HOL.thy @@ -611,7 +611,7 @@ subsection "Examples" text {* Be careful to make the concrete type a schematic type variable. The default behaviour of @{text "schematic_lemma"} makes it a fixed variable, - that will not unify with the infered term! *} + that will not unify with the inferred term! *} schematic_goal "(?f::?'c,[1,2,3]@[4::nat])\?R" by autoref From b423a5e172f3f614cccb1a662f9efb5304d361c3 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:23 -0400 Subject: [PATCH 44/87] spelling: interruptible Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Lib/Foldi.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Automatic_Refinement/Lib/Foldi.thy b/thy/Automatic_Refinement/Lib/Foldi.thy index 76b7b546..13bf7d7a 100644 --- a/thy/Automatic_Refinement/Lib/Foldi.thy +++ b/thy/Automatic_Refinement/Lib/Foldi.thy @@ -1,7 +1,7 @@ -(* Title: Interuptible Fold +(* Title: Interruptible Fold Author: Thomas Tuerk *) -section {* Interuptible Fold *} +section {* Interruptible Fold *} theory Foldi imports Main begin From 7d8f2e3ebad43f0a695c7d85e57e44b72cf920d7 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:28 -0400 Subject: [PATCH 45/87] spelling: ip assignments Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy index 7120b7f1..bee23717 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy @@ -366,7 +366,7 @@ subsection\IP Assignment difference\ text\If an interface is defined in both ip and there is no difference - then the two ipassignements describe the same IP range for this interface.\ + then the two ip assignments describe the same IP range for this interface.\ lemma ipassmt_diff_ifce_equal: "(ifce, [], []) \ set (ipassmt_diff ipassmt1 ipassmt2) \ ifce \ dom (map_of ipassmt1) \ ifce \ dom (map_of ipassmt2) \ ipcidr_union_set (set (the ((map_of ipassmt1) ifce))) = From 49a40e98ba9068000f18b3e55db160784c2a69b1 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:33 -0400 Subject: [PATCH 46/87] spelling: likely Signed-off-by: Josh Soref --- haskell_tool/README.md | 2 +- haskell_tool/lib/Network/IPTables/Main.hs | 2 +- haskell_tool/test/Suites/GoldenFiles/help | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/haskell_tool/README.md b/haskell_tool/README.md index 38eb117d..a367a995 100644 --- a/haskell_tool/README.md +++ b/haskell_tool/README.md @@ -57,7 +57,7 @@ Available options: --routingtbl STRING Optional path to a routing table. --table STRING The table to load for analysis. Default: `filter`. Note: This tool does not support packet modification, - so loading tables such as `nat` will most likeley + so loading tables such as `nat` will most likely fail. --chain STRING The chain to start the analysis. Default: `FORWARD`. Use `INPUT` for a host-based firewall. diff --git a/haskell_tool/lib/Network/IPTables/Main.hs b/haskell_tool/lib/Network/IPTables/Main.hs index 47d5b42a..3812924a 100644 --- a/haskell_tool/lib/Network/IPTables/Main.hs +++ b/haskell_tool/lib/Network/IPTables/Main.hs @@ -45,7 +45,7 @@ data CommandLineArgsLabeled = CommandLineArgsLabeled { verbose :: Bool "Show verbose debug output (for example, of the parser)." , ipassmt :: Maybe FilePath "Optional path to an IP assignment file. If not specified, it only loads `lo = [127.0.0.0/8]`." , routingtbl :: Maybe FilePath "Optional path to a routing table." - , table :: Maybe String "The table to load for analysis. Default: `filter`. Note: This tool does not support packet modification, so loading tables such as `nat` will most likeley fail." + , table :: Maybe String "The table to load for analysis. Default: `filter`. Note: This tool does not support packet modification, so loading tables such as `nat` will most likely fail." , chain :: Maybe String "The chain to start the analysis. Default: `FORWARD`. Use `INPUT` for a host-based firewall." --TODO: we need some grouping for specific options for the analysis -- For example ./fffuu --analysis service-matrix --sport 424242 --analysis spoofing --foo diff --git a/haskell_tool/test/Suites/GoldenFiles/help b/haskell_tool/test/Suites/GoldenFiles/help index 5667e92e..199b3885 100644 --- a/haskell_tool/test/Suites/GoldenFiles/help +++ b/haskell_tool/test/Suites/GoldenFiles/help @@ -21,7 +21,7 @@ Available options: --routingtbl STRING Optional path to a routing table. --table STRING The table to load for analysis. Default: `filter`. Note: This tool does not support packet modification, - so loading tables such as `nat` will most likeley + so loading tables such as `nat` will most likely fail. --chain STRING The chain to start the analysis. Default: `FORWARD`. Use `INPUT` for a host-based firewall. From 772b76bfe1aaf835bb3d09ff0e9919b3b9d4f327 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:40 -0400 Subject: [PATCH 47/87] spelling: match Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Firewall_Common.thy | 2 +- thy/Iptables_Semantics/Matching.thy | 2 +- thy/Iptables_Semantics/Semantics_Ternary/Matching_Ternary.thy | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/thy/Iptables_Semantics/Firewall_Common.thy b/thy/Iptables_Semantics/Firewall_Common.thy index 536093a3..0a15d591 100644 --- a/thy/Iptables_Semantics/Firewall_Common.thy +++ b/thy/Iptables_Semantics/Firewall_Common.thy @@ -130,7 +130,7 @@ text\Structural properties about match expressions\ "matcheq_matchNone (MatchNot (MatchAnd m1 m2)) \ matcheq_matchNone (MatchNot m1) \ matcheq_matchNone (MatchNot m2)" | "matcheq_matchNone (MatchAnd m1 m2) \ matcheq_matchNone m1 \ matcheq_matchNone m2" - lemma matachAny_matchNone: "\ has_primitive m \ matcheq_matchAny m \ \ matcheq_matchNone m" + lemma matchAny_matchNone: "\ has_primitive m \ matcheq_matchAny m \ \ matcheq_matchNone m" by(induction m rule: matcheq_matchNone.induct)(simp_all) lemma matcheq_matchNone_no_primitive: "\ has_primitive m \ matcheq_matchNone (MatchNot m) \ \ matcheq_matchNone m" diff --git a/thy/Iptables_Semantics/Matching.thy b/thy/Iptables_Semantics/Matching.thy index 480cd61d..9617b650 100644 --- a/thy/Iptables_Semantics/Matching.thy +++ b/thy/Iptables_Semantics/Matching.thy @@ -23,7 +23,7 @@ lemma matcheq_matchAny: "\ has_primitive m \ matcheq_matchA by(induction m) simp_all lemma matcheq_matchNone: "\ has_primitive m \ matcheq_matchNone m \ \ matches \ m p" - by(auto dest: matcheq_matchAny matachAny_matchNone) + by(auto dest: matcheq_matchAny matchAny_matchNone) lemma matcheq_matchNone_not_matches: "matcheq_matchNone m \ \ matches \ m p" by(induction m rule: matcheq_matchNone.induct) auto diff --git a/thy/Iptables_Semantics/Semantics_Ternary/Matching_Ternary.thy b/thy/Iptables_Semantics/Semantics_Ternary/Matching_Ternary.thy index 35b2f9a1..d55e893a 100644 --- a/thy/Iptables_Semantics/Semantics_Ternary/Matching_Ternary.thy +++ b/thy/Iptables_Semantics/Semantics_Ternary/Matching_Ternary.thy @@ -379,7 +379,7 @@ begin qed lemma matcheq_matchNone: "\ has_primitive m \ matcheq_matchNone m \ \ matches \ m a p" - by(auto dest: matcheq_matchAny matachAny_matchNone) + by(auto dest: matcheq_matchAny matchAny_matchNone) lemma matcheq_matchNone_not_matches: "matcheq_matchNone m \ \ matches \ m a p" proof(induction m rule: matcheq_matchNone.induct) From a1de73311ac1016c6e89370dc0b951f8475ef4df Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:48 -0400 Subject: [PATCH 48/87] spelling: miscellaneous Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Parametricity/Relators.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Automatic_Refinement/Parametricity/Relators.thy b/thy/Automatic_Refinement/Parametricity/Relators.thy index 924933f7..e66baa55 100644 --- a/thy/Automatic_Refinement/Parametricity/Relators.thy +++ b/thy/Automatic_Refinement/Parametricity/Relators.thy @@ -758,7 +758,7 @@ lemma sv_add_invar: -subsection {* Miscellanneous *} +subsection {* Miscellaneous *} lemma rel_cong: "(f,g)\Id \ (x,y)\Id \ (f x, g y)\Id" by simp lemma rel_fun_cong: "(f,g)\Id \ (f x, g x)\Id" by simp lemma rel_arg_cong: "(x,y)\Id \ (f x, f y)\Id" by simp From 7f84902867ff1be31c2ee00ac6eacb3e1deca846 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:53 -0400 Subject: [PATCH 49/87] spelling: network Signed-off-by: Josh Soref --- thy/LOFT/Examples/OF_conv_test/3chn.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/Examples/OF_conv_test/3chn.py b/thy/LOFT/Examples/OF_conv_test/3chn.py index ede76d9d..cf552c40 100755 --- a/thy/LOFT/Examples/OF_conv_test/3chn.py +++ b/thy/LOFT/Examples/OF_conv_test/3chn.py @@ -164,7 +164,7 @@ def makearpentries(host, hosts): for intf in host.intfList(): if intf.MAC() and intf.IP(): # will also sort out loopback for host in hosts: - host.cmd("arp -s {} {}".format(intf.IP(), intf.MAC())) # will fail with Netwok unreachable at given times. Easier to ignore than fix. + host.cmd("arp -s {} {}".format(intf.IP(), intf.MAC())) # will fail with Network unreachable at given times. Easier to ignore than fix. def standalone(): if "info" in argv: From 9a8d6ac04a7d022976403176055287b626e166dd Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:24:59 -0400 Subject: [PATCH 50/87] spelling: not Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy index bee23717..65f87e85 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy @@ -36,7 +36,7 @@ subsection\Sanity checking for an @{typ "'i ipassignment"}.\ distinct (map fst ipassmt) \ ipassmt_sanity_nowildcards (map_of ipassmt) then map_of ipassmt - else undefined (*undefined_ipassmt_must_be_distinct_and_dont_have_wildcard_interfaces*))" + else undefined (*undefined_ipassmt_must_be_distinct_and_not_have_wildcard_interfaces*))" text\some additional (optional) sanity checks\ From 5116cd400053d102af0013c9540c40b1aaa9a302 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:06 -0400 Subject: [PATCH 51/87] spelling: numeric Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Datatype_Selectors.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Datatype_Selectors.thy b/thy/Iptables_Semantics/Datatype_Selectors.thy index 6f3384e7..70aaaeab 100644 --- a/thy/Iptables_Semantics/Datatype_Selectors.thy +++ b/thy/Iptables_Semantics/Datatype_Selectors.thy @@ -22,7 +22,7 @@ fun wf_disc_sel :: "(('a \ bool) \ ('a \ 'b)) \ (\a. disc (C a)) \ (\a. disc (C a))" *) From 4ea89a336a407c28d78c5658c8db7cb7ffbba589 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:11 -0400 Subject: [PATCH 52/87] spelling: overlapping Signed-off-by: Josh Soref --- thy/LOFT/Semantics_OpenFlow.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/Semantics_OpenFlow.thy b/thy/LOFT/Semantics_OpenFlow.thy index 7fc59987..81a2806c 100644 --- a/thy/LOFT/Semantics_OpenFlow.thy +++ b/thy/LOFT/Semantics_OpenFlow.thy @@ -60,7 +60,7 @@ definition OF_same_priority_match2 :: "('m, 'p) field_matcher \ ('m, | (Suc 0) \ Action (the_elem s) | _ \ Undefined" -(* are there any overlaping rules? *) +(* are there any overlapping rules? *) definition "check_no_overlap \ ft = (\a \ set ft. \b \ set ft. \p \ UNIV. (ofe_prio a = ofe_prio b \ \ (ofe_fields a) p \ a \ b) \ \\ (ofe_fields b) p)" definition "check_no_overlap2 \ ft = (\a \ set ft. \b \ set ft. (a \ b \ ofe_prio a = ofe_prio b) \ \(\p \ UNIV. \ (ofe_fields a) p \ \ (ofe_fields b) p))" lemma check_no_overlap_alt: "check_no_overlap \ ft = check_no_overlap2 \ ft" From 4ad7ac2c9339db896a290e3412b1dfb610639079 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:18 -0400 Subject: [PATCH 53/87] spelling: parameters Signed-off-by: Josh Soref --- thy/Iptables_Semantics/document/mathpartir.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/document/mathpartir.sty b/thy/Iptables_Semantics/document/mathpartir.sty index f9278dd0..4d1a627b 100644 --- a/thy/Iptables_Semantics/document/mathpartir.sty +++ b/thy/Iptables_Semantics/document/mathpartir.sty @@ -46,7 +46,7 @@ % in mathpar or in inferrule \let \mpr@hva \empty -%% normal paragraph parametters, should rather be taken dynamically +%% normal paragraph parameters, should rather be taken dynamically \def \mpr@savepar {% \edef \MathparNormalpar {\noexpand \lineskiplimit \the\lineskiplimit From edb228733e93681a55f949a81377d5a2a2689da8 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:23 -0400 Subject: [PATCH 54/87] spelling: partitioning Signed-off-by: Josh Soref --- thy/Simple_Firewall/Common/IP_Partition_Preliminaries.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Simple_Firewall/Common/IP_Partition_Preliminaries.thy b/thy/Simple_Firewall/Common/IP_Partition_Preliminaries.thy index 445239c9..475fbf50 100644 --- a/thy/Simple_Firewall/Common/IP_Partition_Preliminaries.thy +++ b/thy/Simple_Firewall/Common/IP_Partition_Preliminaries.thy @@ -76,7 +76,7 @@ context begin private lemma coversallAddSubset:"\ (insert a ts) = \ (addSubsetSet a ts)" by (auto simp add: addSubsetSet_def) - private lemma ipPartioningAddSubset0: "disjoint ts \ ipPartition ts (addSubsetSet a ts)" + private lemma ipPartitioningAddSubset0: "disjoint ts \ ipPartition ts (addSubsetSet a ts)" apply(simp add: addSubsetSet_def ipPartition_def) apply(safe) apply blast @@ -175,7 +175,7 @@ context begin case Nil thus ?case by(simp add: ipPartition_def) next case (Cons t ts) - from Cons.prems ipPartioningAddSubset0 have d: "ipPartition As (addSubsetSet t As)" by blast + from Cons.prems ipPartitioningAddSubset0 have d: "ipPartition As (addSubsetSet t As)" by blast from Cons.prems Cons.IH d disjointAddSubset ipPartitioningAddSubset1 have e: "ipPartition (set ts) (partitioning ts (addSubsetSet t As))" by blast from ipPartitioningAddSubset2 Cons.prems From 2b13e9429b1afe074ed891bf9dce59740b69c460 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:29 -0400 Subject: [PATCH 55/87] spelling: preferred Signed-off-by: Josh Soref --- thy/IP_Addresses/IPv6.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/thy/IP_Addresses/IPv6.thy b/thy/IP_Addresses/IPv6.thy index f6503eed..2c17b7fa 100644 --- a/thy/IP_Addresses/IPv6.thy +++ b/thy/IP_Addresses/IPv6.thy @@ -635,14 +635,14 @@ definition ipv6_unparsed_compressed_to_preferred :: "((16 word) option) list \ ipv6addr_c2p ipv6compressed = ipv6prferred" + "ipv6_unparsed_compressed_to_preferred (ipv6addr_syntax_compressed_to_list ipv6compressed) = Some ipv6preferred + \ ipv6addr_c2p ipv6compressed = ipv6preferred" by(cases ipv6compressed) (simp_all add: ipv6_unparsed_compressed_to_preferred_def) (*1s*) lemma ipv6_unparsed_compressed_to_preferred_identity2: - "ipv6_unparsed_compressed_to_preferred ls = Some ipv6prferred + "ipv6_unparsed_compressed_to_preferred ls = Some ipv6preferred \ (\ipv6compressed. parse_ipv6_address_compressed ls = Some ipv6compressed \ - ipv6addr_c2p ipv6compressed = ipv6prferred)" + ipv6addr_c2p ipv6compressed = ipv6preferred)" apply(rule iffI) apply(subgoal_tac "parse_ipv6_address_compressed ls \ None") prefer 2 From 4cd47b18b13ce32ba07cda71ad30d5c3fa0cee33 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:35 -0400 Subject: [PATCH 56/87] spelling: preprocessed Signed-off-by: Josh Soref --- haskell_tool/lib/Network/IPTables/Analysis.hs | 2 +- .../medium-sized-company/Analyze_medium_sized_company.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/haskell_tool/lib/Network/IPTables/Analysis.hs b/haskell_tool/lib/Network/IPTables/Analysis.hs index 59c1ada2..41984b0b 100644 --- a/haskell_tool/lib/Network/IPTables/Analysis.hs +++ b/haskell_tool/lib/Network/IPTables/Analysis.hs @@ -58,7 +58,7 @@ certifySpoofingProtection_generic (IsabelleIpAssmt a -> [Isabelle.Rule (Isabelle.Common_primitive a)] -> [String]) -> IsabelleIpAssmt a -> [Isabelle.Rule (Isabelle.Common_primitive a)] -> ([String], [(Isabelle.Iface, Bool)]) certifySpoofingProtection_generic debug_ipassmt_f ipassmt rs = (warn_defined ++ debug_ipassmt, certResult) - where -- fuc: firewall under certification, prepocessed + where -- fuc: firewall under certification, preprocessed -- no_spoofing_executable_set requires normalized_nnf_match. Isabelle.upper_closure guarantees this. -- It also guarantees that if we start from a simple_ruleset, it remains a simple ruleset. -- Theorem: no_spoofing_executable_set_preprocessed diff --git a/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy b/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy index 57806bf0..4202abe9 100644 --- a/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy +++ b/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy @@ -68,7 +68,7 @@ lemma "simple_fw_valid (to_simple_firewall (lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new unfolded_FORWARD)))))" by eval (* -text{*If we call the IP address spcae partitioning incorrectly (not prepocessed, still has interfaces), we get an error*} +text{*If we call the IP address spcae partitioning incorrectly (not preprocessed, still has interfaces), we get an error*} value[code] " parts_connection_ssh (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded_FORWARD)))))" *) From 2d3cb56dec1de8bf19a350e717820dff2155734d Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:41 -0400 Subject: [PATCH 57/87] spelling: prerequisites Signed-off-by: Josh Soref --- thy/LOFT/OpenFlow_Matches.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/OpenFlow_Matches.thy b/thy/LOFT/OpenFlow_Matches.thy index 0c374e7a..bb48b6b8 100644 --- a/thy/LOFT/OpenFlow_Matches.thy +++ b/thy/LOFT/OpenFlow_Matches.thy @@ -57,7 +57,7 @@ For example: try with oxm_type=OXM_OF_ETH_TYPE, oxm_hasmask=0, and oxm_value=0x0800. That is, match- ing on the IPv4 source address is allowed only if the Ethernet type is explicitly set to IPv4. \ -Even if OpenFlow 1.0 does not require this behavior, some switches may still silently drop matches without prerequsites. +Even if OpenFlow 1.0 does not require this behavior, some switches may still silently drop matches without prerequisites. *) From 46b48f7313ce06f31a2e3a0fbd2fa0eef1271832 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:48 -0400 Subject: [PATCH 58/87] spelling: prettiness Signed-off-by: Josh Soref --- thy/Simple_Firewall/Service_Matrix.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Simple_Firewall/Service_Matrix.thy b/thy/Simple_Firewall/Service_Matrix.thy index 97960335..353c555d 100644 --- a/thy/Simple_Firewall/Service_Matrix.thy +++ b/thy/Simple_Firewall/Service_Matrix.thy @@ -1428,7 +1428,7 @@ the edges are the edges. Result looks nice. Theorem also tells us that this visu vertices = (name, list of ip addresses this vertex corresponds to) and edges = (name \ name) list - Note that the WordInterval is already sorted, which is important for prettyness! + Note that the WordInterval is already sorted, which is important for prettiness! *) text\Only defined for @{const simple_firewall_without_interfaces}\ definition access_matrix_pretty_ipv4 From 37dd905eef2d60a4b547c3a0a9b45757191439a2 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:52 -0400 Subject: [PATCH 59/87] spelling: primitive Signed-off-by: Josh Soref --- .../Primitive_Matchers/Interfaces_Normalize.thy | 4 ++-- .../Primitive_Matchers/Protocols_Normalize.thy | 2 +- .../Semantics_Ternary/Primitive_Normalization.thy | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Interfaces_Normalize.thy b/thy/Iptables_Semantics/Primitive_Matchers/Interfaces_Normalize.thy index 7ff4d56a..d8349947 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Interfaces_Normalize.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Interfaces_Normalize.thy @@ -135,7 +135,7 @@ begin "normalized_n_primitive (disc, sel) P m \ (\a. \ disc (IIface a)) \ normalized_nnf_match m \ compress_normalize_input_interfaces m = Some m' \ normalized_nnf_match m' \ normalized_n_primitive (disc, sel) P m'" unfolding compress_normalize_input_interfaces_def - using compress_normalize_primitve_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(5)] by blast + using compress_normalize_primitive_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(5)] by blast @@ -208,7 +208,7 @@ begin "normalized_n_primitive (disc, sel) P m \ (\a. \ disc (OIface a)) \ normalized_nnf_match m \ compress_normalize_output_interfaces m = Some m' \ normalized_nnf_match m' \ normalized_n_primitive (disc, sel) P m'" unfolding compress_normalize_output_interfaces_def - using compress_normalize_primitve_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(6)] by blast + using compress_normalize_primitive_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(6)] by blast end diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy b/thy/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy index 6f2a56a2..acefa7bc 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy @@ -199,7 +199,7 @@ lemma "simple_proto_conjunct p1 (Proto p2) \ None \ \ (\a. \ disc (Prot a)) \ normalized_nnf_match m \ compress_normalize_protocols_step m = Some m' \ normalized_nnf_match m' \ normalized_n_primitive (disc, sel) P m'" unfolding compress_normalize_protocols_step_def - using compress_normalize_primitve_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(7)] by blast + using compress_normalize_primitive_preserves_normalized_n_primitive[OF _ wf_disc_sel_common_primitive(7)] by blast lemma "case compress_normalize_protocols_step diff --git a/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy b/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy index 20fdb8ff..25e45388 100644 --- a/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy +++ b/thy/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy @@ -866,7 +866,7 @@ subsection\Optimizing a match expression\ thm normalize_primitive_extract_preserves_unrelated_normalized_n_primitive (*is similar*) - lemma compress_normalize_primitve_preserves_normalized_n_primitive: + lemma compress_normalize_primitive_preserves_normalized_n_primitive: assumes am: "normalized_n_primitive (disc2, sel2) P m" and wf: "wf_disc_sel (disc,sel) C" and disc: "(\a. \ disc2 (C a))" From 33c6d025ce714ddbcaf062e6caf2ee737e079d6b Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:25:57 -0400 Subject: [PATCH 60/87] spelling: redefined Signed-off-by: Josh Soref --- thy/LOFT/document/moeptikz.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/document/moeptikz.sty b/thy/LOFT/document/moeptikz.sty index 02be8479..117f3bfc 100644 --- a/thy/LOFT/document/moeptikz.sty +++ b/thy/LOFT/document/moeptikz.sty @@ -1517,7 +1517,7 @@ messageclosed/.default={1cm,black!30,black} } -% Redfined checkerboard decoration with better image quality than the default +% Redefined checkerboard decoration with better image quality than the default \pgfdeclarepatternformonly[\CheckerSize]{moepcheckerboard}% name {\pgfqpoint{0mm}{0mm}}% origin {\pgfqpoint{2\CheckerSize}{2\CheckerSize}}% top right From 0396f282c77d5da9ebb9f9a0901b0bad5ff6a2ef Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:04 -0400 Subject: [PATCH 61/87] spelling: related Signed-off-by: Josh Soref --- .../Examples/TUM_Net_Firewall/README_cheating | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating b/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating index 46fd84d2..a08161a8 100644 --- a/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating +++ b/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating @@ -18,7 +18,7 @@ diff -u iptables_20.11.2013 iptables_20.11.2013_cheating The rule was simply dead. We suffix everything which is based on this modified rulset (with those three rules removed) '_cheating'. -In earlier versions, we also remove the ESTABLISHED;REALTED rule. Details why this is (was) reasonable can be found in the paper: +In earlier versions, we also remove the ESTABLISHED;RELATED rule. Details why this is (was) reasonable can be found in the paper: http://www.net.in.tum.de/fileadmin/bibtex/publications/papers/fm15_Semantics-Preserving_Simplification_of_Real-World_Firewall_Rule_Sets.pdf From 7a6b148f73420fc1d14de36d182a80268e343779 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:08 -0400 Subject: [PATCH 62/87] spelling: repeatedly Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Lib/Refine_Util.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Automatic_Refinement/Lib/Refine_Util.thy b/thy/Automatic_Refinement/Lib/Refine_Util.thy index dccad1de..b080e9f7 100644 --- a/thy/Automatic_Refinement/Lib/Refine_Util.thy +++ b/thy/Automatic_Refinement/Lib/Refine_Util.thy @@ -637,7 +637,7 @@ ML {* "resolve with premises" #> Method.setup @{binding elim_all} (Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (elim_all_tac ctxt thms))) - "repeteadly apply elimination rules to all subgoals" + "repeatedly apply elimination rules to all subgoals" #> Method.setup @{binding subst_tac} eqsubst_inst_meth "single-step substitution (dynamic instantiation)" #> Method.setup @{binding clarsimp_all} ( From e0bd9bcd3291af5699e32d26bdc0cf31460d5917 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:13 -0400 Subject: [PATCH 63/87] spelling: repository Signed-off-by: Josh Soref --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c6224640..1b358f00 100644 --- a/README.md +++ b/README.md @@ -54,7 +54,7 @@ See README.md in [haskell_tool](./haskell_tool/). * Cornelius Diekmann, Lukas Schwaighofer, and Georg Carle. *Certifying spoofing-protection of firewalls.* In 11th International Conference on Network and Service Management, CNSM, Barcelona, Spain, November 2015. [[preprint]](http://www.net.in.tum.de/fileadmin/bibtex/publications/papers/diekmann2015_cnsm.pdf), [[ieee | paywall]](http://ieeexplore.ieee.org/document/7367354/) * Cornelius Diekmann, Lars Hupel, and Georg Carle. *Semantics-Preserving Simplification of Real-World Firewall Rule Sets.* In 20th International Symposium on Formal Methods, June 2015. [[preprint]](http://www.net.in.tum.de/fileadmin/bibtex/publications/papers/fm15_Semantics-Preserving_Simplification_of_Real-World_Firewall_Rule_Sets.pdf), [[springer | paywall]](http://link.springer.com/chapter/10.1007%2F978-3-319-19249-9_13) -The raw data of the iptables rulesets from the Examples is stored in [this](https://github.com/diekmann/net-network) repositoy. +The raw data of the iptables rulesets from the Examples is stored in [this](https://github.com/diekmann/net-network) repository. --- From 6f0103d7a1a6d2a6a1bbeb731ff59be69ddd5001 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:18 -0400 Subject: [PATCH 64/87] spelling: result Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy b/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy index b5cfdec6..26d25a6e 100644 --- a/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy +++ b/thy/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy @@ -351,7 +351,7 @@ fun normalized_nnf_match :: "'a match_expr \ bool" where text\Essentially, @{term normalized_nnf_match} checks for a negation normal form: Only AND is at toplevel, negation only occurs in front of literals. Since @{typ "'a match_expr"} does not support OR, the result is in conjunction normal form. - Applying @{const normalize_match}, the reuslt is a list. Essentially, this is the disjunctive normal form.\ + Applying @{const normalize_match}, the result is a list. Essentially, this is the disjunctive normal form.\ lemma normalize_match_already_normalized: "normalized_nnf_match m \ normalize_match m = [m]" by(induction m rule: normalize_match.induct) (simp)+ From 406668657bb008b22dd7806c5b1e7e4467c918f6 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:24 -0400 Subject: [PATCH 65/87] spelling: ruleset Signed-off-by: Josh Soref --- .../Examples/TUM_Net_Firewall/README_cheating | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating b/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating index a08161a8..15c93ed6 100644 --- a/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating +++ b/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/README_cheating @@ -17,7 +17,7 @@ diff -u iptables_20.11.2013 iptables_20.11.2013_cheating The rule was simply dead. -We suffix everything which is based on this modified rulset (with those three rules removed) '_cheating'. +We suffix everything which is based on this modified ruleset (with those three rules removed) '_cheating'. In earlier versions, we also remove the ESTABLISHED;RELATED rule. Details why this is (was) reasonable can be found in the paper: http://www.net.in.tum.de/fileadmin/bibtex/publications/papers/fm15_Semantics-Preserving_Simplification_of_Real-World_Firewall_Rule_Sets.pdf From 060af594e827c7f7c949a267aeda8cf0689cbd4e Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:29 -0400 Subject: [PATCH 66/87] spelling: satisfied Signed-off-by: Josh Soref --- thy/LOFT/LinuxRouter_OpenFlow_Translation.thy | 2 +- thy/LOFT/OpenFlow_Documentation.thy | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/thy/LOFT/LinuxRouter_OpenFlow_Translation.thy b/thy/LOFT/LinuxRouter_OpenFlow_Translation.thy index 03f630e3..ee3bc54f 100644 --- a/thy/LOFT/LinuxRouter_OpenFlow_Translation.thy +++ b/thy/LOFT/LinuxRouter_OpenFlow_Translation.thy @@ -475,7 +475,7 @@ definition "no_oif_match \ list_all (\m. oiface (match_sel m) = i definition "lr_of_tran rt fw ifs \ if \ (no_oif_match fw \ has_default_policy fw \ simple_fw_valid fw \ valid_prefixes rt \ has_default_route rt \ distinct ifs) - then Inl ''Error in creating OpenFlow table: prerequisites not satisifed'' + then Inl ''Error in creating OpenFlow table: prerequisites not satisfied'' else ( let nrd = lr_of_tran_fbs rt fw ifs; ard = map (apfst of_nat) (annotate_rlen nrd) (* give them a priority *) diff --git a/thy/LOFT/OpenFlow_Documentation.thy b/thy/LOFT/OpenFlow_Documentation.thy index 80b99de1..7d429811 100644 --- a/thy/LOFT/OpenFlow_Documentation.thy +++ b/thy/LOFT/OpenFlow_Documentation.thy @@ -396,7 +396,7 @@ text_raw\ \ lemma "lr_of_tran rt fw ifs \ if \ (no_oif_match fw \ has_default_policy fw \ simple_fw_valid fw \ valid_prefixes rt \ has_default_route rt \ distinct ifs) - then Inl ''Error in creating OpenFlow table: prerequisites not satisifed'' + then Inl ''Error in creating OpenFlow table: prerequisites not satisfied'' else ( let nfw = map simple_rule_dtor fw; @@ -501,7 +501,7 @@ Obviously, we will never see any packets with an input interface that is not in Furthermore, we do not state anything about non-IPv4 traffic. (The traffic will remain unmatched in by the flow table, but we have not verified that.) The last assumption is that the translation does not return a run-time error. The translation will return a run-time error if the rules can not be assigned priorities from a 16 bit integer, -or when one of the following conditions on the input data is not satisifed:\ +or when one of the following conditions on the input data is not satisfied:\ lemma " \ no_oif_match fw \ \ has_default_policy fw \ From 70a17cbe57d7be64c1b303067ed99f4a3ff8704f Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:34 -0400 Subject: [PATCH 67/87] spelling: singleton Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Common/Negation_Type_DNF.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Iptables_Semantics/Common/Negation_Type_DNF.thy b/thy/Iptables_Semantics/Common/Negation_Type_DNF.thy index 3cb34b19..71886bda 100644 --- a/thy/Iptables_Semantics/Common/Negation_Type_DNF.thy +++ b/thy/Iptables_Semantics/Common/Negation_Type_DNF.thy @@ -118,7 +118,7 @@ subsubsection\inverting a DNF\ apply(simp add: map_a_and cnf_to_bool_append dnf_to_bool_append) by blast - lemma cnf_invert_singelton: "cnf_to_bool \ [invert a] \ \ cnf_to_bool \ [a]" by(cases a, simp_all) + lemma cnf_invert_singleton: "cnf_to_bool \ [invert a] \ \ cnf_to_bool \ [a]" by(cases a, simp_all) lemma cnf_singleton_false: "(\a'\set as. \ cnf_to_bool \ [a']) \ \ cnf_to_bool \ as" by(induction \ as rule: cnf_to_bool.induct) (simp_all) @@ -131,7 +131,7 @@ subsubsection\inverting a DNF\ apply(induction d) apply(simp_all) apply(simp add: listprepend_correct) - apply(simp add: cnf_invert_singelton cnf_singleton_false) + apply(simp add: cnf_invert_singleton cnf_singleton_false) done subsubsection\Optimizing\ From f4dfc5faaad74573282cc13a5af07182492fb1aa Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:39 -0400 Subject: [PATCH 68/87] spelling: soundness Signed-off-by: Josh Soref --- thy/Routing/Routing_Table.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Routing/Routing_Table.thy b/thy/Routing/Routing_Table.thy index 0af0a92d..8fd982d6 100644 --- a/thy/Routing/Routing_Table.thy +++ b/thy/Routing/Routing_Table.thy @@ -440,7 +440,7 @@ proof(rule ccontr) from x have "\b2g. x \ wordinterval_to_set b2g \ wordinterval_to_set b2g \ wordinterval_to_set b2 \ (a2, b2g) \ set (routing_port_ranges tbl wordinterval_UNIV)" using iuf(2) by(fastforce simp add: wordinterval_Union) then obtain b2g where b2g: "x \ wordinterval_to_set b2g" "wordinterval_to_set b2g \ wordinterval_to_set b2" "(a2, b2g) \ set (routing_port_ranges tbl wordinterval_UNIV)" by clarsimp - text\Soudness tells us that the both @{term a1} and @{term a2} have to be the result of routing @{term x}.\ + text\Soundness tells us that the both @{term a1} and @{term a2} have to be the result of routing @{term x}.\ note routing_port_ranges_sound[OF b1g(3), unfolded fst_conv snd_conv, OF b1g(1) vpfx] routing_port_ranges_sound[OF b2g(3), unfolded fst_conv snd_conv, OF b2g(1) vpfx] text\A contradiction follows from @{thm dif}.\ with dif show False by simp From 1a3691075efe49f0f44d8c2e5b7ad4d47372b2af Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:43 -0400 Subject: [PATCH 69/87] spelling: space Signed-off-by: Josh Soref --- .../medium-sized-company/Analyze_medium_sized_company.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy b/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy index 4202abe9..c26c9a0a 100644 --- a/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy +++ b/thy/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy @@ -68,7 +68,7 @@ lemma "simple_fw_valid (to_simple_firewall (lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new unfolded_FORWARD)))))" by eval (* -text{*If we call the IP address spcae partitioning incorrectly (not preprocessed, still has interfaces), we get an error*} +text{*If we call the IP address space partitioning incorrectly (not preprocessed, still has interfaces), we get an error*} value[code] " parts_connection_ssh (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded_FORWARD)))))" *) From 05690154a28e141df6c1b6af6938ae12f97e3615 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:47 -0400 Subject: [PATCH 70/87] spelling: specialisations Signed-off-by: Josh Soref --- thy/Word_Lib/Word_Lemmas_32.thy | 2 +- thy/Word_Lib/Word_Lemmas_64.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Word_Lib/Word_Lemmas_32.thy b/thy/Word_Lib/Word_Lemmas_32.thy index b7f6414a..d4750b34 100644 --- a/thy/Word_Lib/Word_Lemmas_32.thy +++ b/thy/Word_Lib/Word_Lemmas_32.thy @@ -290,7 +290,7 @@ lemma cast_chunk_assemble_id_64'[simp]: "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_scast_assemble_id) -(* Specialiasations of down_cast_same for adding to local simpsets. *) +(* Specialisations of down_cast_same for adding to local simpsets. *) lemma cast_down_u64: "(scast::64 word \ 32 word) = (ucast::64 word \ 32 word)" apply (subst down_cast_same[symmetric]) apply (simp add:is_down)+ diff --git a/thy/Word_Lib/Word_Lemmas_64.thy b/thy/Word_Lib/Word_Lemmas_64.thy index e5394a75..c1c66d7a 100644 --- a/thy/Word_Lib/Word_Lemmas_64.thy +++ b/thy/Word_Lib/Word_Lemmas_64.thy @@ -267,7 +267,7 @@ lemma cast_chunk_assemble_id_64'[simp]: "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_scast_assemble_id) -(* Specialiasations of down_cast_same for adding to local simpsets. *) +(* Specialisations of down_cast_same for adding to local simpsets. *) lemma cast_down_u64: "(scast::64 word \ 32 word) = (ucast::64 word \ 32 word)" apply (subst down_cast_same[symmetric]) apply (simp add:is_down)+ From 2fca2935330c45a85200bbf3ed8eed83f28420b1 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:50 -0400 Subject: [PATCH 71/87] spelling: stabilizes Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Firewall_Common.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Firewall_Common.thy b/thy/Iptables_Semantics/Firewall_Common.thy index 0a15d591..3a7a7d56 100644 --- a/thy/Iptables_Semantics/Firewall_Common.thy +++ b/thy/Iptables_Semantics/Firewall_Common.thy @@ -69,7 +69,7 @@ fun opt_MatchAny_match_expr_once :: "'a match_expr \ 'a match_expr" "opt_MatchAny_match_expr_once (MatchAnd _ (MatchNot MatchAny)) = (MatchNot MatchAny)" | "opt_MatchAny_match_expr_once (MatchAnd (MatchNot MatchAny) _) = (MatchNot MatchAny)" | "opt_MatchAny_match_expr_once (MatchAnd m1 m2) = MatchAnd (opt_MatchAny_match_expr_once m1) (opt_MatchAny_match_expr_once m2)" -(* without recursive call: need to apply multiple times until it stabelizes *) +(* without recursive call: need to apply multiple times until it stabilizes *) text\It is still a good idea to apply @{const opt_MatchAny_match_expr_once} multiple times. Example:\ From bfb0b81a0a1f70d85713b37b14ab95e9b815037d Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:55 -0400 Subject: [PATCH 72/87] spelling: succeeded Signed-off-by: Josh Soref --- thy/Native_Word/Uint_Userguide.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Native_Word/Uint_Userguide.thy b/thy/Native_Word/Uint_Userguide.thy index dd83a48e..4fa1703e 100644 --- a/thy/Native_Word/Uint_Userguide.thy +++ b/thy/Native_Word/Uint_Userguide.thy @@ -266,7 +266,7 @@ text {* semantics (code equations @{thm [source] eval.simps} and @{thm [source] step.equation}, respectively). - We check that the adaptation has suceeded by exporting the functions. + We check that the adaptation has succeeded by exporting the functions. As we only use native word sizes that PolyML supports, we can use the usual target @{text "SML"} instead of @{text "SML_word"}. *} From 6befcb7a7ceb0b37a2d2375d92c196d5f8940188 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:26:58 -0400 Subject: [PATCH 73/87] spelling: superseded Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Lib/Misc.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Automatic_Refinement/Lib/Misc.thy b/thy/Automatic_Refinement/Lib/Misc.thy index 550dd323..832f46bf 100644 --- a/thy/Automatic_Refinement/Lib/Misc.thy +++ b/thy/Automatic_Refinement/Lib/Misc.thy @@ -6,7 +6,7 @@ (* CHANGELOG: - 2010-05-09: Removed AC, AI locales, they are superseeded by concepts + 2010-05-09: Removed AC, AI locales, they are superseded by concepts from OrderedGroups 2010-09-22: Merges with ext/Aux From 0d839aa31284eb31217098959889cdfd3e010dbb Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:02 -0400 Subject: [PATCH 74/87] spelling: suppresses Signed-off-by: Josh Soref --- thy/Automatic_Refinement/Parametricity/Param_Tool.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Automatic_Refinement/Parametricity/Param_Tool.thy b/thy/Automatic_Refinement/Parametricity/Param_Tool.thy index cb3c8a1a..1ffe5678 100644 --- a/thy/Automatic_Refinement/Parametricity/Param_Tool.thy +++ b/thy/Automatic_Refinement/Parametricity/Param_Tool.thy @@ -305,7 +305,7 @@ begin subsection \Convenience Tools\ ML {* - (* Prefix p_ or wrong type supresses generation of relAPP *) + (* Prefix p_ or wrong type suppresses generation of relAPP *) fun cnv_relAPP t = let fun consider (Var ((name,_),T)) = From 8997f158d529b8c636bb9846395eaa8462f9aa99 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:05 -0400 Subject: [PATCH 75/87] spelling: text Signed-off-by: Josh Soref --- thy/LOFT/Examples/OF_conv_test/3chn.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/LOFT/Examples/OF_conv_test/3chn.py b/thy/LOFT/Examples/OF_conv_test/3chn.py index cf552c40..6e28cf60 100755 --- a/thy/LOFT/Examples/OF_conv_test/3chn.py +++ b/thy/LOFT/Examples/OF_conv_test/3chn.py @@ -130,9 +130,9 @@ def build(self): csl = self.addLink(client, switch, intfName2='s1-lan') nhsl = self.addLink(nhost, switch, intfName2='s1-wan') -def dump(ofile, strng): +def dump(ofile, text): with open(ofile, "w") as fo: - fo.write(strng.replace("\r\n","\n")) + fo.write(text.replace("\r\n","\n")) def tcpreachtest(net, client, server, port=80, timeout=2.5): output("TCP {}: {} -> {}: ".format(port, client, server)) From c156b8f851e35fc5e889859ea897dc6596236fac Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:08 -0400 Subject: [PATCH 76/87] spelling: unambiguous Signed-off-by: Josh Soref --- thy/Routing/Routing_Table.thy | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/thy/Routing/Routing_Table.thy b/thy/Routing/Routing_Table.thy index 8fd982d6..cec4c2f2 100644 --- a/thy/Routing/Routing_Table.thy +++ b/thy/Routing/Routing_Table.thy @@ -164,12 +164,12 @@ proof(induction rtbl) qed qed(simp add: unambiguous_routing_def) -lemma unambigous_prefix_routing_weak_mono: +lemma unambiguous_prefix_routing_weak_mono: assumes lpfx: "is_longest_prefix_routing (rr#rtbl)" assumes e:"rr' \ set rtbl" shows "routing_rule_sort_key rr' \ routing_rule_sort_key rr" using assms by(simp add: linorder_class.sorted_Cons is_longest_prefix_routing_def) -lemma unambigous_prefix_routing_strong_mono: +lemma unambiguous_prefix_routing_strong_mono: assumes lpfx: "is_longest_prefix_routing (rr#rtbl)" assumes uam: "unambiguous_routing (rr#rtbl)" assumes e:"rr' \ set rtbl" @@ -177,7 +177,7 @@ lemma unambigous_prefix_routing_strong_mono: shows "routing_rule_sort_key rr' > routing_rule_sort_key rr" proof - from uam e ne have "routing_rule_sort_key rr \ routing_rule_sort_key rr'" by(fastforce simp add: unambiguous_routing_def) - moreover from unambigous_prefix_routing_weak_mono lpfx e have "routing_rule_sort_key rr \ routing_rule_sort_key rr'" . + moreover from unambiguous_prefix_routing_weak_mono lpfx e have "routing_rule_sort_key rr \ routing_rule_sort_key rr'" . ultimately show ?thesis by simp qed @@ -222,7 +222,7 @@ next from C have e: "rr' \ set rtbl" using rr' by simp show False proof cases assume eq: "routing_match rr' = routing_match rr" - with e have "routing_rule_sort_key rr < routing_rule_sort_key rr'" using unambigous_prefix_routing_strong_mono[OF Cons.prems(2,4) _ eq] by simp + with e have "routing_rule_sort_key rr < routing_rule_sort_key rr'" using unambiguous_prefix_routing_strong_mono[OF Cons.prems(2,4) _ eq] by simp with True rr' show False by simp next assume ne: "routing_match rr' \ routing_match rr" @@ -230,7 +230,7 @@ next note same_length_prefixes_distinct[OF this(1,2) ne[symmetric] _ True this(3)] moreover have "routing_prefix rr = routing_prefix rr'" (is ?pe) proof - have "routing_rule_sort_key rr < routing_rule_sort_key rr' \ \ prefix_match_semantics (routing_match rr) addr" using rr' by simp - with unambigous_prefix_routing_weak_mono[OF Cons.prems(2) e] True have "routing_rule_sort_key rr = routing_rule_sort_key rr'" by simp + with unambiguous_prefix_routing_weak_mono[OF Cons.prems(2) e] True have "routing_rule_sort_key rr = routing_rule_sort_key rr'" by simp thus ?pe by(simp add: routing_rule_sort_key_def int_of_nat_def) qed ultimately show False . From 1e71eaba6c749c7a17b1a1603548956734efd9e9 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:11 -0400 Subject: [PATCH 77/87] spelling: undefined Signed-off-by: Josh Soref --- thy/LOFT/Featherweight_OpenFlow_Comparison.thy | 6 +++--- thy/LOFT/OpenFlow_Documentation.thy | 2 +- thy/LOFT/Semantics_OpenFlow.thy | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/thy/LOFT/Featherweight_OpenFlow_Comparison.thy b/thy/LOFT/Featherweight_OpenFlow_Comparison.thy index 4bfe4cb2..af3525f5 100644 --- a/thy/LOFT/Featherweight_OpenFlow_Comparison.thy +++ b/thy/LOFT/Featherweight_OpenFlow_Comparison.thy @@ -91,7 +91,7 @@ lemma guha_equal_hlp: apply(simp add: guha_equal_Action[OF no]) apply(simp add: guha_equal_NoAction[OF no]) apply(subgoal_tac False, simp) - apply(simp add: no no_overlaps_not_unefined) + apply(simp add: no no_overlaps_not_undefined) done lemma guha_deterministic1: "guha_table_semantics \ ft p (Some x1) \ \ guha_table_semantics \ ft p None" @@ -120,8 +120,8 @@ lemma guha_equal: using guha_deterministic1 apply fast using guha_deterministic2[OF no] apply blast using guha_deterministic1 apply fast - using no_overlaps_not_unefined[OF no] apply fastforce - using no_overlaps_not_unefined[OF no] apply fastforce + using no_overlaps_not_undefined[OF no] apply fastforce + using no_overlaps_not_undefined[OF no] apply fastforce done lemma guha_nondeterministicD: diff --git a/thy/LOFT/OpenFlow_Documentation.thy b/thy/LOFT/OpenFlow_Documentation.thy index 7d429811..135291e6 100644 --- a/thy/LOFT/OpenFlow_Documentation.thy +++ b/thy/LOFT/OpenFlow_Documentation.thy @@ -316,7 +316,7 @@ We give the following definition:\ lemma "check_no_overlap \ ft = (\a \ set ft. \b \ set ft. (a \ b \ ofe_prio a = ofe_prio b) \ \(\p. \ (ofe_fields a) p \ \ (ofe_fields b) p))" unfolding check_no_overlap_alt check_no_overlap2_def by force text\Together with distinctness of the flow table, this provides the absence of @{term Undefined}\footnote{It is slightly stronger than necessary, overlapping rules might be shadowed and thus never influence the behavior.}:\ lemma "\check_no_overlap \ ft; distinct ft\ \ - OF_priority_match \ ft p \ Undefined" by (simp add: no_overlapsI no_overlaps_not_unefined) + OF_priority_match \ ft p \ Undefined" by (simp add: no_overlapsI no_overlaps_not_undefined) text\Given the absence of overlapping or duplicate flow entries, we can show two interesting equivalences. the first is the equality to the semantics defined by Guha \emph{et al.}:\ diff --git a/thy/LOFT/Semantics_OpenFlow.thy b/thy/LOFT/Semantics_OpenFlow.thy index 81a2806c..c7dd4945 100644 --- a/thy/LOFT/Semantics_OpenFlow.thy +++ b/thy/LOFT/Semantics_OpenFlow.thy @@ -68,7 +68,7 @@ lemma check_no_overlap_alt: "check_no_overlap \ ft = check_no_overlap2 \< by blast (* If there are no overlapping rules, our match should check out. *) -lemma no_overlap_not_unefined: "check_no_overlap \ ft \ OF_same_priority_match2 \ ft p \ Undefined" +lemma no_overlap_not_undefined: "check_no_overlap \ ft \ OF_same_priority_match2 \ ft p \ Undefined" proof assume goal1: "check_no_overlap \ ft" "OF_same_priority_match2 \ ft p = Undefined" let ?as = "{f. f \ set ft \ \ (ofe_fields f) p \ (\fo \ set ft. ofe_prio f < ofe_prio fo \ \ \ (ofe_fields fo) p)}" @@ -363,7 +363,7 @@ lemma OF_spm3_noa_none: unfolding OF_eq_sort[OF no] by(drule OF_lm_noa_none) simp (* repetition of the lemma for definition 2 for definition 3 *) -lemma no_overlaps_not_unefined: "no_overlaps \ ft \ OF_priority_match \ ft p \ Undefined" - using check_no_overlapI no_overlap_not_unefined no_overlaps_defeq by fastforce +lemma no_overlaps_not_undefined: "no_overlaps \ ft \ OF_priority_match \ ft p \ Undefined" + using check_no_overlapI no_overlap_not_undefined no_overlaps_defeq by fastforce end From 01ab93ccd3203a7bcde9873d11e978fbb256ba24 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:13 -0400 Subject: [PATCH 78/87] spelling: unhandled Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy b/thy/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy index 32fafed9..206054fc 100644 --- a/thy/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy +++ b/thy/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy @@ -190,7 +190,7 @@ fun approximating_bigstep_fun :: "('a, 'p) match_tac \ 'p \ Decision FinalDeny | Log \ approximating_bigstep_fun \ p rs Undecided | Empty \ approximating_bigstep_fun \ p rs Undecided - (*unhalndled cases*) + (*unhandled cases*) )" From b9afea5ecebd92e3ff90fd47ec2e84b7c1502377 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:17 -0400 Subject: [PATCH 79/87] spelling: unknown Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy | 4 ++-- thy/Iptables_Semantics/Primitive_Matchers/Conntrack_State.thy | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy b/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy index 922e1bb3..7a40ff8a 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy @@ -106,7 +106,7 @@ begin IIface (Iface ''foobar''), Extra ''--name DEFAULT --rsource'']" by eval - private lemma eval_ternary_And_Unknown_Unkown: + private lemma eval_ternary_And_Unknown_Unknown: "eval_ternary_And TernaryUnknown (eval_ternary_And TernaryUnknown tv) = eval_ternary_And TernaryUnknown tv" by(cases tv) (simp_all) @@ -127,7 +127,7 @@ begin case (2 a1 a2) thus ?case apply(simp add: is_pos_Extra_alist_and) apply(cases a1) - apply(simp_all add: eval_ternary_And_Unknown_Unkown) + apply(simp_all add: eval_ternary_And_Unknown_Unknown) done next case 3 thus ?case by(simp) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Conntrack_State.thy b/thy/Iptables_Semantics/Primitive_Matchers/Conntrack_State.thy index 2245f485..1b273c5a 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Conntrack_State.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Conntrack_State.thy @@ -29,7 +29,7 @@ function ctstate_set_toString_list :: "ctstate set \ string list" wh if CT_New \ S then ''NEW''#ctstate_set_toString_list (S - {CT_New}) else if CT_Established \ S then ''ESTABLISHED''#ctstate_set_toString_list (S - {CT_Established}) else if CT_Related \ S then ''RELATED''#ctstate_set_toString_list (S - {CT_Related}) else - if CT_Untracked \ S then ''UNTRACKED''#ctstate_set_toString_list (S - {CT_Untracked}) else [''ERROR-unkown-ctstate''])" + if CT_Untracked \ S then ''UNTRACKED''#ctstate_set_toString_list (S - {CT_Untracked}) else [''ERROR-unknown-ctstate''])" by(pat_completeness) auto termination ctstate_set_toString_list From 76f4ac582cf89774b10cf1f81667bea88a29f079 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:23 -0400 Subject: [PATCH 80/87] spelling: unlabeled Signed-off-by: Josh Soref --- haskell_tool/lib/Network/IPTables/Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/haskell_tool/lib/Network/IPTables/Main.hs b/haskell_tool/lib/Network/IPTables/Main.hs index 3812924a..fb9ae276 100644 --- a/haskell_tool/lib/Network/IPTables/Main.hs +++ b/haskell_tool/lib/Network/IPTables/Main.hs @@ -56,7 +56,7 @@ data CommandLineArgsLabeled = CommandLineArgsLabeled instance ParseRecord CommandLineArgsLabeled --- unlabeld, mandatory command line arguments. For example: ./fffuu "path/to/iptables-save" +-- unlabeled, mandatory command line arguments. For example: ./fffuu "path/to/iptables-save" -- http://stackoverflow.com/questions/36375556/haskell-unnamed-command-line-arguments-for-optparse-generic/36382477#36382477 data CommandLineArgsUnlabeled = CommandLineArgsUnlabeled (FilePath "Required: Path to `iptables-save` output. This is the input for this tool.") From 12954f6a3ae88a12664f59f74b2ddcc8684cf3d5 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:27 -0400 Subject: [PATCH 81/87] spelling: unsupported Signed-off-by: Josh Soref --- haskell_tool/lib/Network/IPTables/Ruleset.hs | 2 +- .../GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating | 4 ++-- .../sqrl_2015_aug_iptables-save-spoofing-protection | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/haskell_tool/lib/Network/IPTables/Ruleset.hs b/haskell_tool/lib/Network/IPTables/Ruleset.hs index 1336abd1..287496bb 100644 --- a/haskell_tool/lib/Network/IPTables/Ruleset.hs +++ b/haskell_tool/lib/Network/IPTables/Ruleset.hs @@ -168,7 +168,7 @@ checkParsedTables res = mapM_ check tables errormsg t msg = concat ["Table `", t ,"' caught exception: `" , msg , "'. Analysis not possible for this table. " - , "This is probably due to unsupportd actions " + , "This is probably due to unsupported actions " , "(or a bug in the parser)."] success t chain = concat ["Parsed ", show (length chain) , " chains in table ", t, ", a total of " diff --git a/haskell_tool/test/Suites/GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating b/haskell_tool/test/Suites/GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating index 8ccc70ef..a6cc13c4 100644 --- a/haskell_tool/test/Suites/GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating +++ b/haskell_tool/test/Suites/GoldenFiles/i8_iptables-save-2015-05-15_15-23-41_cheating @@ -2,8 +2,8 @@ Parsed IpAssmt IpAssmt [(eth0,Pos [0.0.0.0-255.255.255.255]),(foo,Pos []),(eth1.96,Pos [131.159.14.3/25]),(eth1.108,Pos [131.159.14.129/26]),(eth1.109,Pos [131.159.20.11/24]),(eth1.110,Neg [131.159.14.0/23,131.159.20.0/23,192.168.212.0/23,188.95.233.0/24,188.95.232.192/27,188.95.234.0/23,192.48.107.0/24,188.95.236.0/22,185.86.232.0/22]),(eth1.116,Pos [131.159.15.131/26]),(eth1.152,Pos [131.159.15.252/28]),(eth1.171,Pos [131.159.15.2/26]),(eth1.173,Pos [131.159.21.252/24]),(eth1.1010,Pos [131.159.15.227/28]),(eth1.1011,Pos [131.159.14.194/27]),(eth1.1012,Pos [131.159.14.238/28]),(eth1.1014,Pos [131.159.15.217/27]),(eth1.1016,Pos [131.159.15.66/26]),(eth1.1017,Pos [131.159.14.242/28]),(eth1.1111,Pos [192.168.212.4/24]),(eth1.97,Pos [188.95.233.2/24]),(eth1.1019,Pos [188.95.234.2/23]),(eth1.1020,Pos [192.48.107.2/24]),(eth1.1023,Pos [188.95.236.2/22]),(eth1.1025,Pos [185.86.232.2/22]),(eth1.1024,Neg [131.159.14.0/23,131.159.20.0/23,192.168.212.0/23,188.95.233.0/24,188.95.232.192/27,188.95.234.0/23,192.48.107.0/24,188.95.236.0/22,185.86.232.0/22])] == Checking which tables are supported for analysis. Usually, only `filter'. == Parsed 90 chains in table filter, a total of 4813 rules -Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser). -Table `raw' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser). +Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser). +Table `raw' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser). == Transformed to Isabelle type (only filter table) == == unfolded FORWARD chain (upper closure) == (-m state --state ESTABLISHED,RELATED,UNTRACKED, -j ACCEPT) diff --git a/haskell_tool/test/Suites/GoldenFiles/sqrl_2015_aug_iptables-save-spoofing-protection b/haskell_tool/test/Suites/GoldenFiles/sqrl_2015_aug_iptables-save-spoofing-protection index 8d25dc2c..0baec188 100644 --- a/haskell_tool/test/Suites/GoldenFiles/sqrl_2015_aug_iptables-save-spoofing-protection +++ b/haskell_tool/test/Suites/GoldenFiles/sqrl_2015_aug_iptables-save-spoofing-protection @@ -134,8 +134,8 @@ INFO: Officially, we only support the filter table. You requested the `raw' tabl INFO: Officially, we only support the chains FORWARD, INPUT, OUTPUT. You requested the `PREROUTING' chain. Let's see what happens ;-) == Checking which tables are supported for analysis. Usually, only `filter'. == Parsed 7 chains in table filter, a total of 53 rules -Table `mangle' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser). -Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupportd actions (or a bug in the parser). +Table `mangle' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser). +Table `nat' caught exception: `Reading ruleset failed! sanity_wf_ruleset check failed.'. Analysis not possible for this table. This is probably due to unsupported actions (or a bug in the parser). Parsed 3 chains in table raw, a total of 12 rules == Transformed to Isabelle type (only raw table) == [("OUTPUT",[]),("PREROUTING",[(-i lup, -j lupSpoofProtect (call)),(! -s 10.13.42.136/29 -i ldit, -j DROP),(! -s 10.13.42.128/29 -i lmd, -j DROP),(! -s 10.13.42.144/28 -i loben, -j DROP),(! -s 10.13.42.176/28 -i wg, -j DROP),(! -s 10.13.42.160/28 -i wt, -j DROP)]),("lupSpoofProtect",[(-s 192.168.0.0/16, -j DROP),(-s 10.0.0.0/8, -j DROP),(-s 172.16.0.0/12, -j DROP),(-d 192.168.0.0/16, -j DROP),(-d 10.0.0.0/8, -j DROP),(-d 172.16.0.0/12, -j DROP)])] From 0e8b44bd9e6f49506c82d1d234826363d815419b Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:32 -0400 Subject: [PATCH 82/87] spelling: unverified Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy b/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy index 7a40ff8a..9e67d6f4 100644 --- a/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy +++ b/thy/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy @@ -197,7 +197,7 @@ end -(*currently unused and unverifed. may be needed for future use*) +(*currently unused and unverified. may be needed for future use*) definition prefix_to_strange_inverse_cisco_mask:: "nat \ (nat \ nat \ nat \ nat)" where "prefix_to_strange_inverse_cisco_mask n \ dotdecimal_of_ipv4addr ( (NOT (((mask n)::ipv4addr) << (32 - n))) )" lemma "prefix_to_strange_inverse_cisco_mask 8 = (0, 255, 255, 255)" by eval From c017686f44587d38904fffabc2f47919bd47ca0c Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:37 -0400 Subject: [PATCH 83/87] spelling: update Signed-off-by: Josh Soref --- thy/Iptables_Semantics/Semantics_Stateful.thy | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/thy/Iptables_Semantics/Semantics_Stateful.thy b/thy/Iptables_Semantics/Semantics_Stateful.thy index 1a873a0a..94e3d27c 100644 --- a/thy/Iptables_Semantics/Semantics_Stateful.thy +++ b/thy/Iptables_Semantics/Semantics_Stateful.thy @@ -36,15 +36,15 @@ inductive semantics_stateful :: semantics_stateful \ \\<^sub>\ state_update \\<^sub>0 (built_in_chain, default_policy) ps (ps_processed@[(p, X)]) (state_update \' X p)" -lemma semantics_stateful_intro_process_one: "semantics_stateful \ \\<^sub>\ state_upate \\<^sub>0 (built_in_chain, default_policy) (p#ps) ps_processed_old \_old \ +lemma semantics_stateful_intro_process_one: "semantics_stateful \ \\<^sub>\ state_update \\<^sub>0 (built_in_chain, default_policy) (p#ps) ps_processed_old \_old \ \,\\<^sub>\ \_old,p\ \[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy], Undecided\ \ Decision X \ - \' = state_upate \_old X p \ + \' = state_update \_old X p \ ps_processed = ps_processed_old@[(p, X)] \ - semantics_stateful \ \\<^sub>\ state_upate \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" + semantics_stateful \ \\<^sub>\ state_update \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" by(auto intro: semantics_stateful.intros) lemma semantics_stateful_intro_start: "\\<^sub>0 = \' \ ps_processed = [] \ - semantics_stateful \ \\<^sub>\ state_upate \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" + semantics_stateful \ \\<^sub>\ state_update \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" by(auto intro: semantics_stateful.intros) @@ -74,15 +74,15 @@ inductive semantics_stateful_packet_tagging :: lemma semantics_stateful_packet_tagging_intro_start: "\\<^sub>0 = \' \ ps_processed = [] \ - semantics_stateful_packet_tagging \ \ packet_tagger state_upate \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" + semantics_stateful_packet_tagging \ \ packet_tagger state_update \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" by(auto intro: semantics_stateful_packet_tagging.intros) lemma semantics_stateful_packet_tagging_intro_process_one: - "semantics_stateful_packet_tagging \ \ packet_tagger state_upate \\<^sub>0 (built_in_chain, default_policy) (p#ps) ps_processed_old \_old \ + "semantics_stateful_packet_tagging \ \ packet_tagger state_update \\<^sub>0 (built_in_chain, default_policy) (p#ps) ps_processed_old \_old \ \,\,(packet_tagger \_old p)\ \[Rule MatchAny (Call built_in_chain), Rule MatchAny default_policy], Undecided\ \ Decision X \ - \' = state_upate \_old X p \ + \' = state_update \_old X p \ ps_processed = ps_processed_old@[(p, X)] \ - semantics_stateful_packet_tagging \ \ packet_tagger state_upate \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" + semantics_stateful_packet_tagging \ \ packet_tagger state_update \\<^sub>0 (built_in_chain, default_policy) ps ps_processed \'" by(auto intro: semantics_stateful_packet_tagging.intros) From 1837b7cbf423ec52a985e500dad71827d57ea140 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:41 -0400 Subject: [PATCH 84/87] spelling: wellformed Signed-off-by: Josh Soref --- thy/IP_Addresses/IP_Address.thy | 6 +++--- thy/IP_Addresses/Prefix_Match.thy | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/thy/IP_Addresses/IP_Address.thy b/thy/IP_Addresses/IP_Address.thy index 3f810cbe..357daff8 100644 --- a/thy/IP_Addresses/IP_Address.thy +++ b/thy/IP_Addresses/IP_Address.thy @@ -110,7 +110,7 @@ subsection\Sets of IP Addresses\ by(simp add: ipset_from_cidr_alt bitmagic_zeroLast_leq_or1Last) text{*Though we can write 192.168.1.2/24, we say that 192.168.0.0/24 is well-formed.*} - lemma ipset_from_cidr_base_wellforemd: fixes base:: "'i::len word" + lemma ipset_from_cidr_base_wellformed: fixes base:: "'i::len word" assumes "mask (len_of TYPE('i) - l) AND base = 0" shows "ipset_from_cidr base l = {base .. base OR mask (len_of TYPE('i) - l)}" proof - @@ -135,7 +135,7 @@ subsection\Sets of IP Addresses\ proof - have obviously: "mask (len_of TYPE('i) - n) = 0" by (simp add: assms) show ?thesis - apply(subst ipset_from_cidr_base_wellforemd) + apply(subst ipset_from_cidr_base_wellformed) subgoal using assms by simp by (simp add: obviously) qed @@ -172,7 +172,7 @@ subsection\Sets of IP Addresses\ apply(subst ipset_from_cidr_alt2[symmetric]) apply(subst zero_base_lsb_imp_set_eq_as_bit_operation) apply(simp; fail) - apply(subst ipset_from_cidr_base_wellforemd) + apply(subst ipset_from_cidr_base_wellformed) apply(simp; fail) apply(simp) done diff --git a/thy/IP_Addresses/Prefix_Match.thy b/thy/IP_Addresses/Prefix_Match.thy index c243d845..8d2cffa5 100644 --- a/thy/IP_Addresses/Prefix_Match.thy +++ b/thy/IP_Addresses/Prefix_Match.thy @@ -153,7 +153,7 @@ subsection\Equivalence Proofs\ unfolding prefix_match_semantics_wordset[OF assms] unfolding valid_prefix_ipset_from_netmask_ipset_from_cidr unfolding prefix_to_wordset_def - apply(subst ipset_from_cidr_base_wellforemd) + apply(subst ipset_from_cidr_base_wellformed) subgoal using assms by(simp add: valid_prefix_def pfxm_mask_def) by(simp add: pfxm_mask_def) From 71f6f92686c0fbb9f31b605f8e38c290f0b904d3 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:44 -0400 Subject: [PATCH 85/87] spelling: whereas Signed-off-by: Josh Soref --- thy/LOFT/OpenFlow_Documentation.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/LOFT/OpenFlow_Documentation.thy b/thy/LOFT/OpenFlow_Documentation.thy index 135291e6..952048d1 100644 --- a/thy/LOFT/OpenFlow_Documentation.thy +++ b/thy/LOFT/OpenFlow_Documentation.thy @@ -213,7 +213,7 @@ schematic_goal "(field_match :: of_match_field) \ { text\ Two things are worth additional mention: L3 and L4 ``addresses''. The @{term IPv4Src} and @{term IPv4Dst} matches are specified as ``can be subnet masked'' in~\cite{specification10}, - whereras~\cite{specification15} states clearly that arbitrary bitmasks can be used. We took the conservative approach here. + whereas~\cite{specification15} states clearly that arbitrary bitmasks can be used. We took the conservative approach here. Our alteration of @{term L4Src} and @{term L4Dst} is more grave. While~\cite{specification10} does not state anything about layer 4 ports and masks, \cite{specification15} specifically forbids using masks on them. Nevertheless, OpenVSwitch \cite{openvswitch} and some other implementations support them. From d3be6d866f717f6ba30ab38900987cff3ea74eb1 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:48 -0400 Subject: [PATCH 86/87] spelling: which Signed-off-by: Josh Soref --- .../Examples/TUM_Net_Firewall/TUM_Simple_FW.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/TUM_Simple_FW.thy b/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/TUM_Simple_FW.thy index 5c4e5cc0..905dda65 100644 --- a/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/TUM_Simple_FW.thy +++ b/thy/Iptables_Semantics/Examples/TUM_Net_Firewall/TUM_Simple_FW.thy @@ -6,7 +6,7 @@ begin section\Printing various version of the simplified firewall\ - text\We got lucky that we do not need to abstract over the primitives whcih are not supported by the simple firewall\ + text\We got lucky that we do not need to abstract over the primitives which are not supported by the simple firewall\ value[code] "let x = to_simple_firewall (upper_closure (packet_assume_new (unfold_ruleset_FORWARD net_fw_3_FORWARD_default_policy (map_of net_fw_3)))) From 3d47506f19db9e34a5ebe932f1caf0277632cd24 Mon Sep 17 00:00:00 2001 From: Josh Soref Date: Thu, 21 Oct 2021 22:27:52 -0400 Subject: [PATCH 87/87] spelling: wildcard Signed-off-by: Josh Soref --- thy/Simple_Firewall/Primitives/Iface.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/thy/Simple_Firewall/Primitives/Iface.thy b/thy/Simple_Firewall/Primitives/Iface.thy index 05a2fe23..1e38f0d4 100644 --- a/thy/Simple_Firewall/Primitives/Iface.thy +++ b/thy/Simple_Firewall/Primitives/Iface.thy @@ -524,7 +524,7 @@ begin apply(simp_all) done - text\Non-wildacrd interfaces of length @{term n}\ + text\Non-wildcard interfaces of length @{term n}\ private definition non_wildcard_ifaces :: "nat \ string list" where "non_wildcard_ifaces n \ filter (\i. \ iface_name_is_wildcard i) (List.n_lists n all_chars)" @@ -537,7 +537,7 @@ begin private lemma "(\ i \ set (non_wildcard_ifaces n). internal_iface_name_to_set i) = {s::string. length s = n \ \ iface_name_is_wildcard s}" by(simp add: non_wildcard_ifaces) - text\Non-wildacrd interfaces up to length @{term n}\ + text\Non-wildcard interfaces up to length @{term n}\ private fun non_wildcard_ifaces_upto :: "nat \ string list" where "non_wildcard_ifaces_upto 0 = [[]]" | "non_wildcard_ifaces_upto (Suc n) = (non_wildcard_ifaces (Suc n)) @ non_wildcard_ifaces_upto n"