Skip to content

Commit 04b6d30

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
added further test cases
1 parent ba81f2a commit 04b6d30

File tree

6 files changed

+1675
-0
lines changed

6 files changed

+1675
-0
lines changed

‎hol/policy_to_table/policy_test_cases/internet_firewall_10Script.sml‎

Lines changed: 349 additions & 0 deletions
Large diffs are not rendered by default.

‎hol/policy_to_table/policy_test_cases/internet_firewall_5Script.sml‎

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
3+
open policy_arith_to_varTheory;
4+
5+
open bdd_utilsLib;
6+
open fwd_proofLib;
7+
8+
9+
val _ = new_theory "internet_firewall_5";
10+
11+
val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
12+
13+
val test_pd_type = “[("h", type_record [("srcPort", type_length 16);
14+
("dstPort", type_length 16);
15+
("srcNAT", type_length 16);
16+
("dstNAT", type_length 16)])]”;
17+
18+
(************************************************)
19+
(* rule 1 *)
20+
21+
val is_srcPort_le_57222 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
22+
val is_srcPort_ge_57222 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
23+
24+
val is_dstPort_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
25+
val is_dstPort_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
26+
27+
val is_srcNAT_le_54587 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
28+
val is_srcNAT_ge_54587 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
29+
30+
val is_dstNAT_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
31+
val is_dstNAT_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
32+
33+
34+
val arith_policy_rule1 = “((arith_and (arith_a ^is_srcPort_le_57222)
35+
(arith_and (arith_a ^is_srcPort_ge_57222)
36+
(arith_and (arith_a ^is_dstPort_le_53)
37+
(arith_and (arith_a ^is_dstPort_ge_53)
38+
(arith_and (arith_a ^is_srcNAT_le_54587)
39+
(arith_and (arith_a ^is_srcNAT_ge_54587)
40+
(arith_and (arith_a ^is_dstNAT_le_53)
41+
(arith_a ^is_dstNAT_ge_53)))))))) ,
42+
action ("allow",[])):single_rule”;
43+
44+
(* rule 2 *)
45+
46+
val is_srcPort_le_56258 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 56258 16))”;
47+
val is_srcPort_ge_56258 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 56258 16))”;
48+
49+
val is_dstPort_le_3389 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 3389 16))”;
50+
val is_dstPort_ge_3389 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 3389 16))”;
51+
52+
val is_srcNAT_le_56258 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 56258 16))”;
53+
val is_srcNAT_ge_56258 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 56258 16))”;
54+
55+
val is_dstNAT_le_3389 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 3389 16))”;
56+
val is_dstNAT_ge_3389 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 3389 16))”;
57+
58+
59+
val arith_policy_rule2 = “((arith_and (arith_a ^is_srcPort_le_56258)
60+
(arith_and (arith_a ^is_srcPort_ge_56258)
61+
(arith_and (arith_a ^is_dstPort_le_3389)
62+
(arith_and (arith_a ^is_dstPort_ge_3389)
63+
(arith_and (arith_a ^is_srcNAT_le_56258)
64+
(arith_and (arith_a ^is_srcNAT_ge_56258)
65+
(arith_and (arith_a ^is_dstNAT_le_3389)
66+
(arith_a ^is_dstNAT_ge_3389)))))))) ,
67+
action ("allow",[])):single_rule”;
68+
69+
(* rule 3 *)
70+
71+
val is_srcPort_le_6881 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 6881 16))”;
72+
val is_srcPort_ge_6881 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 6881 16))”;
73+
74+
val is_dstPort_le_50321 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 50321 16))”;
75+
val is_dstPort_ge_50321 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 50321 16))”;
76+
77+
val is_srcNAT_le_43265 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 43265 16))”;
78+
val is_srcNAT_ge_43265 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 43265 16))”;
79+
80+
val is_dstNAT_le_50321 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 50321 16))”;
81+
val is_dstNAT_ge_50321 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 50321 16))”;
82+
83+
84+
val arith_policy_rule3 = “((arith_and (arith_a ^is_srcPort_le_6881)
85+
(arith_and (arith_a ^is_srcPort_ge_6881)
86+
(arith_and (arith_a ^is_dstPort_le_50321)
87+
(arith_and (arith_a ^is_dstPort_ge_50321)
88+
(arith_and (arith_a ^is_srcNAT_le_43265)
89+
(arith_and (arith_a ^is_srcNAT_ge_43265)
90+
(arith_and (arith_a ^is_dstNAT_le_50321)
91+
(arith_a ^is_dstNAT_ge_50321)))))))) ,
92+
action ("allow",[])):single_rule”;
93+
94+
(* rule 4 *)
95+
96+
val is_srcPort_le_50553 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 50553 16))”;
97+
val is_srcPort_ge_50553 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 50553 16))”;
98+
99+
val is_srcNAT_le_50553 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 50553 16))”;
100+
val is_srcNAT_ge_50553 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 50553 16))”;
101+
102+
103+
val arith_policy_rule4 = “((arith_and (arith_a ^is_srcPort_le_50553)
104+
(arith_and (arith_a ^is_srcPort_ge_50553)
105+
(arith_and (arith_a ^is_dstPort_le_3389)
106+
(arith_and (arith_a ^is_dstPort_ge_3389)
107+
(arith_and (arith_a ^is_srcNAT_le_50553)
108+
(arith_and (arith_a ^is_srcNAT_ge_50553)
109+
(arith_and (arith_a ^is_dstNAT_le_3389)
110+
(arith_a ^is_dstNAT_ge_3389)))))))) ,
111+
action ("allow",[])):single_rule”;
112+
113+
(* rule 5 *)
114+
115+
val is_srcPort_le_50002 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 50002 16))”;
116+
val is_srcPort_ge_50002 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 50002 16))”;
117+
118+
val is_dstPort_le_443 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 443 16))”;
119+
val is_dstPort_ge_443 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 443 16))”;
120+
121+
val is_srcNAT_le_45848 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 45848 16))”;
122+
val is_srcNAT_ge_45848 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 45848 16))”;
123+
124+
val is_dstNAT_le_443 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 443 16))”;
125+
val is_dstNAT_ge_443 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 443 16))”;
126+
127+
128+
val arith_policy_rule5 = “((arith_and (arith_a ^is_srcPort_le_50002)
129+
(arith_and (arith_a ^is_srcPort_ge_50002)
130+
(arith_and (arith_a ^is_dstPort_le_443)
131+
(arith_and (arith_a ^is_dstPort_ge_443)
132+
(arith_and (arith_a ^is_srcNAT_le_45848)
133+
(arith_and (arith_a ^is_srcNAT_ge_45848)
134+
(arith_and (arith_a ^is_dstNAT_le_443)
135+
(arith_a ^is_dstNAT_ge_443)))))))) ,
136+
action ("allow",[])):single_rule”;
137+
138+
(* Default policy rule *)
139+
val arith_policy_rule_default = “(arith_a a_True, action ("drop", [])):single_rule”;
140+
141+
(* Combined arith policy list *)
142+
val arith_policy = “[
143+
^arith_policy_rule1;
144+
^arith_policy_rule2;
145+
^arith_policy_rule3;
146+
^arith_policy_rule4;
147+
^arith_policy_rule5;
148+
^arith_policy_rule_default
149+
]:single_rule list”;
150+
151+
152+
153+
(* Combined policy mapping *)
154+
val policy_me = “[
155+
("is_srcPort_le_57222", ^is_srcPort_le_57222);
156+
("is_srcPort_ge_57222", ^is_srcPort_ge_57222);
157+
("is_dstPort_le_53", ^is_dstPort_le_53);
158+
("is_dstPort_ge_53", ^is_dstPort_ge_53);
159+
("is_srcNAT_le_54587", ^is_srcNAT_le_54587);
160+
("is_srcNAT_ge_54587", ^is_srcNAT_ge_54587);
161+
("is_dstNAT_le_53", ^is_dstNAT_le_53);
162+
("is_dstNAT_ge_53", ^is_dstNAT_ge_53);
163+
("is_srcPort_le_56258", ^is_srcPort_le_56258);
164+
("is_srcPort_ge_56258", ^is_srcPort_ge_56258);
165+
("is_dstPort_le_3389", ^is_dstPort_le_3389);
166+
("is_dstPort_ge_3389", ^is_dstPort_ge_3389);
167+
("is_srcNAT_le_56258", ^is_srcNAT_le_56258);
168+
("is_srcNAT_ge_56258", ^is_srcNAT_ge_56258);
169+
("is_dstNAT_le_3389", ^is_dstNAT_le_3389);
170+
("is_dstNAT_ge_3389", ^is_dstNAT_ge_3389);
171+
("is_srcPort_le_6881", ^is_srcPort_le_6881);
172+
("is_srcPort_ge_6881", ^is_srcPort_ge_6881);
173+
("is_dstPort_le_50321", ^is_dstPort_le_50321);
174+
("is_dstPort_ge_50321", ^is_dstPort_ge_50321);
175+
("is_srcNAT_le_43265", ^is_srcNAT_le_43265);
176+
("is_srcNAT_ge_43265", ^is_srcNAT_ge_43265);
177+
("is_dstNAT_le_50321", ^is_dstNAT_le_50321);
178+
("is_dstNAT_ge_50321", ^is_dstNAT_ge_50321);
179+
("is_srcPort_le_50553", ^is_srcPort_le_50553);
180+
("is_srcPort_ge_50553", ^is_srcPort_ge_50553);
181+
("is_srcNAT_le_50553", ^is_srcNAT_le_50553);
182+
("is_srcNAT_ge_50553", ^is_srcNAT_ge_50553);
183+
("is_srcPort_le_50002", ^is_srcPort_le_50002);
184+
("is_srcPort_ge_50002", ^is_srcPort_ge_50002);
185+
("is_dstPort_le_443", ^is_dstPort_le_443);
186+
("is_dstPort_ge_443", ^is_dstPort_ge_443);
187+
("is_srcNAT_le_45848", ^is_srcNAT_le_45848);
188+
("is_srcNAT_ge_45848", ^is_srcNAT_ge_45848);
189+
("is_dstNAT_le_443", ^is_dstNAT_le_443);
190+
("is_dstNAT_ge_443", ^is_dstNAT_ge_443);
191+
]”;
192+
193+
(* Grouped policy ordering *)
194+
val policy_full_order = “[
195+
("srcPortGrp",["is_srcPort_le_57222";"is_srcPort_ge_57222";"is_srcPort_le_56258";"is_srcPort_ge_56258";"is_srcPort_le_6881";"is_srcPort_ge_6881";"is_srcPort_le_50553";"is_srcPort_ge_50553";"is_srcPort_le_50002";"is_srcPort_ge_50002"]);
196+
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53";"is_dstPort_le_3389";"is_dstPort_ge_3389";"is_dstPort_le_50321";"is_dstPort_ge_50321";"is_dstPort_le_443";"is_dstPort_ge_443"]);
197+
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587";"is_srcNAT_le_56258";"is_srcNAT_ge_56258";"is_srcNAT_le_43265";"is_srcNAT_ge_43265";"is_srcNAT_le_50553";"is_srcNAT_ge_50553";"is_srcNAT_le_45848";"is_srcNAT_ge_45848"]);
198+
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53";"is_dstNAT_le_3389";"is_dstNAT_ge_3389";"is_dstNAT_le_50321";"is_dstNAT_ge_50321";"is_dstNAT_le_443";"is_dstNAT_ge_443"])
199+
]”;
200+
201+
(* Flat policy order (grouped) *)
202+
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_srcPort_le_56258"; "is_srcPort_ge_56258"; "is_srcPort_le_6881"; "is_srcPort_ge_6881"; "is_srcPort_le_50553"; "is_srcPort_ge_50553"; "is_srcPort_le_50002"; "is_srcPort_ge_50002"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_dstPort_le_3389"; "is_dstPort_ge_3389"; "is_dstPort_le_50321"; "is_dstPort_ge_50321"; "is_dstPort_le_443"; "is_dstPort_ge_443"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_srcNAT_le_56258"; "is_srcNAT_ge_56258"; "is_srcNAT_le_43265"; "is_srcNAT_ge_43265"; "is_srcNAT_le_50553"; "is_srcNAT_ge_50553"; "is_srcNAT_le_45848"; "is_srcNAT_ge_45848"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"; "is_dstNAT_le_3389"; "is_dstNAT_ge_3389"; "is_dstNAT_le_50321"; "is_dstNAT_ge_50321"; "is_dstNAT_le_443"; "is_dstNAT_ge_443"]”;
203+
204+
(***********************************************)
205+
206+
val final_thm_res =
207+
fwd_proofLib.convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order);
208+
209+
210+
val _ = export_theory ();

0 commit comments

Comments
 (0)