Skip to content

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

Draft
clebreto wants to merge 1 commit into
jasmin-lang:mainfrom
clebreto:fix/riscv-ct-doit
Draft

riscv: DIV, DIVU, REM and REMU are neither constant-time nor DOIT#1544
clebreto wants to merge 1 commit into
jasmin-lang:mainfrom
clebreto:fix/riscv-ct-doit

Conversation

@clebreto

Copy link
Copy Markdown
Contributor

Fixes #1013.

RISC-V has no run-time flag akin to Intel DOIT or ARM DIT; the reference for data operand independent timing is the ratified Zkt extension ("Data-Independent Execution Latency Subset", chapter Zkt of the Scalar Cryptography spec). Its safe list covers, for the RV32IM subset modelled by Jasmin, all the base ALU instructions and mul/mulh/mulhu/mulhsu, and deliberately excludes division and remainder.

Changes:

  • riscv_instr_decl.v: the DOIT/NOT_DOIT constructors are now passed explicitly to the descriptor helpers at every call site (as done for the other architectures in arch: carry the DOIT classification in the instruction descriptors #1520); DIV, DIVU, REM and REMU become NOT_DOIT. A documentation block records the classification rationale against the Zkt list, including:
    • pseudo-instructions, classified by their canonical expansions (MVaddi, NOTxori, NEGsub, LIlui+addi, LAauipc+addi), all Zkt-listed;
    • loads and stores, which Zkt does not cover: the address is already leaked by the Jasmin leakage model, and independence from the transferred values is assumed, as on the other architectures (Intel's DOIT list contains MOV, ARM's DIT covers LDR/STR), so they stay DOIT;
    • the HINT caveat raised in the issue: Zkt exempts HINT encodings (typically rd = x0) from the latency requirement, but Jasmin can never emit one since x0 is not part of the declared register file.
  • riscv_arch_full.ml: is_ct_asm_op returns false for DIV/DIVU/REM/REMU (the FIXME RISCV is resolved), matching the x86/ARM convention of assuming everything but division to be constant-time.
  • Tests: new CCT-riscv and CCT-DOIT-riscv categories with six tests: secret #DIV/#REM rejected by the plain CT checker, secret / and % rejected under --doit (both were wrongly accepted before this change), public division accepted, and secret mul/add/xor/shift/spill accepted under --doit.
  • The Zkt reference is added next to the Intel and ARM ones in docs/source/tools/ct.md.

Validation: full proofs build, extraction and compiler build are green; CCT, CCT-riscv, CCT-DOIT, CCT-DOIT-riscv, SCT (43/43) and the risc-v compilation category (106/106) all pass.

They have data-dependent latency on typical implementations and are
deliberately excluded from the Zkt ("Data-Independent Execution Latency
Subset") safe list of the RISC-V specification, which is the reference
for data operand independent timing on this architecture.

The DOIT classification of every RISC-V instruction is now written
explicitly in the instruction descriptors and documented against the
Zkt list.  Loads and stores, which Zkt does not cover, keep the same
assumption as on the other architectures: the address is leaked, and
the latency is assumed not to depend on the transferred values.
Pseudo-instructions are classified according to their canonical
expansions.  Zkt exempts HINT encodings (rd = x0) from the latency
requirement, but Jasmin cannot emit them: x0 is not part of the
declared register file.

Fixes jasmin-lang#1013
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

RISC-V: CT and doit are wrong

1 participant