-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhelper.ml
254 lines (220 loc) · 9.15 KB
/
helper.ml
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
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
open Ast
open Proplogic
exception HelperError of string
let number_of_enclaves = 2
let labnotlow = function
| Low -> false
| _ -> true
let is_array_type = function
|BtArray (s,li), _ -> true
| _ -> false
let get_content_type = function
| EBtRef(mu', lt), p -> lt
| _, q ->raise (HelperError "Expected Ref")
let get_mode = function
| EBtRef(mu', lt), p -> mu'
| EBtArray(mu',_,_), p -> mu'
| EBtFunc(mu', _,_,p,u,_,_), q -> mu'
| EBtCond mu', p -> mu'
| _, q ->raise (HelperError "Type has no mode")
let get_mode_var = function
|ModeVar(mu1, l) -> mu1
| _ -> raise (HelperError "Expected Mode variable")
let get_mode_eidlist = function
|ModeVar(mu1, l) -> l
| _ -> raise (HelperError "Expected Mode variable")
let get_prekillset(t:enclabeltype) =
match t with
|EBtFunc(m,gencpre,prekill,p,u, gencpost,postkill), q -> prekill
|_ -> raise (HelperError "")
let get_postkillset(t:enclabeltype) =
match t with
|EBtFunc(m,gencpre,prekill,p,u, gencpost,postkill), q -> postkill
|_ -> raise (HelperError "")
let get_enc_precontext (t:enclabeltype) =
match t with
|EBtFunc(m,gencpre,_,p,u, gencpost,_), q -> gencpre
|_ -> raise (HelperError "")
let get_enc_postcontext (t:enclabeltype) =
match t with
|EBtFunc(m,gencpre,_,p,u, gencpost,_), q -> gencpost
|_ -> raise (HelperError "")
let get_src_precontext (t:labeltype) =
match t with
|BtFunc(gpre,p,u, gpost), q -> gpre
|_ -> raise (HelperError "")
let get_src_postcontext (t:labeltype) =
match t with
|BtFunc(gpre,p,u, gpost), q -> gpost
|_ -> raise (HelperError "")
let invert_encfunctype = function
|EBtFunc(m, gencpre, kpre, p, u, gencpost, kpost), q -> (m, gencpre, kpre, p, u, gencpost, kpost)
| _,q -> raise (HelperError "Expecting function type")
(* Check if base types are same. Ignore policy for comparison
*)
let rec check_src_base_type b1 b2 = match (b1, b2) with
| BtRef lt1, BtRef lt2 -> check_src_base_type (fst lt1) (fst lt2)
| BtFunc (gpre1, p1, u1, gpost1), BtFunc (gpre2, p2, u2, gpost2) ->
let ispreequal = VarLocMap.equal (fun bp1 bp2 ->
begin match (bp1, bp2) with
|((b1, p1), (b2, p2)) ->
if (p1=p2) && (check_src_base_type b1 b2) then true
else false
| _ -> false
end) gpre1 gpre2 in
let ispostequal = VarLocMap.equal (fun bp1 bp2 ->
begin match (bp1, bp2) with
|((b1, p1), (b2, p2)) ->
if (p1=p2) && (check_src_base_type b1 b2) then true
else false
| _ -> false
end ) gpost1 gpost2 in
(* For functions lower bounds should be equal *)
(ispreequal && ispostequal && (p1 = p2) && (VarSet.equal u1 u2))
| BtInt, BtInt -> true
| BtBool, BtBool -> true
| BtCond, BtCond -> true
| BtString, BtString -> true
| BtArray (n1, lt1), BtArray (n2, lt2) -> if n1 = n2 then check_src_base_type (fst lt1) (fst lt2)
else false
| BtPair (bp11, bp12), BtPair (bp21, bp22) -> let fsteq = check_src_base_type bp11 bp21 in
let sndeq = check_src_base_type bp12 bp22 in
if fsteq && sndeq then true
else false
| _ ,_ -> false (* int, bool, cond *)
(* Check if base types are same. What about rho?
Ignore rho and policy for comparison
*)
let rec check_enc_base_type b1 b2 = match (b1, b2) with
| EBtRef (rho1, lt1), EBtRef (rho2, lt2) -> check_enc_base_type (fst lt1) (fst lt2)
| EBtFunc (rho1, gencpre1, kpre1, p1, u1, gencpost1, kpost1), EBtFunc (rho2, gencpre2, kpre2, p2, u2, gencpost2, kpost2) ->
let ispreequal = VarLocMap.equal (fun bp1 bp2 ->
begin match (bp1, bp2) with
|((b1, p1), (b2, p2)) ->
if (p1 =p2) && (check_enc_base_type b1 b2) then true
else false
| _ -> false
end) gencpre1 gencpre2 in
let ispostequal = VarLocMap.equal (fun bp1 bp2 ->
begin match (bp1, bp2) with
|((b1, p1), (b2, p2)) ->
if (p1=p2) && (check_enc_base_type b1 b2) then true
else false
| _ -> false
end ) gencpost1 gencpost2 in
(* For functions lower bounds should be equal *)
(ispreequal && ispostequal && (p1 = p2) && (VarSet.equal u1 u2))
| EBtInt, EBtInt -> true
| EBtBool, EBtBool -> true
| EBtCond rho1, EBtCond rho2 -> true
| EBtString, EBtString -> true
| EBtArray (mu1, n1, lt1), EBtArray (mu2, n2, lt2) -> if n1 = n2 then check_enc_base_type (fst lt1) (fst lt2)
else false
| EBtPair (bp11, bp12), EBtPair (bp21, bp22) -> let fsteq = check_enc_base_type bp11 bp21 in
let sndeq = check_enc_base_type bp12 bp22 in
if fsteq && sndeq then true
else false
| _ ,_ -> false (* int, bool, cond *)
(* ---------- FRESH TYPE VARIABLES ---------- *)
let tvar_cell = ref 1
(* [next_tid ()] generates a fresh type variable *)
let next_tid () : var =
let x = !tvar_cell in
let s = "x" ^ string_of_int x in
incr tvar_cell; s
let next_kvar() : var =
let x = !tvar_cell in
let s = "x" ^ string_of_int x in
let _ = incr tvar_cell in
s
let gen_killset():killset =
let n = number_of_enclaves in
let rec loop k counter =
if counter !=0 then
loop (k@[next_kvar()]) (counter-1)
else
k
in
loop [] n
(* [next_tvar ()] generates a fresh type variable *)
let next_tvar () : mode =
let x = !tvar_cell in
let s = "x" ^ string_of_int x in
let _ = incr tvar_cell in
(* Generate a list of boolean variables indicating the enclave id *)
let eidvarlist = gen_killset () in
ModeVar (s, eidvarlist)
let rec flattenseq s = match s with
|Seq s1 -> s1
| _ -> [s]
(* Returns true when all registers all low *)
let check_typing_context_reg_low (genc1:enccontext) =
VarLocMap.for_all (fun key value -> begin match key with
| Reg x -> begin match (snd value) with
| Low -> true
| _ -> false
end
| _ -> true
end) genc1
let rec countCondConstraints (c:constr2) =
let rec outerloop c2 num_constraints =
let a, b = Constr2.choose c2 in
let c2' = Constr2.remove (a,b) c2 in
let constraints_per_row = 1 in
let totalconstraints = constraints_per_row + num_constraints in
if (Constr2.is_empty c2') then totalconstraints else outerloop c2' totalconstraints
in
if (Constr2.is_empty c) then 0 else outerloop c 0
(* Get list of all pre and post killed enclaves *)
let get_pre_post_killset = function
|TSeq(pc, srcgamma,setu,srcgamma', s,mu,gamma, k, delta, tstmtlistpair, gamma', k') ->
let tstmtlist = fst (List.split tstmtlistpair) in
let rec loop killlist tstmtlist =
begin match tstmtlist with
| [] -> killlist
| TSkip(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')::tail
| TSetcnd(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')::tail
| TAssign (pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')::tail
| TDeclassify(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')::tail
| TUpdate(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')::tail
| TOut(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')::tail
| TIf(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, _, gamma', k')::tail
| TWhile(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')::tail
| TCall(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')::tail->
let klist' = killlist@[(k,k')] in
loop klist' tail
end in
loop [] tstmtlist
| TSkip(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')
| TSetcnd(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')
| TAssign (pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TDeclassify(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TUpdate(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TOut(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TIf(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, _, gamma', k')
| TWhile(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TCall(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')->
[(k, k')]
let get_killed_enclaves_list = function
|TSeq(pc, srcgamma,setu,srcgamma', s,mu,gamma, k, delta, tstmtlistpair, gamma', k') ->
snd (List.split tstmtlistpair)
| TSkip(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')
| TSetcnd(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')
| TAssign (pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TDeclassify(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TUpdate(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TOut(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TIf(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, _, gamma', k')
| TWhile(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, _, gamma', k')
| TCall(pc, srcgamma,setu,srcgamma',s,mu,gamma, k, delta, _, gamma', k')->
[]
let get_enclaves_of_confidential_locations genc =
let confidential_map = VarLocMap.filter (fun key value -> begin match key with
|Reg v -> false
| Mem l -> let lt = get_content_type value in
begin match lt with
| (b, Low) -> false
| _ -> true
end
end ) genc in
VarLocMap.fold (fun key value li -> (li@[get_mode value])) confidential_map []