Skip to content

Commit 19ee799

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
finished the pipeline for a forward proof with sptrees, added small example
1 parent 89a10a2 commit 19ee799

File tree

6 files changed

+530
-112
lines changed

6 files changed

+530
-112
lines changed

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sig‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,6 @@ signature apply_trans_to_IOLib =
22
sig
33
include Abbrev
44

5+
val sptrees_gen_bdds_policy_and_table : term * term * term -> (term * term * term)
6+
57
end

‎hol/policy_to_table/bdd_cake_trans/apply_trans_to_IOLib.sml‎

Lines changed: 42 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -14,21 +14,21 @@ open fromSexpTheory;
1414
val _ = translation_extends "sptrees_bdd_trans_Prog";
1515

1616

17-
1817
val _ = type_abbrev("action_policy_type", “:((string# num list) action_expr) policy”);
1918

19+
20+
fun sptrees_gen_bdds_policy_and_table (var_policy, policy_order, policy_full_order) =
21+
22+
let
23+
2024
Definition policy_order_test_def:
21-
policy_order_test = (["x";"y";"z"]:string list)
25+
policy_order_test = (^policy_order:string list)
2226
End
2327

2428
val r = translate policy_order_test_def;
2529

2630
Definition policy_content_test_def:
27-
policy_content_test = [
28-
(Var "x", action ("allow",[1]));
29-
(And (Var "y") (Var "z"), action ("allow",[2]));
30-
(True, action ("drop",[]))
31-
]:action_policy_type
31+
policy_content_test = (^var_policy:action_policy_type)
3232
End
3333

3434
val r = translate policy_content_test_def;
@@ -84,20 +84,34 @@ val prog =
8484
(Dlet unknown_loc (Pcon NONE [])
8585
(App Opapp [Var (Short "main"); Con NONE []]))
8686
^(get_ml_prog_state() |> get_prog)
87-
`` |> EVAL |> concl |> rhs
87+
`` |> EVAL |> concl |> rhs;
8888

8989

9090

9191
val _ = astToSexprLib.write_ast_to_file "../bdd_cake_test/test_bdd_policy.sexp" prog;
9292

9393

94-
val status = OS.Process.system "cd ../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_policy.sexp > test_bdd_policy.cake.S && cc test_bdd_policy.cake.S basis_ffi.c -lm -o test_bdd_policy.cake -lm && cd ../bdd_cake_test/ && time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt"
94+
val status_compile_sexp = OS.Process.system "cd ../bdd_cake_test/ && CML_STACK_SIZE=2048 CML_HEAP_SIZE=8192 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --jump=false --reg_alg=0 < test_bdd_policy.sexp > test_bdd_policy.cake.S"
9595

96-
val _ = if OS.Process.isSuccess status
96+
val _ = if OS.Process.isSuccess status_compile_sexp
9797
then print "Ja, policy cakeML compilation completed\n"
9898
else (print "Nej, policy cakeML compilation failed\n";
9999
OS.Process.exit OS.Process.failure)
100100

101+
val status_cc = OS.Process.system "cd ../bdd_cake_test/ && cc test_bdd_policy.cake.S basis_ffi.c -lm -o test_bdd_policy.cake -lm"
102+
103+
val _ = if OS.Process.isSuccess status_cc
104+
then print "Ja, policy cc compilation completed\n"
105+
else (print "Nej, policy cc compilation failed\n";
106+
OS.Process.exit OS.Process.failure)
107+
108+
val status_exec = OS.Process.system "cd ../bdd_cake_test/ && time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt";
109+
110+
val _ = if OS.Process.isSuccess status_exec
111+
then print "Ja, policy cc compilation completed\n"
112+
else (print "Nej, policy cc compilation failed\n";
113+
OS.Process.exit OS.Process.failure)
114+
101115

102116

103117
(*
@@ -121,12 +135,12 @@ time ./test_bdd_policy.cake > bdd_policy_cakeml_export.txt
121135

122136

123137
val ins = TextIO.openIn "../bdd_cake_test/bdd_policy_cakeml_export.txt";
124-
val content_str = TextIO.inputAll ins;
138+
val policy_content_str = TextIO.inputAll ins;
125139
val _ = TextIO.closeIn ins;
126140

127141
(*open Term;*)
128142

129-
val content_term =
143+
val policy_bdd_content_term =
130144
let
131145
(* Clean the string by removing newlines and backslash escapes *)
132146
fun clean s =
@@ -139,7 +153,7 @@ val content_term =
139153
String.implode (process chars)
140154
end
141155

142-
val cleaned = clean content_str
156+
val cleaned = clean policy_content_str
143157
val parsed = Parse.Term [QUOTE cleaned]
144158
in
145159
parsed
@@ -149,24 +163,11 @@ end;
149163

150164

151165

152-
153-
val policy_full_order = “[
154-
("A",["x";"y"]);
155-
("B" ,["z"])
156-
]”;
157-
158-
159166
val test_groupings = rhs(concl(EVAL policy_full_order));
160-
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative content_term test_groupings;
161-
167+
val gen_var_table_auto = bdd_utilsLib.bdd_to_tables_iterative policy_bdd_content_term test_groupings;
162168

163169

164170

165-
(*
166-
val eval_table_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^gen_var_table_auto))]) [] ["x";"y";"z"] 1”;
167-
*)
168-
169-
170171
Definition table_content_test_def:
171172
table_content_test = (^gen_var_table_auto : action_table_type)
172173
End
@@ -219,7 +220,7 @@ val prog =
219220
(Dlet unknown_loc (Pcon NONE [])
220221
(App Opapp [Var (Short "main"); Con NONE []]))
221222
^(get_ml_prog_state() |> get_prog)
222-
`` |> EVAL |> concl |> rhs
223+
`` |> EVAL |> concl |> rhs;
223224

