Add support for DOIT

AUTHORS

@@ -14,6 +14,7 @@ Clément Sartori
 François Dupressoir
 Gaëtan Cassiers
 Gilles Barthe
+Ján Jančár
 Jean-Christophe Léchenet
 José Bacelar Almeida
 Kai-Chun Ning

CHANGELOG.md

@@ -28,6 +28,12 @@
   returned first and in the same order in the list of results.
   ([PR #707](https://github.com/jasmin-lang/jasmin/pull/707)).
 
+- The (speculative) constant-time checker can optionally check that secrets are
+  only used with guaranteed constant time instructions (DOIT for Intel, DIT for
+  ARM)
+  ([PR #736](https://github.com/jasmin-lang/jasmin/pull/736),
+  [PR #811](https://github.com/jasmin-lang/jasmin/pull/811)).
+
 - Add spill/unspill primitives allowing to spill/unspill reg and reg ptr
   to/from the stack without need to declare the corresponding stack variable.
   If the annotation #spill_to_mmx is used at the variable declaration the variable

compiler/CCT/fail/doit/x86_64/rol.jazz

@@ -0,0 +1,6 @@
+// This is CT in the ordinary sense, but not DOIT as ROL is not DOIT.
+export fn rol(#secret reg u32 x) -> #secret reg u32 {
+  x <<r = 5;
+  x = x;
+  return x;
+}

compiler/CCT/fail/doit/x86_64/xchg.jazz

@@ -0,0 +1,7 @@
+// This is CT in the ordinary sense, but not DOIT as XCHG is not DOIT.
+export fn xchange(#secret reg u32 a, #secret reg u32 b) -> #secret reg u32, #secret reg u32 {
+    a = a;
+    b = b;
+    a, b = #swap(a, b);
+    return a, b;
+}

compiler/CCT/success/doit/by_stack.jazz

@@ -0,0 +1,6 @@
+export fn id(#secret reg u32 x) -> #secret reg u32 {
+  stack u32 s;
+  s = x;
+  x = s;
+  return x;
+}

compiler/Makefile

@@ -7,7 +7,7 @@ CHECK     := $(CHECKPY) scripts/runtest --jobs="$(JSJOBS)"
 CHECK     += config/tests.config
 CHECKCATS ?= \
 	safety \
-	CCT \
+	CCT CCT-DOIT \
 	x86-64-ATT \
 	x86-64-Intel \
 	x86-64-print \

compiler/config/tests.config

@@ -14,6 +14,13 @@ kodirs = safety/fail
 bin    = ./scripts/check-cct
 okdirs = CCT/success
 kodirs = CCT/fail
+exclude = CCT/success/doit CCT/fail/doit
+
+[test-CCT-DOIT]
+bin    = ./scripts/check-cct
+args = --doit
+okdirs = CCT/success/doit
+kodirs = CCT/fail/doit
 
 [test-SCT]
 bin    = ./scripts/check-cct

compiler/entry/jasmin_ct.ml

@@ -5,7 +5,7 @@ open Utils
 
 let parse_and_check arch call_conv =
   let module A = (val get_arch_module arch call_conv) in
-  let check infer ct_list speculative pass file =
+  let check ~doit infer ct_list speculative pass file =
     let _env, pprog, _ast =
       try Compile.parse_file A.arch_info file with
       | Annot.AnnotationError (loc, code) ->
@@ -44,7 +44,7 @@ let parse_and_check arch call_conv =
     in
 
     if speculative then
-      match Sct_checker_forward.ty_prog A.is_ct_sopn prog ct_list with
+      match Sct_checker_forward.ty_prog (A.is_ct_sopn ~doit) prog ct_list with
       | exception Annot.AnnotationError (loc, code) ->
           hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code
       | sigs ->
@@ -53,7 +53,7 @@ let parse_and_check arch call_conv =
             sigs
     else
       let sigs, errs =
-        Ct_checker_forward.ty_prog A.is_ct_sopn ~infer prog ct_list
+        Ct_checker_forward.ty_prog (A.is_ct_sopn ~doit) ~infer prog ct_list
       in
       Format.printf "/* Security types:\n@[<v>%a@]*/@."
         (pp_list "@ " (Ct_checker_forward.pp_signature prog))
@@ -63,8 +63,13 @@ let parse_and_check arch call_conv =
       in
       Stdlib.Option.iter on_err errs
   in
-  fun infer ct_list speculative compile file ->
-    match check infer ct_list speculative compile file with
+  fun infer ct_list speculative compile file doit ->
+    let compile =
+      if doit && compile < Compiler.PropagateInline then
+        Compiler.PropagateInline
+      else compile
+    in
+    match check ~doit infer ct_list speculative compile file with
     | () -> ()
     | exception HiError e ->
         Format.eprintf "%a@." pp_hierror e;
@@ -104,6 +109,10 @@ let file =
   let doc = "The Jasmin source file to verify" in
   Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"JAZZ" ~doc)
 
+let doit =
+  let doc = "Allow only DOIT instructions on secrets" in
+  Arg.(value & flag & info [ "doit" ] ~doc)
+
 let () =
   let doc = "Check Constant-Time security of Jasmin programs" in
   let man =
@@ -114,9 +123,11 @@ let () =
       `I ("JASMINPATH", "To resolve $(i,require) directives");
     ]
   in
-  let info = Cmd.info "jasmin-ct" ~version:Glob_options.version_string ~doc ~man in
+  let info =
+    Cmd.info "jasmin-ct" ~version:Glob_options.version_string ~doc ~man
+  in
   Cmd.v info
     Term.(
       const parse_and_check $ arch $ call_conv $ infer $ slice $ speculative
-      $ compile $ file)
+      $ compile $ file $ doit)
   |> Cmd.eval |> exit

compiler/src/arch_full.ml

@@ -35,7 +35,9 @@ module type Core_arch = sig
   val known_implicits : (Name.t * string) list
 
   val is_ct_asm_op : asm_op -> bool
+  val is_doit_asm_op : asm_op -> bool
   val is_ct_asm_extra : extra_op -> bool
+  val is_doit_asm_extra : extra_op -> bool
 
 end
 
@@ -71,7 +73,7 @@ module type Arch = sig
 
   val arch_info : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Pretyping.arch_info
 
-  val is_ct_sopn : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op -> bool
+  val is_ct_sopn : ?doit:bool -> (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op -> bool
 end
 
 module Arch_from_Core_arch (A : Core_arch) :
@@ -198,9 +200,9 @@ module Arch_from_Core_arch (A : Core_arch) :
       flagnames = List.map fst known_implicits;
     }
 
-  let is_ct_sopn (o : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) =
+  let is_ct_sopn ?(doit = false) (o : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op) =
    match o with
-   | BaseOp (_, o) -> is_ct_asm_op o
-   | ExtOp o -> is_ct_asm_extra o
+   | BaseOp (_, o) -> (if doit then is_doit_asm_op else is_ct_asm_op) o
+   | ExtOp o -> (if doit then is_doit_asm_extra else is_ct_asm_extra) o
 
 end

compiler/src/arch_full.mli

@@ -36,7 +36,9 @@ module type Core_arch = sig
   val known_implicits : (Name.t * string) list
 
   val is_ct_asm_op : asm_op -> bool
+  val is_doit_asm_op : asm_op -> bool
   val is_ct_asm_extra : extra_op -> bool
+  val is_doit_asm_extra : extra_op -> bool
 
 end
 
@@ -72,7 +74,7 @@ module type Arch = sig
 
   val arch_info : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Pretyping.arch_info
 
-  val is_ct_sopn : (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op -> bool
+  val is_ct_sopn : ?doit:bool -> (reg, regx, xreg, rflag, cond, asm_op, extra_op) Arch_extra.extended_op -> bool
 end
 
 module Arch_from_Core_arch (A : Core_arch) : Arch

compiler/src/arm_arch_full.ml

@@ -33,8 +33,71 @@ module Arm_core = struct
     | ARM_op( (SDIV  | UDIV), _) -> false
     | _ -> true
 
-
-  let is_ct_asm_extra (_ : extra_op) = true
+  let is_doit_asm_op (o : asm_op) =
+    match o with
+    | ARM_op(ADC, _) -> true
+    | ARM_op(ADD, _) -> true
+    | ARM_op(ADR, _) -> false (* Not DIT *)
+    | ARM_op(AND, _) -> true
+    | ARM_op(ASR, _) -> true
+    | ARM_op(BFC, _) -> true
+    | ARM_op(BFI, _) -> true
+    | ARM_op(BIC, _) -> true
+    | ARM_op(CLZ, _) -> true
+    | ARM_op(CMN, _) -> true
+    | ARM_op(CMP, _) -> true
+    | ARM_op(EOR, _) -> true
+    | ARM_op(LDR, _) -> true
+    | ARM_op(LDRB, _) -> true
+    | ARM_op(LDRH, _) -> true
+    | ARM_op(LDRSB, _) -> true
+    | ARM_op(LDRSH, _) -> true
+    | ARM_op(LSL, _) -> true
+    | ARM_op(LSR, _) -> true
+    | ARM_op(MLA, _) -> true
+    | ARM_op(MLS, _) -> true
+    | ARM_op(MOV, _) -> true
+    | ARM_op(MOVT, _) -> true
+    | ARM_op(MUL, _) -> true
+    | ARM_op(MVN, _) -> true
+    | ARM_op(ORR, _) -> true
+    | ARM_op(REV, _) -> true
+    | ARM_op(REV16, _) -> true
+    | ARM_op(REVSH, _) -> false (* Not DIT *)
+    | ARM_op(ROR, _) -> true
+    | ARM_op(RSB, _) -> false (* Not DIT *)
+    | ARM_op(SBFX, _) -> true
+    | ARM_op(SDIV, _) -> false (* Not DIT *)
+    | ARM_op(SMLA_hw _, _) -> false (* Not DIT *)
+    | ARM_op(SMLAL, _) -> true
+    | ARM_op(SMMUL, _) -> false (* Not DIT *)
+    | ARM_op(SMMULR, _) -> false (* Not DIT *)
+    | ARM_op(SMUL_hw _, _) -> false (* Not DIT *)
+    | ARM_op(SMULL, _) -> true
+    | ARM_op(SMULW_hw _, _) -> false (* Not DIT *)
+    | ARM_op(STR, _) -> true
+    | ARM_op(STRB, _) -> true
+    | ARM_op(STRH, _) -> true
+    | ARM_op(SUB, _) -> true
+    | ARM_op(TST, _) -> true
+    | ARM_op(UBFX, _) -> true
+    | ARM_op(UDIV, _) -> false (* Not DIT *)
+    | ARM_op(UMAAL, _) -> false (* Not DIT *)
+    | ARM_op(UMLAL, _) -> true
+    | ARM_op(UMULL, _) -> true
+    | ARM_op(UXTB, _) -> true
+    | ARM_op(UXTH, _) -> true
+
+
+  (* All of the extra ops compile into CT instructions (no DIV). *)
+  let is_ct_asm_extra (o : extra_op) = true
+
+  (* All of the extra ops compile into DIT instructions only, but this needs to be checked manually. *)
+  let is_doit_asm_extra (o : extra_op) =
+    match o with
+    | Oarm_swap _ -> true
+    | Oarm_add_large_imm -> true
+    | (Osmart_li _ | Osmart_li_cc _) -> true (* emit MOVT *)
 
 end