riscv: DIV, DIVU, REM and REMU are neither constant-time nor DOIT

changes/02-bugfix/1544-riscv-ct-doit.md

@@ -0,0 +1,7 @@
+- On RISC-V, the `DIV`, `DIVU`, `REM` and `REMU` instructions are no longer
+  considered constant-time nor DOIT: they have data-dependent latency on
+  typical implementations and are excluded from the Zkt ("Data-Independent
+  Execution Latency") safe list of the RISC-V specification; every other
+  instruction keeps its classification, now documented against the Zkt list
+  ([PR 1544](https://github.com/jasmin-lang/jasmin/pull/1544);
+  fixes [#1013](https://github.com/jasmin-lang/jasmin/issues/1013)).

compiler/CCT/fail/doit/riscv/div.jazz

@@ -0,0 +1,11 @@
+/* Unsigned division lowers to DIVU, which is not in the Zkt safe list,
+   hence not DOIT. */
+#[ct="secret -> secret"]
+export fn div(reg u32 x) -> reg u32 {
+  reg u32 d q;
+  x = x;
+  d = 3;
+  q = x / d;
+  q = q;
+  return q;
+}

compiler/CCT/fail/doit/riscv/mod.jazz

@@ -0,0 +1,11 @@
+/* Unsigned remainder lowers to REMU, which is not in the Zkt safe list,
+   hence not DOIT. */
+#[ct="secret -> secret"]
+export fn mod(reg u32 x) -> reg u32 {
+  reg u32 d q;
+  x = x;
+  d = 3;
+  q = x % d;
+  q = q;
+  return q;
+}

compiler/CCT/fail/riscv/div_secret.jazz

@@ -0,0 +1,10 @@
+/* DIV has data-dependent latency, it is not constant-time. */
+#[ct="secret -> secret"]
+export fn div_secret(reg u32 x) -> reg u32 {
+  reg u32 d q;
+  x = x;
+  d = 3;
+  q = #DIV(x, d);
+  q = q;
+  return q;
+}

compiler/CCT/fail/riscv/rem_secret.jazz

@@ -0,0 +1,10 @@
+/* REM has data-dependent latency, it is not constant-time. */
+#[ct="secret -> secret"]
+export fn rem_secret(reg u32 x) -> reg u32 {
+  reg u32 d q;
+  x = x;
+  d = 3;
+  q = #REM(x, d);
+  q = q;
+  return q;
+}

compiler/CCT/success/doit/riscv/arith.jazz

@@ -0,0 +1,15 @@
+/* MUL, ADD, XOR and SLLI are in the Zkt safe list; loads and stores of
+   secret data are also accepted (see the documentation of [id_doit] in
+   proofs/compiler/riscv_instr_decl.v). */
+#[ct="secret * secret -> secret"]
+export fn arith(reg u32 a, reg u32 b) -> reg u32 {
+  stack u32 s;
+  reg u32 t;
+  t = a * b;
+  t += b;
+  t ^= a;
+  t <<= 2;
+  s = t;
+  t = s;
+  return t;
+}

compiler/CCT/success/riscv/div_public.jazz

@@ -0,0 +1,14 @@
+/* Division and remainder are allowed on public data. */
+#[ct="public -> public"]
+export fn add_div_mod(reg u32 x) -> reg u32 {
+  reg u32 x1 x2 d q q1 r r1;
+  x1 = x; x2 = x;
+  d = 3;
+  q = x1 / d;
+  q1 = q;
+  r = x2 % d;
+  r = r1;
+  r = r + q1;
+  r = r;
+  return r;
+}

compiler/Makefile

@@ -17,7 +17,7 @@ CHECKCATS ?= \
 	arm-m4-stack-zero-unrolled \
 	risc-v-stack-zero-loop \
 	risc-v-stack-zero-unrolled \
-	CCT CCT-DOIT SCT
+	CCT CCT-riscv CCT-DOIT CCT-DOIT-riscv SCT
 
 # --------------------------------------------------------------------
 DESTDIR  ?=

compiler/config/tests.config

@@ -9,13 +9,26 @@ kodirs = tests/fail/nolea/x86-64
 bin    = ./jasmin-ct
 okdirs = CCT/success
 kodirs = CCT/fail
-exclude = CCT/success/doit CCT/fail/doit
+exclude = CCT/success/doit CCT/fail/doit CCT/success/riscv CCT/fail/riscv
+
+[test-CCT-riscv]
+bin    = ./jasmin-ct
+args = --arch riscv
+okdirs = CCT/success/riscv
+kodirs = CCT/fail/riscv
 
 [test-CCT-DOIT]
 bin    = ./jasmin-ct
 args = --doit
 okdirs = CCT/success/doit
 kodirs = CCT/fail/doit
+exclude = CCT/success/doit/riscv CCT/fail/doit/riscv
+
+[test-CCT-DOIT-riscv]
+bin    = ./jasmin-ct
+args = --doit --arch riscv
+okdirs = CCT/success/doit/riscv
+kodirs = CCT/fail/doit/riscv
 
 [test-SCT]
 bin    = ./jasmin-ct

compiler/src/riscv_arch_full.ml

@@ -24,11 +24,19 @@ module Riscv_core = struct
   let alloc_stack_need_extra sz =
     not (Riscv_params_core.is_arith_small (Conv.cz_of_z sz))
 
-  (* FIXME RISCV: check if everything is ct *)
+  (* Division and remainder have data-dependent latency on typical
+     implementations, and are explicitly excluded from the Zkt safe list of
+     the RISC-V specification ("Data-Independent Execution Latency Subset");
+     see the documentation in proofs/compiler/riscv_instr_decl.v.
+     Every other instruction is assumed to be constant-time, as on the other
+     architectures. *)
   let is_ct_asm_op (o : asm_op) =
     match o with
+    | Riscv_instr_decl.DIV | DIVU | REM | REMU -> false
     | _ -> true
 
+  (* All of the extra ops compile into CT instructions (no DIV/REM):
+     SWAP into xor, add_large_imm into lui/addi/add. *)
   let is_ct_asm_extra (_o : extra_op) = true
 
 end

docs/source/tools/ct.md

@@ -41,7 +41,7 @@ any pass, but the type system can be more precise after some step of compilation
   - `--doit`
 The usual leakage model for constant-time considers that only conditional instructions and load/store
 instructions leak. This option allows to consider a stronger model where non Data Independent Timing instructions
-leak. In this model, secret data can only be applied to Data Independent Timing instructions ([DOIT](https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/best-practices/data-operand-independent-timing-isa-guidance.html) for Intel and [DIT](https://developer.arm.com/documentation/ddi0595/2020-12/AArch64-Registers/DIT--Data-Independent-Timing) for Arm).
+leak. In this model, secret data can only be applied to Data Independent Timing instructions ([DOIT](https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/best-practices/data-operand-independent-timing-isa-guidance.html) for Intel, [DIT](https://developer.arm.com/documentation/ddi0595/2020-12/AArch64-Registers/DIT--Data-Independent-Timing) for Arm and [Zkt](https://github.com/riscv/riscv-crypto/blob/main/doc/scalar/riscv-crypto-scalar-zkt.adoc) for RISC-V).
   - `--infer`
 Infer security contracts. This can be used for development purpose but should not be used for production.
   - `--print`
@@ -287,6 +287,10 @@ Third-party references:
 
 - [List of DOIT instructions on Intel platforms](https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/resources/data-operand-independent-timing-instructions.html)
 - [ARM documentation for DIT](https://developer.arm.com/documentation/ddi0601/2025-06/AArch64-Registers/DIT--Data-Independent-Timing)
+- [RISC-V Zkt extension, “Data-Independent Execution Latency Subset”](https://github.com/riscv/riscv-crypto/blob/main/doc/scalar/riscv-crypto-scalar-zkt.adoc)
+  (RISC-V has no run-time flag akin to Intel DOIT or ARM DIT: Zkt is an
+  attestation, by the hardware vendor, that the listed instructions have
+  data-independent latency)
 
 More details can be found in the following paper: