Safety assert2

compiler/Makefile

@@ -54,6 +54,7 @@ check-ci:
 check-ec:
 	$(MAKE) -C examples/gimli/proofs
 	$(MAKE) -C examples/extraction-unit-tests
+	$(MAKE) -C examples/extraction-safety-unit-tests
 
 check-all: check
 	dune runtest -f

compiler/entry/commonCLI.ml

@@ -57,7 +57,7 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
        and type rflag = rflag
        and type cond = cond
        and type asm_op = asm_op
-       and type extra_op = extra_op) ~wi2i pass file idirs =
+       and type extra_op = extra_op) ~wi2i ~safety pass file idirs =
   let _env, pprog, _ast =
     try Compile.parse_file Arch.arch_info ~idirs file with
     | Annot.AnnotationError (loc, code) ->
@@ -76,6 +76,10 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
 
   let prog =
     if not wi2i then prog else Compile.do_wint_int (module Arch) prog
+  in 
+
+  let prog =
+    if not safety then prog else Compile.create_safety_asserts (module Arch) prog
   in
 
   let prog =

compiler/entry/commonCLI.mli

@@ -18,6 +18,7 @@ val parse_and_compile :
       and type xreg = 'xreg) ->
   wi2i:bool ->
   (* true => start by replacing wint operation by int operation *)
+  safety:bool ->
   Compiler.compiler_step ->
   string ->
   (string * string) list ->

compiler/entry/jasmin2ec.ml

@@ -3,56 +3,84 @@ open Cmdliner
 open CommonCLI
 open Utils
 
-let extract_to_file prog arch pd msfsz asmOp model amodel fnames array_dir
-    outfile =
-  let array_dir =
-    if array_dir = None then Option.map Filename.dirname outfile else array_dir
-  in
+let get_outfile_name outfile =
+  match outfile with
+  | None -> ""
+  | Some f -> 
+        let basename = Filename.basename f in
+        let basename' =
+          try Filename.chop_extension basename with Invalid_argument _ -> basename in
+        String.capitalize_ascii basename'
+
+let format_to_file outfile action =
   let fmt, close =
     match outfile with
-    | None -> (Format.std_formatter, fun () -> ())
+    | None ->
+        Format.std_formatter, (fun () -> ())
     | Some f ->
         let out = open_out f in
         let fmt = Format.formatter_of_out_channel out in
-        (fmt, fun () -> close_out out)
+        fmt, (fun () -> close_out out)
   in
   try
     BatPervasives.finally
       (fun () -> close ())
-      (fun () ->
-        ToEC.extract prog arch pd msfsz asmOp model amodel fnames array_dir fmt)
+      (fun () -> action fmt)
       ()
   with e ->
     BatPervasives.ignore_exceptions
       (fun () -> Option.map Unix.unlink outfile)
       ();
     raise e
 
+let extract_to_file prog arch pd msfsz asmOp model amodel fnames array_dir outfile prooffile =
+  let array_dir =
+    if array_dir = None then Option.map Filename.dirname outfile else array_dir
+  in
+  let extract () =
+    format_to_file outfile (fun fmt ->
+      ToEC.extract prog arch pd msfsz asmOp model amodel fnames array_dir fmt) in
+  let extract_proof () =
+    format_to_file prooffile (fun fmt ->
+      ToEC.generate_safety_lemmas (get_outfile_name outfile) prog arch pd msfsz asmOp model amodel fnames array_dir fmt) in
+  match model, outfile, prooffile with
+  | SafetyAnnotations, None, Some _ -> extract_proof ()
+  | SafetyAnnotations, Some _, None -> extract ()
+  | SafetyAnnotations, _, _         -> extract (); extract_proof ()
+  | _ -> extract ()
+
 let parse_and_extract arch call_conv idirs =
   let module A = (val CoreArchFactory.get_arch_module arch call_conv) in
-  let extract model amodel functions array_dir output pass file =
-    let prog = parse_and_compile (module A) ~wi2i:true pass file idirs in
-    extract_to_file prog arch A.reg_size A.msf_size A.asmOp model amodel
-      functions array_dir output
+  let extract model amodel functions array_dir output output_proof pass file =
+    let safety =
+      match model with
+       | SafetyAnnotations -> true
+       | _ -> false
+    in
+    let prog = parse_and_compile (module A) ~wi2i:true ~safety:safety pass file idirs in
+    extract_to_file prog arch A.reg_size  A.msf_size A.asmOp model amodel functions
+      array_dir output output_proof
   in
-  fun model amodel functions array_dir output pass file warn ->
+  fun model amodel functions array_dir output output_proof pass file warn ->
     if not warn then nowarning ();
-    match extract model amodel functions array_dir output pass file with
+    match extract model amodel functions array_dir output output_proof pass file with
     | () -> ()
     | exception HiError e ->
         Format.eprintf "%a@." pp_hierror e;
         exit 1
 
 let model =
   let alts =
-    [ ("normal", Normal); ("CT", ConstantTime); ("CTG", ConstantTimeGlobal) ]
+    [ ("normal", Normal); ("CT", ConstantTime); ("CTG", ConstantTimeGlobal); ("safety", SafetyAnnotations)]
   in
+  (* TODO : fix the documentation *)
   let doc =
     "Extraction model.
     $(b,normal): plain extraction.
     $(b,CT): Functions additionally return timing-observable leakage for
     'cryptographic constant time' (if/while conditions, memory access
     addresses, array indices, for loop bounds).
+    $(b,safety): extract for safety verification.
     (Deprecated) $(b,CTG): Cryptographic constant time leakage is added to a
     global variable."
   in
@@ -86,6 +114,13 @@ let output =
     & opt (some string) None
     & info [ "o"; "output" ] ~docv:"OUTPUT FILE" ~doc)
 
+let output_proof =
+ let doc = "Output proof file. If not given, output will be printed on stdout." in
+  Arg.(
+    value
+    & opt (some string) None
+    & info [ "output-proof" ] ~docv:"OUTPUT PROOF FILE" ~doc)
+
 let array_dir =
   let doc =
     "Directory for generation of easycrypt array theories. \
@@ -117,5 +152,5 @@ let () =
   Cmd.v info
     Term.(
       const parse_and_extract $ arch $ call_conv $ idirs $ model $ array_model
-      $ functions $ array_dir $ output $ after_pass $ file $ warn)
+      $ functions $ array_dir $ output $ output_proof $ after_pass $ file $ warn)
   |> Cmd.eval |> exit

compiler/entry/jasmin_ct.ml

@@ -11,8 +11,7 @@ type printer =
 let parse_and_check arch call_conv idirs =
   let module A = (val CoreArchFactory.get_arch_module arch call_conv) in
   let check ~doit infer ct_list speculative pass file print =
-    let prog = parse_and_compile (module A) ~wi2i:false pass file idirs in
-
+    let prog = parse_and_compile (module A) ~wi2i:false ~safety:false pass file idirs in
     if speculative then
       let prog =
         (* Ensure there are no spill/unspill operations left *)

compiler/examples/extraction-safety-unit-tests/Makefile

@@ -0,0 +1,19 @@
+ECARGS ?= -I Jasmin:../../../eclib
+
+JASMIN2EC := ../../jasmin2ec
+
+.SUFFIXES: .jazz .ec
+
+SOURCES := $(wildcard *.jazz)
+EXTRACTED := $(SOURCES:.jazz=.ec)
+
+all: proofs.ec $(EXTRACTED)
+	easycrypt runtest $(ECARGS) ec.config $@
+
+clean:
+	$(RM) $(EXTRACTED)
+
+%.ec: %.jazz $(JASMIN2EC)
+	$(JASMIN2EC) --model safety -o $@ $<
+
+.PHONY: all

compiler/examples/extraction-safety-unit-tests/ec.config

@@ -0,0 +1,6 @@
+[default]
+bin = easycrypt
+
+[test-all]
+okdirs = .
+

compiler/examples/extraction-safety-unit-tests/proofs.ec

@@ -0,0 +1,109 @@
+
+require import AllCore IntDiv CoreMap List Distr.
+from Jasmin require import JWord Jcheck JSafety.
+
+(* ----------------------------------------------------------------------------*)
+require Test_arr_sum.
+
+lemma Test_arr_sum_ok _x _b_x : Test_arr_sum.test_spec _x _b_x.
+proof.
+  rewrite /Test_arr_sum.test_spec .
+  proc; auto .
+  while ((valid trace_test) /\ (0 <= i)).
+  + auto => &m.
+    rewrite /valid all_cat => /> _ /#.
+  auto.
+qed.
+
+(* ----------------------------------------------------------------------------*)
+require Test_array.
+
+lemma Test_array_ok : Test_array.test_spec.
+proof.
+  rewrite /Test_array.test_spec.
+  proc; auto.
+qed.
+
+(* ----------------------------------------------------------------------------*)
+require Test_glob_array.
+
+lemma Test_glob_array_ok : Test_glob_array.get_global_spec.
+proof.
+  rewrite /get_global_spec.
+  proc; auto.
+qed.
+
+(* ----------------------------------------------------------------------------*)
+require Test_glob_var.
+
+lemma Test_glob_var_ok : Test_glob_var.zero_spec.
+proof.
+  rewrite /Test_glob_var.zero_spec .
+  proc; auto.
+qed.
+
+(* ----------------------------------------------------------------------------*)
+require Test_init_arr_sum.
+
+lemma Test_init_arr_sum_ok _x _b_x _y _b_y _z _b_z :
+       Test_init_arr_sum.test_spec _x _b_x _y _b_y _z _b_z.
+proof.
+  rewrite /test_spec.
+  proc; auto.
+  while ((valid trace_test) /\ 0 <= i /\ BArray10.is_init b_z 0 (2 * i)).
+  + auto => &m.
+    rewrite /is_init /valid !all_cat => /> /#.
+  auto => &m.
+  rewrite /is_init /valid !all_cat => /> /#.
+qed.
+
+(* ----------------------------------------------------------------------------*)
+require Test_init_pos_func.
+
+lemma init_pos_proof _x _b_x _i : Test_init_pos_func.init_pos_spec _x _b_x _i.
+proof.
+  rewrite /Test_init_pos_func.init_pos_spec.
+  proc; auto.
+  move=> &hr.
+  rewrite !and_iota /= /is_init /valid /= /#.
+qed .
+
+lemma test2_proof _x _b_x : Test_init_pos_func.test2_spec _x _b_x.
+proof.
+  rewrite /Test_init_pos_func.test2_spec.
+  proc; auto.
+  have init_pos_proof_aux := init_pos_proof; rewrite /Test_init_pos_func.init_pos_spec in init_pos_proof_aux;
+  ecall (init_pos_proof_aux param_0 (BArray5.init_arr (W8.of_int 255)) param).
+  auto => &hr.
+  rewrite and_iota /is_init /valid /= => /> ? result.
+  rewrite and_iota /= all_cat /= => />.
+  by move => ->.
+qed .
+
+lemma test_proof _x _b_x : Test_init_pos_func.test_spec _x _b_x.
+proof.
+  rewrite /test_spec.
+  proc; auto.
+  while ((valid trace_test) /\  (((0 <= i) /\ (i <= 5)) /\
+                                (BArray5.is_init b_x 0 i))).
+  + auto.
+    have init_pos_proof_aux := init_pos_proof; rewrite /init_pos_spec in init_pos_proof_aux;
+     ecall (init_pos_proof_aux param_0 b_param param).
+    auto.
+    rewrite /is_init /valid /= => /> &hr 5? result.
+    rewrite !and_iota /= !all_cat /= => 2?.
+    smt().
+  auto => &m.
+  rewrite /is_init /valid => />; split; first smt().
+  move => *; rewrite all_cat /= /#.
+qed .
+
+(* ----------------------------------------------------------------------------*)
+require Test_mem.
+
+lemma Test_mem_ok _str : Test_mem.test_spec _str.
+proof.
+rewrite /test_spec.
+proc; auto => &m /> *.
+smt (all_cat).
+qed.

compiler/examples/extraction-safety-unit-tests/test_arr_sum.jazz

@@ -0,0 +1,15 @@
+#[safety =
+   { requires = is_arr_init(x,0,5) }
+ ]
+fn test(reg ptr u8[5] x) -> reg u8
+{
+    reg u8 sum;
+    inline int i;
+    sum = 0;
+    for i = 0 to 5 {
+      sum += x[i];
+    }
+    return sum;
+}
+
+

compiler/examples/extraction-safety-unit-tests/test_array.jazz

@@ -0,0 +1,11 @@
+u8[8] a =
+{0X0, 0X4, 0X1, 0X5, 0X2, 0X6, 0X3, 0X7};
+
+fn test() -> reg u8 {
+  reg ptr u8[8] b;
+  reg u8 c;
+  c = a[3];
+  b = a;
+  c = b[2];
+  return c;
+}

compiler/examples/extraction-safety-unit-tests/test_cast.jazz

@@ -0,0 +1,13 @@
+fn test(reg u64 x, reg u64 y) -> reg u32
+{
+    reg u32 sum;
+    sum = x +32u y;
+    return sum;
+}
+
+fn test1(reg u64 x, reg u64 y) -> reg u32
+{
+    reg u32 sum;
+    _,_,_,_,_,sum = #ADD_32(x, y);
+    return sum;
+}

compiler/examples/extraction-safety-unit-tests/test_glob_array.jazz

@@ -0,0 +1,7 @@
+u32[2] t = {0, 1};
+
+export fn get_global() -> reg u32 {
+  reg u32 r;
+  r = t[0];
+  return r;
+}

compiler/examples/extraction-safety-unit-tests/test_glob_var.jazz

@@ -0,0 +1,7 @@
+u32 x = 0;
+
+export fn zero() -> reg u32 {
+  reg u32 r;
+  r = x;
+  return r;
+}

compiler/examples/extraction-safety-unit-tests/test_init_arr_sum.jazz

@@ -0,0 +1,12 @@
+#[safety =
+   { requires = is_arr_init(x,0,10) && is_arr_init(y,0,10)
+   , ensures = is_arr_init(z,0,10) }
+ ]
+fn test(reg ptr u16[5] x,reg ptr u16[5] y,reg ptr u16[5] z) -> reg ptr u16[5]
+{
+    inline int i;
+    for i = 0 to 5 {
+      z[i] = x[i] + y[i];
+    }
+    return z;
+}