Add DOIT data to the architecture descriptions

jasmin-lang · May 28, 2024 · 07ab447 · 07ab447
1 parent d6e672c
commit 07ab447
Show file tree

Hide file tree

Showing 6 changed files with 232 additions and 9 deletions.
diff --git a/AUTHORS b/AUTHORS
@@ -13,6 +13,7 @@ Benoît Viguier
 Clément Sartori
 François Dupressoir
 Gilles Barthe
+Ján Jančár
 Jean-Christophe Léchenet
 José Bacelar Almeida
 Kai-Chun Ning

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -15,6 +15,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

diff --git a/compiler/src/arch_full.ml b/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
diff --git a/compiler/src/arch_full.mli b/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

diff --git a/compiler/src/arm_arch_full.ml b/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, _) -> false (* Not DIT *)
+    | ARM_op(LDRB, _) -> false (* Not DIT *)
+    | ARM_op(LDRH, _) -> false (* Not DIT *)
+    | ARM_op(LDRSB, _) -> false (* Not DIT *)
+    | ARM_op(LDRSH, _) -> false (* Not DIT *)
+    | ARM_op(LSL, _) -> true
+    | ARM_op(LSR, _) -> true
+    | ARM_op(MLA, _) -> true
+    | ARM_op(MLS, _) -> true
+    | ARM_op(MOV, _) -> true
+    | ARM_op(MOVT, _) -> false (* Not DIT *)
+    | 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, _) -> false (* Not DIT *)
+    | ARM_op(STRB, _) -> false (* Not DIT *)
+    | ARM_op(STRH, _) -> false (* Not DIT *)
+    | 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 _) -> false (* emit MOVT *)
 
 end
 

diff --git a/compiler/src/x86_arch_full.ml b/compiler/src/x86_arch_full.ml
@@ -1,5 +1,6 @@
 open Arch_decl
 open X86_decl
+open Wsize
 
 module type X86_input = sig
 
@@ -47,8 +48,156 @@ module X86_core = struct
     | DIV _ | IDIV _ -> false
     | _ -> true
 
-  let is_ct_asm_extra (_ : extra_op) = true
-
+  let is_doit_asm_op (o : asm_op) =
+    match o with
+    | ADC _ -> true
+    | ADCX _ -> true
+    | ADD _ -> true
+    | ADOX _ -> true
+    | AESDEC -> true
+    | AESDECLAST -> true
+    | AESENC -> true
+    | AESENCLAST -> true
+    | AESIMC -> true
+    | AESKEYGENASSIST -> true
+    | AND _ -> true
+    | ANDN _ -> true
+    | BSWAP _ -> false (* Not DOIT *)
+    | BT _ -> true
+    | CLC -> false (* Not DOIT *)
+    | CLFLUSH -> false (* Not DOIT *)
+    | CMOVcc _ -> true
+    | CMP _ -> true
+    | CQO _ -> false (* Not DOIT *)
+    | DEC _ -> true
+    | DIV _ -> false (* Not DOIT *)
+    | IDIV _ -> false (* Not DOIT *)
+    | IMUL _ -> true
+    | IMULr _ -> false (* Not DOIT *)
+    | IMULri _ -> false (* Not DOIT *)
+    | INC _ -> true
+    | LEA _ -> true
+    | LFENCE -> false (* Not DOIT *)
+    | LZCNT _ -> false (* Not DOIT *)
+    | MFENCE -> false (* Not DOIT *)
+    | MOV _ -> true
+    | MOVD _ -> true
+    | MOVSX _ -> true
+    | MOVV _ -> true
+    | MOVX _ -> true
+    | MOVZX _ -> true
+    | MUL _ -> true
+    | MULX_lo_hi _ -> true
+    | NEG _ -> true
+    | NOT _ -> true
+    | OR _ -> true
+    | PCLMULQDQ -> true
+    | PDEP _ -> false (* Not DOIT *)
+    | PEXT _ -> false (* Not DOIT *)
+    | POPCNT _ -> false (* Not DOIT *)
+    | RCL _ -> false (* Not DOIT *)
+    | RCR _ -> false (* Not DOIT *)
+    | RDTSC _ -> false (* Not DOIT *)
+    | RDTSCP _ -> false (* Not DOIT *)
+    | ROL _ -> false (* Not DOIT *)
+    | ROR _ -> false (* Not DOIT *)
+    | SAL _ -> false (* Not DOIT *)
+    | SAR _ -> true
+    | SBB _ -> true
+    | SETcc -> true
+    | SFENCE -> false (* Not DOIT *)
+    | SHL _ -> true
+    | SHLD _ -> false (* Not DOIT *)
+    | SHR _ -> true
+    | SHRD _ -> false (* Not DOIT *)
+    | STC -> false (* Not DOIT *)
+    | SUB _ -> true
+    | TEST _ -> true
+    | VAESDEC -> true
+    | VAESDECLAST -> true
+    | VAESENC -> true
+    | VAESENCLAST -> true
+    | VAESIMC -> true
+    | VAESKEYGENASSIST -> true
+    | VBROADCASTI128 -> true
+    | VEXTRACTI128 -> true
+    | VINSERTI128 -> true
+    | VMOV _ -> true
+    | VMOVDQA _ -> true
+    | VMOVDQU _ -> true
+    | VMOVHPD -> false (* Not DOIT *)
+    | VMOVLPD -> false (* Not DOIT *)
+    | VMOVSHDUP _ -> true
+    | VMOVSLDUP _ -> true
+    | VPACKSS _ -> true
+    | VPACKUS _ -> true
+    | VPADD _ -> true
+    | VPALIGNR _ -> true
+    | VPAND _ -> true
+    | VPANDN _ -> true
+    | VPAVG _ -> true
+    | VPBLEND _ -> true
+    | VPBLENDVB _ -> true
+    | VPBROADCAST _ -> true
+    | VPCLMULQDQ _ -> true
+    | VPCMPEQ _ -> true
+    | VPCMPGT _ -> true
+    | VPERM2I128 -> true
+    | VPERMD -> true
+    | VPERMQ -> true
+    | VPEXTR _ -> true
+    | VPINSR _ -> true
+    | VPMADDUBSW _ -> true
+    | VPMADDWD _ -> true
+    | VPMAXS (ve, _) -> ve = VE8 || ve = VE16
+    | VPMAXU _ -> true
+    | VPMINS (ve, _) -> ve = VE8 || ve = VE16
+    | VPMINU _ -> true
+    | VPMOVMSKB _ -> true
+    | VPMOVSX _ -> true
+    | VPMOVZX _ -> true
+    | VPMUL _ -> true
+    | VPMULH _ -> true
+    | VPMULHRS _ -> true
+    | VPMULHU _ -> true
+    | VPMULL _ -> true
+    | VPMULU _ -> true
+    | VPOR _ -> true
+    | VPSHUFB _ -> true
+    | VPSHUFD _ -> true
+    | VPSHUFHW _ -> true
+    | VPSHUFLW _ -> true
+    | VPSLL _ -> true
+    | VPSLLDQ _ -> true
+    | VPSLLV _ -> true
+    | VPSRA _ -> true
+    | VPSRL _ -> true
+    | VPSRLDQ _ -> true
+    | VPSRLV _ -> true
+    | VPSUB _ -> true
+    | VPTEST _ -> true
+    | VPUNPCKH _ -> true
+    | VPUNPCKL _ -> true
+    | VPXOR _ -> true
+    | VSHUFPS _ -> false (* Not DOIT *)
+    | XCHG _ -> false (* Not DOIT *)
+    | XOR _ -> 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 DOIT instructions only, but this needs to be checked manually. *)
+  let is_doit_asm_extra (o : extra_op) =
+    match o with
+    | Oset0 _           -> true
+    | Oconcat128        -> true
+    | Ox86MOVZX32       -> true
+    | Ox86MULX ws       -> true
+    | Ox86MULX_hi _     -> true
+    | Ox86SLHinit       -> true
+    | Ox86SLHupdate     -> true
+    | Ox86SLHmove       -> true
+    | Ox86SLHprotect _  -> true
 
 end