Repository navigation
Expand file tree
/
Copy pathTestingMiniCET.v
More file actions
206 lines (128 loc) · 5.65 KB
/
Copy pathTestingMiniCET.v
File metadata and controls
206 lines (128 loc) · 5.65 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From Stdlib Require Import Strings.String.
From Stdlib Require Import Bool.Bool.
From Stdlib Require Import Arith.Arith.
From Stdlib Require Import Arith.EqNat.
From Stdlib Require Import Arith.PeanoNat. Import Nat.
From Stdlib Require Import Lia.
From Stdlib Require Import List. Import ListNotations.
Set Default Goal Selector "!".
From QuickChick Require Import QuickChick Tactics.
Import QcNotation QcDefaultNotation. Open Scope qc_scope.
Import MonadNotation.
From SECF Require Import MiniCET TaintTracking MapsFunctor TestingLib TestingSemantics.
(*! Section testing_ETE *)
Module Import MCC := MiniCETSemantics ListTotalMap.
Module Import TS := TestingStrategies MCC.
Module Import TT := TaintTracking MCC.
Definition max_block_size := 3.
Definition max_program_length := 8.
Definition gen_dbr : G dir :=
b <- arbitrary;; ret (DBranch b).
Definition gen_dcall (pst: list nat) : G dir :=
l <- (elems_ (0, 0) (proc_hd pst));; ret (DCall l).
Definition wf_ret_addrs (p: prog) : list cptr :=
let fix all_cptrs (l: nat) (blocks: prog) :=
match blocks with
| [] => []
| (blk, _) :: rest => map (fun o => (l, o)) (seq 0 (List.length blk)) ++ all_cptrs (S l) rest
end
in filter (wf_retb p) (all_cptrs 0 p).
Definition gen_dret (p: prog) : G dir :=
l <- elems_ (0, 0) (wf_ret_addrs p);; ret (DRet l).
Instance ShowDirection : Show dir := {
show dir := match dir with
| DBranch b => ("DBranch " ++ show b)%string
| DCall cptr => ("DCall " ++ show cptr)%string
| DRet cptr => ("DRet" ++ show cptr)%string
end
}.
QuickChick (forAll gen_pub_mem (fun P =>
forAll gen_mem (fun s1 =>
forAll (gen_pub_mem_equiv P s1) (fun s2 =>
(checker (pub_equiv_listb P s1 s2))
)))).
QuickChick (forAll gen_pub_vars (fun P =>
forAll gen_state (fun s1 =>
forAll (gen_pub_equiv P s1) (fun s2 =>
pub_equivb P s1 s2
)))).
Definition wt_exp_is_defined := (forAll arbitrary (fun (c : rctx) =>
forAll (gen_reg_wt c [3; 3; 1; 1]) (fun (state: reg) =>
forAll (gen_exp_wt 4 c [3; 3; 1; 1]) (fun (exp : exp) =>
implication (is_defined (eval state exp)) true)))).
(*! QuickChick wt_exp_is_defined. *)
QuickChick wt_exp_is_defined.
Definition basic_block_test := (forAll (basic_block_gen_example) (fun (blk: list inst) => (basic_block_checker blk))).
(*! QuickChick basic_block_test. *)
QuickChick basic_block_test.
Definition wt_wf := (forAll (gen_prog_wt max_block_size max_program_length) (fun (p : prog) => (wf p))).
(*! QuickChick wt_wf. *)
QuickChick wt_wf.
(* should fail *)
Definition wt_uslh_wf := (forAll (gen_prog_wt max_block_size max_program_length) (fun (p : prog) => (wf (uslh_prog p)))).
QuickChick wt_uslh_wf.
Definition wt_expr_is_defined := (
forAll arbitrary (fun (c : rctx) =>
forAll arbitrary (fun (pl : nat) =>
forAll (choose (2, 5)) (fun (exp_sz : nat) =>
pst <- gen_partition pl;;
forAll (gen_reg_wt c pst) (fun (r : reg) =>
forAll (gen_exp_wt exp_sz c pst) (fun (e : exp) =>
is_defined (eval r e)
)))))).
(*! QuickChick wt_expr_is_defined. *)
QuickChick wt_expr_is_defined.
Definition ty_prog_wf :=
(forAll (gen_prog_ty_ctx_wt max_block_size max_program_length) (fun '(c, tm, p) =>
((ty_prog c tm p) && (wf p)))).
Definition load_store_trans_basic_blk := TS.load_store_trans_basic_blk.
(*! QuickChick load_store_trans_basic_blk. *)
QuickChick load_store_trans_basic_blk.
Definition load_store_trans_stuck_free := TS.load_store_trans_stuck_free.
(*! QuickChick load_store_trans_stuck_free. *)
QuickChick load_store_trans_stuck_free.
Definition no_obs_prog_no_obs := TS.no_obs_prog_no_obs.
(*! QuickChick no_obs_prog_no_obs. *)
QuickChick no_obs_prog_no_obs.
Example implicit_flow_test p rs icfg
(P: p = [([ IBranch (AId "x") 1; IJump 1 ], true); ([ IAsgn "y"%string (ANum 1); IRet], false)])
(RS: rs = (N 0, [("x"%string, N 10); ("y"%string, N 0)]))
(ICFG: icfg = (ipc, rs, [], [])):
match taint_tracking 10 p icfg with
| Some (obs, leaked_vars, _) =>
existsb (String.eqb "x") leaked_vars
| None => false
end = true.
Proof.
remember (taint_tracking 10 p icfg).
subst p rs icfg. simpl in Heqo.
subst. simpl. reflexivity.
Qed.
Definition unused_var_no_leak_transform_load_store :=
unused_var_no_leak (fun c tm p => transform_load_store_prog c tm p).
(*! QuickChick unused_var_no_leak_transform_load_store. *)
QuickChick unused_var_no_leak_transform_load_store.
Definition gen_pub_equiv_same_ty := TS.gen_pub_equiv_same_ty.
Definition gen_pub_equiv_is_pub_equiv := TS.gen_pub_equiv_is_pub_equiv.
(*! QuickChick gen_pub_equiv_is_pub_equiv. *)
QuickChick gen_pub_equiv_is_pub_equiv.
Definition gen_reg_wt_is_wt := TS.gen_reg_wt_is_wt.
(*! QuickChick gen_reg_wt_is_wt. *)
QuickChick gen_reg_wt_is_wt.
Definition gen_pub_mem_equiv_is_pub_equiv := TS.gen_pub_mem_equiv_is_pub_equiv.
(*! QuickChick gen_pub_mem_equiv_is_pub_equiv. *)
QuickChick gen_pub_mem_equiv_is_pub_equiv.
Definition gen_mem_wt_is_wt := TS.gen_mem_wt_is_wt.
(*! QuickChick gen_mem_wt_is_wt. *)
QuickChick gen_mem_wt_is_wt.
Definition test_ni_transform_load_store :=
test_ni (fun c tm p => transform_load_store_prog c tm p).
(*! QuickChick test_ni_transform_load_store. *)
QuickChick test_ni_transform_load_store.
Definition test_safety_preservation_uslh := test_safety_preservation uslh_prog gen_dbr gen_dcall gen_dret.
(*! QuickChick test_safety_preservation_uslh. *)
QuickChick test_safety_preservation_uslh.
Definition test_relative_security_uslh := test_relative_security uslh_prog gen_dbr gen_dcall gen_dret.
(*! QuickChick test_relative_security_uslh. *)
QuickChick test_relative_security_uslh.