224225

225226

@@ -243,14 +244,14 @@ val _ = (max_print_depth := 200);
243244

244245

245246

246-
val ins = TextIO.openIn "../bdd_cake_test/bdd_cake_cakeml_export.txt";
247-
val content_str = TextIO.inputAll ins;
247+
val ins = TextIO.openIn "../bdd_cake_test/bdd_table_cakeml_export.txt";
248+
val tbl_content_str = TextIO.inputAll ins;
248249
val _ = TextIO.closeIn ins;
249250

250251

251252

252253

253-
val content_term =
254+
val table_bdd_content_term =
254255
let
255256
(* Clean the string by removing newlines and backslash escapes *)
256257
fun clean s =
@@ -263,7 +264,7 @@ val content_term =
263264
String.implode (process chars)
264265
end
265266

266-
val cleaned = clean content_str
267+
val cleaned = clean tbl_content_str
267268
val parsed = Parse.Term [QUOTE cleaned]
268269
in
269270
parsed
@@ -272,4 +273,13 @@ end;
272273

273274

274275

276+
277+
278+
279+
in
280+
(policy_bdd_content_term, gen_var_table_auto, table_bdd_content_term)
281+
end;
282+
283+
284+
275285
end;

‎hol/policy_to_table/bdd_cake_trans/internet_firewall_1Script.sml‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
open HolKernel boolLib liteLib simpLib Parse bossLib;
2+
3+
open policy_arith_to_varTheory;
4+
5+
open bdd_utilsLib;
6+
open apply_trans_to_IOLib;
7+
open sptrees_fwd_proofLib;
8+
9+
val _ = new_theory "internet_firewall_1";
10+
11+
12+
13+
val _ = type_abbrev("single_rule", “:((string# num list) action_expr) arith_rule”);
14+
15+
16+
17+
val test_pd_type = “[("h", type_record [("srcPort", type_length 16);
18+
("dstPort", type_length 16);
19+
("srcNAT", type_length 16);
20+
("dstNAT", type_length 16)])]”;
21+
22+
(************************************************)
23+
24+
(* rule 1 *)
25+
26+
val is_srcPort_le_57222 = “(arithm_le (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
27+
val is_srcPort_ge_57222 = “(arithm_ge (lv_acc (lv_x "h") "srcPort") ^(bdd_utilsLib.make_bv 57222 16))”;
28+
29+
val is_dstPort_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
30+
val is_dstPort_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstPort") ^(bdd_utilsLib.make_bv 53 16))”;
31+
32+
val is_srcNAT_le_54587 = “(arithm_le (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
33+
val is_srcNAT_ge_54587 = “(arithm_ge (lv_acc (lv_x "h") "srcNAT") ^(bdd_utilsLib.make_bv 54587 16))”;
34+
35+
val is_dstNAT_le_53 = “(arithm_le (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
36+
val is_dstNAT_ge_53 = “(arithm_ge (lv_acc (lv_x "h") "dstNAT") ^(bdd_utilsLib.make_bv 53 16))”;
37+
38+
39+
val arith_policy_rule1 = “((arith_and (arith_a ^is_srcPort_le_57222)
40+
(arith_and (arith_a ^is_srcPort_ge_57222)
41+
(arith_and (arith_a ^is_dstPort_le_53)
42+
(arith_and (arith_a ^is_dstPort_ge_53)
43+
(arith_and (arith_a ^is_srcNAT_le_54587)
44+
(arith_and (arith_a ^is_srcNAT_ge_54587)
45+
(arith_and (arith_a ^is_dstNAT_le_53)
46+
(arith_a ^is_dstNAT_ge_53)))))))) ,
47+
action ("allow",[1])):single_rule”;
48+
49+
(* Default policy rule *)
50+
val arith_policy_rule_default = “(arith_a a_True, action ("drop", [])):single_rule”;
51+
52+
(* Combined arith policy list *)
53+
val arith_policy = “[
54+
^arith_policy_rule1;
55+
^arith_policy_rule_default
56+
]:single_rule list”;
57+
58+
59+
60+
(* Combined policy mapping *)
61+
val policy_me = “[
62+
("is_srcPort_le_57222", ^is_srcPort_le_57222);
63+
("is_srcPort_ge_57222", ^is_srcPort_ge_57222);
64+
("is_dstPort_le_53", ^is_dstPort_le_53);
65+
("is_dstPort_ge_53", ^is_dstPort_ge_53);
66+
("is_srcNAT_le_54587", ^is_srcNAT_le_54587);
67+
("is_srcNAT_ge_54587", ^is_srcNAT_ge_54587);
68+
("is_dstNAT_le_53", ^is_dstNAT_le_53);
69+
("is_dstNAT_ge_53", ^is_dstNAT_ge_53);
70+
]”;
71+
72+
(* Grouped policy ordering *)
73+
val policy_full_order = “[
74+
("srcPortGrp",["is_srcPort_le_57222";"is_srcPort_ge_57222"]);
75+
("dstPortGrp",["is_dstPort_le_53";"is_dstPort_ge_53"]);
76+
("srcNATGrp" ,["is_srcNAT_le_54587";"is_srcNAT_ge_54587"]);
77+
("dstNATGrp" ,["is_dstNAT_le_53";"is_dstNAT_ge_53"])
78+
]”;
79+
80+
(* Flat policy order (grouped) *)
81+
val policy_order = “["is_srcPort_le_57222"; "is_srcPort_ge_57222"; "is_dstPort_le_53"; "is_dstPort_ge_53"; "is_srcNAT_le_54587"; "is_srcNAT_ge_54587"; "is_dstNAT_le_53"; "is_dstNAT_ge_53"]”;
82+
83+
84+
85+
val _ = sptrees_fwd_proofLib.sptrees_convert_arith_policy_to_interval_tables (arith_policy, policy_me, test_pd_type, policy_full_order, policy_order)
86+
87+
88+
val _ = export_theory ();

0 commit comments

Comments
 (0)