Source file ct_checker_forward.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
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
open Utils
open Prog
module A = Annotations
module S = Syntax
module Pt = Pretyping
module Vl : sig
type t
val compare : t -> t -> int
val is_poly : t -> bool
val mk_uni : string -> t
val mk_poly : string -> t
val pp : Format.formatter -> t -> unit
end = struct
type t =
{ vl_name : string
; vl_flex : bool }
let compare vl1 vl2 = String.compare vl1.vl_name vl2.vl_name
let is_poly vl = not vl.vl_flex
let mk_uni name = { vl_name = name; vl_flex = true }
let mk_poly name = { vl_name = name; vl_flex = false }
let pp fmt vl = Format.fprintf fmt "%s" vl.vl_name
end
module Svl : Set.S with type elt = Vl.t = Set.Make(Vl)
type level =
| Secret
| Poly of Svl.t
| Public
module Lvl : sig
type t = level
val poly1 : Vl.t -> t
val max : t -> t -> t
val maxs : t list -> t
val equal : t -> t -> bool
val le : t -> t -> bool
val pp : Format.formatter -> t -> unit
val parse : single:bool -> A.annotations -> t option
end = struct
type t = level
let poly1 vl = Poly (Svl.singleton vl)
let max l1 l2 =
match l1, l2 with
| Secret, _ | _, Secret -> Secret
| Public, l | l, Public -> l
| Poly l1, Poly l2 -> Poly (Svl.union l1 l2)
let maxs ls = List.fold_left max Public ls
let equal l1 l2 =
match l1, l2 with
| Public, Public -> true
| Secret, Secret -> true
| Poly l1, Poly l2 -> Svl.equal l1 l2
| _, _ -> false
let le l1 l2 =
match l1, l2 with
| Public, _ -> true
| _, Secret -> true
| Poly l1, Poly l2 -> Svl.subset l1 l2
| _, _ -> false
let ssecret = "secret"
let spoly = "poly"
let spublic = "public"
let pp fmt = function
| Secret -> Format.fprintf fmt "#%s" ssecret
| Poly s ->
let l = Svl.elements s in
begin match l with
| [vl] -> Format.fprintf fmt "#%s=%a" spoly Vl.pp vl
| _ -> Format.fprintf fmt "#%s={@[%a@]}" spoly (pp_list ",@ " Vl.pp) l
end
| Public -> Format.fprintf fmt "#%s" spublic
let parse ~(single: bool) (annot: A.annotations) =
let module A = Annot in
let on_struct loc _nid s =
List.iter A.none s;
let s = List.fold_left (fun s (id, _) -> Svl.add (Vl.mk_poly (L.unloc id)) s) Svl.empty s in
if single && Svl.cardinal s <> 1 then
A.error ~loc
"= ident or = { ident } is expected after “%s”" spoly;
Poly s in
let on_id _loc _nid id = poly1 (Vl.mk_poly id) in
let error loc _nid =
A.error ~loc
"= ident or = { ident, ..., ident } is expected after “%s”" spoly in
let poly arg = A.on_attribute ~on_id ~on_struct error arg in
let filters =
[spublic, (fun a -> A.none a; Public);
ssecret, (fun a -> A.none a; Secret);
"transient", (fun a -> A.none a; Public);
spoly , poly] in
A.ensure_uniq filters annot
end
type signature = {
tyin : Lvl.t list;
tyout: Lvl.t list;
}
type ('info, 'asm) fenv = {
ensure_annot : bool;
env_ty : signature Hf.t;
env_def : ('info, 'asm) func list;
}
let pp_arg fmt (x, lvl) =
Format.fprintf fmt "%a %a" Lvl.pp lvl (Printer.pp_var ~debug:false) x
let pp_signature prog fmt (fn, { tyin ; tyout }) =
Format.fprintf fmt "@[<h>@[%s(@[%a@]) ->@ @[%a@]@]@]@."
fn.fn_name
(pp_list ",@ " pp_arg) (List.combine (List.find (fun f -> F.equal f.f_name fn) (snd prog)).f_args tyin)
(pp_list ",@ " Lvl.pp) tyout
exception CtTypeError of Location.t * (Format.formatter -> unit)
let error ~loc =
Format.kdprintf (fun msg ->
raise (CtTypeError (loc, msg)))
module Env : sig
type env
val empty : env
val norm_lvl : env -> Lvl.t -> Lvl.t
val set : env -> var_i -> Lvl.t -> env
val add : env -> var -> Lvl.t -> env
val max : env -> env -> env
val le : env -> env -> bool
val get : public:bool -> env -> var_i -> env * Lvl.t
val gget : public:bool -> env -> int ggvar -> env * Lvl.t
val pp : Format.formatter -> env -> unit
end = struct
type env =
{ env_v : Lvl.t Mv.t
; env_vl : Svl.t }
let empty =
{ env_v = Mv.empty
; env_vl = Svl.empty }
let norm_lvl_aux env_vl = function
| Secret -> Secret
| Public -> Public
| Poly s ->
let s = Svl.diff s env_vl in
if Svl.is_empty s then Public else Poly s
let norm_lvl env lvl = norm_lvl_aux env.env_vl lvl
let get_var env x =
try
let lvl = Mv.find (L.unloc x) env.env_v in
norm_lvl env lvl
with Not_found -> Public
let max env1 env2 =
let env_vl = Svl.union env1.env_vl env2.env_vl in
let merge_lvl _ lvl1 lvl2 =
match lvl1, lvl2 with
| None, _ -> lvl2
| _, None -> lvl1
| Some lvl1, Some lvl2 ->
Some (Lvl.max (norm_lvl_aux env_vl lvl1) (norm_lvl_aux env_vl lvl2))
in
{ env_v = Mv.merge merge_lvl env1.env_v env2.env_v;
env_vl}
let le env1 env2 =
try
let _ =
Mv.merge (fun _ lvl1 lvl2 ->
let lvl1 = Option.default Public lvl1 in
let lvl2 = Option.default Public lvl2 in
let lvl1 = norm_lvl env1 lvl1 in
let lvl2 = norm_lvl env2 lvl2 in
if Lvl.le lvl1 lvl2 then None
else raise Not_found) env1.env_v env2.env_v in
Svl.subset env1.env_vl env2.env_vl
with Not_found -> false
let set env x lvl =
let lvl = norm_lvl env lvl in
{ env with env_v = Mv.add (L.unloc x) lvl env.env_v }
let add env x lvl =
assert (not (Mv.mem x env.env_v));
{ env with env_v = Mv.add x lvl env.env_v }
let get ~(public:bool) env x =
let loc = L.loc x in
let lvl = get_var env x in
if public then
match lvl with
| Secret ->
error ~loc
"%a has type secret it needs to be public"
(Printer.pp_var ~debug:false) (L.unloc x)
| Public -> env, Public
| Poly s ->
let poly = Svl.filter Vl.is_poly s in
if Svl.is_empty poly then { env with env_vl = Svl.union s env.env_vl }, Public
else
error ~loc
"variable %a has type %a, it should be public. Replace the polymorphic variable(s) %a by public"
(Printer.pp_var ~debug:false) (L.unloc x)
Lvl.pp lvl
(pp_list ",@ " Vl.pp) (Svl.elements poly)
else env, lvl
let gget ~(public:bool) env x =
if is_gkvar x then get ~public env x.gv
else env, Public
let pp fmt env =
let pp_ty fmt (x, lvl) =
Format.fprintf fmt "@[%a : %a@]" (Printer.pp_var ~debug:false) x Lvl.pp lvl
in
Format.fprintf fmt "@[<v>type = @[%a@]@ vlevel= @[%a@]@]"
(pp_list ";@ " pp_ty) (Mv.bindings env.env_v)
(pp_list "@ " Vl.pp) (Svl.elements env.env_vl)
end
module UE = struct
type unienv = (Vl.t, level) Hashtbl.t
let create n = Hashtbl.create n
let get (ue:unienv) vl =
try Hashtbl.find ue vl with Not_found -> Public
let set (ue:unienv) s lvl =
assert (Svl.cardinal s = 1);
let vl = Svl.choose s in
Hashtbl.add ue vl (Lvl.max (get ue vl) lvl)
end
let unify uty ety : UE.unienv =
let ue = UE.create 31 in
let doit uty ety =
match uty, ety with
| Public, Public -> ()
| Poly s, _ -> UE.set ue s ety
| Secret, _ -> ()
| _, _ -> assert false in
List.iter2 doit uty ety;
ue
let instanciate ue ty =
match ty with
| Secret | Public -> ty
| Poly s -> Svl.fold (fun vl lvl -> Lvl.max (UE.get ue vl) lvl) s Public
let instanciates ue tyin =
List.map (instanciate ue) tyin
let instanciate_fty fty lvls =
let ue = unify fty.tyin lvls in
let tyout = instanciates ue fty.tyout in
tyout
let is_ct_op1 (_: Expr.sop1) = true
let is_ct_op2 (o: Expr.sop2) =
match o with
| Omod (_, Op_w _) | Odiv (_, Op_w _) -> false
| Owi2(_, _, (WImod | WIdiv)) -> false
| _ -> true
let is_ct_opN (_ : Expr.opN) = true
let is_ct_sopn is_ct_asm (o : 'a Sopn.sopn) =
match o with
| Opseudo_op _ -> true
| Oslh _ -> true
| Oasm asm -> is_ct_asm asm
let rec ty_expr ~(public:bool) env (e:expr) =
match e with
| Pconst _ | Pbool _ | Parr_init _ -> env, Public
| Pvar x -> Env.gget ~public env x
| Pget (_, _, _, x, i) | Psub (_, _, _, x, i) ->
let env, ty = Env.gget ~public env x in
let env, _ = ty_expr ~public:true env i in
env, ty
| Pload (_, _, i) ->
let env, _ = ty_expr ~public:true env i in
env, Secret
| Papp1(o, e) ->
let public = public || not (is_ct_op1 o) in
ty_expr ~public env e
| Papp2(o, e1, e2) ->
let public = public || not (is_ct_op2 o) in
ty_exprs_max ~public env [e1; e2]
| PappN(o, es) ->
let public = public || not (is_ct_opN o) in
ty_exprs_max ~public env es
| Pif(_, e1, e2, e3) -> ty_exprs_max ~public env [e1; e2; e3]
and ty_exprs ~public env es =
List.map_fold (ty_expr ~public) env es
and ty_exprs_max ~public env es =
let env, lvls = ty_exprs ~public env es in
env, Lvl.maxs lvls
let ty_lval env x lvl =
match x with
| Lnone _ -> env
| Lvar x -> Env.set env x lvl
| Lmem(_, _, _, i) ->
let env, _ = ty_expr ~public:true env i in
env
| Laset(_, _, _, x, i) | Lasub(_, _, _, x, i) ->
let env, xlvl = Env.get ~public:false env x in
let env, _ = ty_expr ~public:true env i in
Env.set env x (Lvl.max xlvl lvl)
let ty_lvals env xs lvls =
List.fold_left2 ty_lval env xs lvls
let ty_lvals1 env xs lvl =
List.fold_left (fun env x -> ty_lval env x lvl) env xs
let lvl_of_level =
function
| SecurityAnnotations.Public -> Public
| Secret -> Secret
| Named n -> Lvl.poly1 (Vl.mk_poly n)
let lvl_of_typ =
function
| SecurityAnnotations.Msf -> Public
| Direct t | Indirect { value = t ; ptr = _ } -> lvl_of_level t.normal
let get_annot ensure_annot f =
let sig_annot = SecurityAnnotations.get_sct_signature f.f_annot.f_user_annot in
let process_argument i x =
let lvl =
match Lvl.parse ~single:true x.v_annot, Option.bind sig_annot (SecurityAnnotations.get_nth_argument i) with
| lvl, None -> lvl
| Some _ as lvl, _ -> lvl
| _, Some t -> Some (lvl_of_typ t)
in
x.v_name, lvl
in
let process_result i a =
match Lvl.parse ~single:false a, Option.bind sig_annot (SecurityAnnotations.get_nth_result i) with
| lvl, None -> lvl
| Some _ as lvl, _ -> lvl
| _, Some t -> Some (lvl_of_typ t)
in
let ain = List.mapi process_argument f.f_args in
let ainlevels = List.map (fun (_, x) -> x) ain in
let aout = List.mapi process_result f.f_ret_info.ret_annot in
let check_defined msg l =
if List.exists (fun a -> a = None) l then
error ~loc:f.f_loc
"export functions should be fully annotated, missing some security annotations on %s.@ User option “--infer” to infer them."
msg in
if ensure_annot && FInfo.is_export f.f_cc then
(check_defined "result types" aout;
check_defined "function parameters" ainlevels);
let used_lvls =
let f acc lvl =
match lvl with
| Some (Poly s) -> Svl.union s acc
| _ -> acc
in
let lvls = List.fold_left f Svl.empty ainlevels in
List.fold_left f lvls aout
in
let used_lvls = ref used_lvls in
let counter = ref (-1) in
let rec fresh_lvl ?n () =
let vl =
let k =
match n with
| None -> incr counter; "l" ^ string_of_int !counter
| Some x -> x
in
Vl.mk_uni k in
if Svl.mem vl !used_lvls then fresh_lvl ()
else (used_lvls := Svl.add vl !used_lvls; vl)
in
let ain =
let doit (n, o) =
match o with
| None -> Lvl.poly1 (fresh_lvl ~n ())
| Some lvl -> lvl in
List.map doit ain
in
let do_local x decls =
let lvl = Lvl.parse ~single:true x.v_annot in
match lvl with
| Some lvl -> (x,lvl) :: decls
| None -> decls
in
let ldecls = Sv.fold do_local (Prog.locals f) [] in
let known =
List.fold_left
(fun s lvl -> match lvl with Poly s' -> Svl.union s s' | _ -> s) Svl.empty ain in
let check_lvl lvl =
match lvl with
| Poly s ->
let diff = Svl.diff s known in
if not (Svl.is_empty diff) then
error ~loc:f.f_loc
"variable(s) level %a should be used in the input security annotations"
(pp_list ", " Vl.pp) (Svl.elements diff)
| _ -> () in
List.iter (Option.may check_lvl) aout;
List.iter (fun (_, lvl) -> check_lvl lvl) ldecls;
ain, aout, ldecls
let sdeclassify = "declassify"
let is_declassify annot =
Annot.ensure_uniq1 sdeclassify Annot.none annot <> None
let declassify_lvl annot lvl =
if is_declassify annot then Public
else lvl
let declassify_lvls annot lvls =
if is_declassify annot then List.map (fun _ -> Public) lvls
else lvls
let rec ty_instr is_ct_asm fenv env i =
let env1 =
match i.i_desc with
| Cassgn(x, _, _, e) ->
let env, lvl = ty_expr ~public:false env e in
ty_lval env x (declassify_lvl i.i_annot lvl)
| Copn(xs, _, o, es) ->
let public = not (is_ct_sopn is_ct_asm o) in
let env, lvl = ty_exprs_max ~public env es in
ty_lvals1 env xs (declassify_lvl i.i_annot lvl)
| Csyscall(xs, RandomBytes _, es) ->
let env, _ = ty_exprs_max ~public:true env es in
ty_lvals1 env xs (declassify_lvl i.i_annot Secret)
| Cif(e, c1, c2) ->
let env, _ = ty_expr ~public:true env e in
let env1 = ty_cmd is_ct_asm fenv env c1 in
let env2 = ty_cmd is_ct_asm fenv env c2 in
Env.max env1 env2
| Cfor(x, (_, e1, e2), c) ->
let env, _ = ty_exprs ~public:true env [e1; e2] in
let rec loop env =
let env1 = Env.set env x Public in
let env1 = ty_cmd is_ct_asm fenv env1 c in
if Env.le env1 env then env
else loop (Env.max env1 env) in
loop env
| Cwhile(_, c1, e, _, c2) ->
let rec loop env =
let env1 = ty_cmd is_ct_asm fenv env c1 in
let env1,_ = ty_expr ~public:true env1 e in
let env2 = ty_cmd is_ct_asm fenv env1 c2 in
if Env.le env2 env then env1
else loop (Env.max env2 env) in
loop env
| Ccall (xs, f, es) ->
let fty = get_fun is_ct_asm fenv f in
let do_e env e lvl = ty_expr ~public:(lvl=Public) env e in
let env, elvls = List.map_fold2 do_e env es fty.tyin in
let olvls = instanciate_fty fty elvls in
ty_lvals env xs (declassify_lvls i.i_annot olvls)
in
if !Glob_options.debug then
Format.eprintf "%a: @[<v>before %a@ after %a@]@." L.pp_loc (i.i_loc.base_loc) Env.pp env Env.pp env1;
env1
and ty_cmd is_ct_asm fenv env c =
List.fold_left (fun env i -> ty_instr is_ct_asm fenv env i) env c
and get_fun is_ct_asm fenv f =
try Hf.find fenv.env_ty f
with Not_found ->
let fty = ty_fun is_ct_asm fenv f in
Hf.add fenv.env_ty f fty;
fty
and ty_fun is_ct_asm fenv fn =
let f = List.find (fun f -> F.equal f.f_name fn) fenv.env_def in
let tyin, aout, ldecls = get_annot fenv.ensure_annot f in
let env = List.fold_left2 Env.add Env.empty f.f_args tyin in
let env = List.fold_left (fun env (x,lvl) -> Env.add env x lvl) env ldecls in
let env = ty_cmd is_ct_asm fenv env f.f_body in
let set_pub env x aout =
if aout = Some Public then
let env, _ = Env.get ~public:true env x in
env
else env in
let env = List.fold_left2 set_pub env f.f_ret aout in
if !Glob_options.debug then Format.eprintf "env return %a@." Env.pp env;
let do_r env x aout =
let _, lvl = Env.get ~public:false env x in
let lvl =
match aout with
| None -> lvl
| Some alvl ->
if Lvl.le lvl alvl then alvl
else
error ~loc:(L.loc x)
"the variable %a has type %a instead of %a"
(Printer.pp_var ~debug:false) (L.unloc x)
Lvl.pp lvl Lvl.pp alvl in
lvl in
let tyout = List.map2 (do_r env) f.f_ret aout in
let tyin = List.map (fun lvl -> Env.norm_lvl env lvl) tyin in
{ tyin ; tyout }
let ty_prog (is_ct_asm: 'asm -> bool) ~infer (prog: ('info, 'asm) prog) fl =
let prog = snd prog in
let fenv =
{ ensure_annot = not infer
; env_ty = Hf.create 101
; env_def = prog } in
let fl =
if fl = [] then
List.rev_map (fun f -> f.f_name) prog
else
let get fn =
try (List.find (fun f -> f.f_name.fn_name = fn) prog).f_name
with Not_found -> hierror ~loc:Lnone ~kind:"constant type checker" "unknown function %s" fn in
List.map get fl in
let status =
match List.iter (fun fn -> ignore (get_fun is_ct_asm fenv fn : signature)) fl with
| () -> None
| exception Annot.AnnotationError (loc, msg)
| exception CtTypeError (loc, msg)
-> Some (loc, msg)
in
Hf.to_list fenv.env_ty, status