Reject RIP-relative memory operands in the assembly equivalence checker (scrutineer #2516)

[JasonGross]

Fixes scrutineer security finding #2516 (duplicate #2513): RIP-relative memory operands are parsed and stored but ignored by both address models.

The bug

Parse.v records [rip + disp] (and every bare [disp] after a DEFAULT REL line) in the rip_relative field of MEM, but Symbolic.Address (src/Assembly/Symbolic.v) and Semantics.DenoteAddress (src/Assembly/WithBedrock/Semantics.v) never read that field and computed 0 + 0 + disp. Loads and stores through such an operand happened to fail because the folded constant address is not in symbolic memory, but lea never touches memory, so lea rcx, [rip + 0x26] was checked as mov rcx, 0x26. An attacker-supplied --hints-file can replace any mov r64, imm with lea r64, [rip + imm] and have the equivalence checker certify assembly that computes RIP + imm on hardware.

I confirmed this end to end with the installed pre-fix binary (fiat_crypto unsaturated-solinas curve25519 64 5 '2^255 - 19' carry_mul ... --hints-file): a copy of fiat-amd64/fiat_curve25519_carry_mul/seed0000000059842304_ratio12536.asm with line 108 mov rdx, 0x33 replaced by lea rdx, [rip + 0x33] was accepted (exit 0) and the hostile assembly emitted.

The fix

Both models now fail closed, consistently:

• Symbolic.Address raises a new error error.unsupported_rip_relative_addressing <operand> (with a readable Show instance, next to unsupported_label_in_memory) when the operand is explicitly_rip_relative or implicitly_rip_relative. All memory operands (lea, loads, stores) go through Address, so loads and stores now get the explicit error instead of the accidental "index not present" one.
• Semantics.DenoteAddress now returns option Z and is None for RIP-relative and label-based operands; DenoteOperand, SetOperand, and lea propagate that. The machine state has no instruction pointer, so this is the honest semantics and it keeps SymbolicProofs.Address_R true.
• SymbolicProofs.v adapted (Address_R now concludes DenoteAddress ... = Some v; GetOperand_R, R_SetOperand, SetOperand_same rewrite with it). EquivalenceProofs.v and WithBedrock/Proofs.v needed no changes.
• DEFAULT REL lines were already rejected by SymexRawLine (unsupported_line), so the implicit case could not previously reach Address through SymexLines; the new check covers it anyway and a test pins both facts down.
• New regression tests: src/Assembly/SymbolicTests.v (parse + symbolic execution of lea/load/store with [rip + disp], [rip - disp], DEFAULT REL, an implicitly RIP-relative operand as produced by the parser under default_rel := true, a label operand, and a register-relative lea that must still succeed) and src/Assembly/WithBedrock/SemanticsTests.v (DenoteAddress and lea undefined on such operands, defined on an absolute displacement).

Alternatives considered: keeping DenoteAddress : Z and only guarding in DenoteOperand/SetOperand/lea would work but leaves a function that returns a meaningless value for these operands; making DenoteAddress partial is the smaller trust surface. Modelling RIP properly is out of scope, since the symbolic state has no notion of code addresses.

grep -rliw rip fiat-amd64 --include=*.asm finds no shipped assembly using RIP-relative operands, so the existing CryptOpt verification workflow is unaffected.

Verification

Compiled locally with coqc (Rocq 9.4+alpha, -R src Crypto) against the installed coq-fiat-crypto-with-bedrock, recompiling the full downstream cone of the changed files:

• src/Assembly/Symbolic.v, src/Assembly/WithBedrock/Semantics.v (changed) — OK
• src/Assembly/Equivalence.v, src/Assembly/EquivalenceProofs.v, src/Assembly/WithBedrock/SymbolicProofs.v, src/Assembly/WithBedrock/Proofs.v (HEAD versions; the last two differ from the installed build) — OK
• src/BoundsPipeline.v, src/PushButtonSynthesis/{Primitives,SaturatedSolinas,UnsaturatedSolinas,WordByWordMontgomery,BaseConversion,DettmanMultiplication,SolinasReduction}.v, src/CLI.v, src/StandaloneOCamlMain.v, src/ExtractionOCaml/unsaturated_solinas.v — OK
• src/Assembly/SymbolicTests.v, src/Assembly/WithBedrock/SemanticsTests.v (new) — OK

Rebuilt src/ExtractionOCaml/unsaturated_solinas from the extraction with the Makefile.standalone ocamlfind ocamlopt command and ran:

• hostile hints file (line 108 mov rdx, 0x33 → lea rdx, [rip + 0x33]): rejected, exit 2, output ends with Symbolic execution failed: error.unsupported_rip_relative_addressing [rip + 0x33] (RIP-relative memory operands are not supported: the symbolic model has no notion of the instruction pointer).
• the unmodified seed0000000059842304_ratio12536.asm: verified, exit 0.
• the exact fiat-amd64/curve25519-carry_mul.status invocation from gentest.py --makefile with all 30 hints files: verified, exit 0 (about 9 s).

Not verified: a full make (many hours), the other five separate binaries and the JsOfOCaml/Haskell mains (same Coq source, no separate proofs), and the full test-amd64-files suite beyond curve25519 carry_mul. CI should cover those.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD