From 07ab4472d6285f887e6ccba82ec352519128074d Mon Sep 17 00:00:00 2001 From: J08nY Date: Wed, 8 May 2024 12:31:06 +0200 Subject: [PATCH] Add DOIT data to the architecture descriptions --- AUTHORS | 1 + CHANGELOG.md | 6 ++ compiler/src/arch_full.ml | 10 ++- compiler/src/arch_full.mli | 4 +- compiler/src/arm_arch_full.ml | 67 ++++++++++++++- compiler/src/x86_arch_full.ml | 153 +++++++++++++++++++++++++++++++++- 6 files changed, 232 insertions(+), 9 deletions(-) diff --git a/AUTHORS b/AUTHORS index 2c01e5312..489ed05f3 100644 --- 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 index 0b5d638b7..3790b6050 100644 --- 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 index 464643bde..3d8785aad 100644 --- 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 index 3b99dd576..d9ce086f8 100644 --- 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 index 9dcbce8a8..0747c48b1 100644 --- 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 index c32243e88..8ddb3d7cc 100644 --- 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