Model one-operand imul as a signed multiply in the assembly checker (scrutineer #2514)

[JasonGross]

Fixes scrutineer security finding #2514 (CWE-682): One-operand imul is modelled as an unsigned multiply in both the symbolic executor and the concrete semantics, so its rdx high word is wrong whenever an operand has its top bit set.

The bug

src/Assembly/Symbolic.v (SymexNormalInstruction) and src/Assembly/WithBedrock/Semantics.v (DenoteNormalInstruction) handled the one-operand forms of mul and imul in one shared branch, | (Syntax.mul | imul), [src2] =>, computing the unsigned full product and writing its high word to rdx (ah for 8-bit operands). On x86-64, mul r/m64 is unsigned but one-operand imul r/m64 is signed (Intel SDM Vol. 2A, IMUL). The low words agree; the high words differ whenever an operand has bit 63 set. E.g. with rax = 0xffffffff00000001 (top limb of the P-256 prime) and rcx = 3, hardware imul rcx gives rdx = 0xffffffffffffffff while both models gave 0x2.

So the --hints-file equivalence checker accepted assembly using imul rcx where the reference computation needs the unsigned high word (mul/mulx), i.e. it certified non-equivalent assembly. The two- and three-operand imul forms only write the low half and were already correct.

The fix

The shared branch is split:

• mul keeps exactly its previous (unsigned) definition in both models.
• One-operand imul:
  • concrete semantics: the high word is Z.land (Z.shiftr (Z.signed s v1 * Z.signed s v2) s) (Z.ones s); the low word is still v1 * v2 (equal to the signed product after truncation);
  • symbolic executor: the high word is shr s (mulZ (signed a) (signed b)) s where signed x := addZ (add s x (2^(s-1))) (-(2^(s-1))), which is Z.signed s x unfolded, expressed with the existing operators (no new op constructor, so no changes to the rewriting passes or their proofs). This lives in a new definition SignedMulHigh (next to SymexNormalInstruction) rather than inline; see below for why. The low word is the unsigned mulZ product as before. Flags are havocked as before. The 8-bit form (ah:al) goes through the same code.
• SymbolicProofs.v: SymexNornalInstruction_R unfolds SignedMulHigh together with SymexNormalInstruction and gains a four-line case relating the unfolded sign extension to Z.signed.
• EquivalenceProofs.v: same_reg_some_of_success / same_mem_addressed_of_success instances for SignedMulHigh, derived by typeclasses eauto exactly like the Symeval ones, and Typeclasses Opaque SignedMulHigh.
• New src/Assembly/WithBedrock/SemanticsTests.v pins down the hardware values of mul/imul (64-bit and 8-bit; top bit set/clear; low and high words; untouched upper bytes for the 8-bit form) for both the concrete semantics and the symbolic executor (symbolic execution from init_symbolic_state, then interp_expr with concrete values for the rax/rcx symbols). The imul cases fail against the previous model (checked by compiling the test against the previously installed library: Unable to unify "Some 18446744073709551615" with "Some 2").

Alternatives considered: adding a dedicated signed-multiply / sign-extension op (rejected: every op enumeration, Show instance, and rewriting-pass proof would need a case, for an instruction the shipped corpus never uses); rejecting one-operand imul outright (rejected: the correct semantics is expressible with existing operators and the proofs go through). Two formulations were tried and rejected on proof-performance grounds: nesting the whole high-word expression in a single Symeval pre-expression inline in the branch made the Qed of SymexNornalInstruction_R take over an hour in the kernel (the tactics themselves ran in seconds); splitting it into several Symeval/App binds inline instead made the generic tactic behind SymexNormalInstruction_reg_same/_mem_same in EquivalenceProofs.v run for over 40 minutes (it is exponential in the number of binds in a branch; the unmodified file takes 50 s). Factoring the computation into SignedMulHigh, which those proofs treat as a unit like Symeval, brings every file back to its usual compile time.

Verification

All compiled with the overlay recipe (coqc -q -R src Crypto ... against the installed coq-fiat-crypto-with-bedrock, with src/Assembly/WithBedrock/Semantics.v compiled locally from HEAD since the installed copy differs):

• src/Assembly/WithBedrock/Semantics.v, src/Assembly/Symbolic.v (43 s), src/Assembly/Equivalence.v, src/Assembly/WithBedrock/SymbolicProofs.v (47 s; unmodified master: 41 s), src/Assembly/EquivalenceProofs.v (52 s; unmodified master: 50 s), src/Assembly/WithBedrock/Proofs.v (2 min), src/Assembly/WithBedrock/SemanticsTests.v (2 s): all compile.

• Binary chain BoundsPipeline.v → PushButtonSynthesis/*.v → CLI.v → StandaloneOCamlMain.v → ExtractionOCaml/word_by_word_montgomery.v → ocamlfind ocamlopt: builds.

• End-to-end demo with that binary: took fiat-amd64/fiat_p256_mul/seed0000000015492029_ratio16518.asm and rewrote its first mulx r11, r10, [rax+0x10] (whose rdx is reloaded immediately and whose flags are dead) as mov rcx, rdx; mov rax, [rsi+0x10]; mov r11, [rcx+0x10]; {mul|imul} r11; mov r10, rax; mov r11, rdx; mov rax, rcx, then ran word_by_word_montgomery p256 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' mul --hints-file <file>:

  binary	mul r11 variant	imul r11 variant
  installed pre-fix fiat_crypto word-by-word-montgomery	accepted (exit 0)	accepted (exit 0) — the bug
  this branch's word_by_word_montgomery	accepted (exit 0)	rejected (exit 2, Equivalence checking error: Unable to unify ...)

• Shipped CryptOpt corpus: grep finds no one-operand imul in fiat-amd64/ (only the three-operand form and mulx). Re-ran the gentest.py invocations for all word-by-word Montgomery curves with the final rebuilt binary: p224, p256, secp256k1_montgomery, p384, p434 (× mul, square; 300 hints files in 10 invocations) all verify (exit 0; the p434 invocations take ~70-80 min each).

Not verified: the full make (CI will do it), the Haskell/JS extraction targets, and anything outside the cone listed above.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD