{"id":"be785745-9c26-4a46-afff-546bece6c4a5","arxiv_id":"2607.27480","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A Rocq-verified proof chain shows that a constant-time Salsa20 binary running on a synthesizable, pipelined RISC core has cycle-level timing independent of secrets, without trusting the ISA contract.","lead":"Granite presents a machine-checked methodology for proving that a pipelined RISC processor's cycle-by-cycle timing leaks nothing beyond what an ISA leakage contract declares public. It composes processor, submodule, and software static-analysis proofs down to synthesizable RTL, including a Salsa20 case study.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Unverified Quartz-to-SystemVerilog pretty-printer leaves the actual RTL outside the machine-checked theorem; the 'synthesizable RTL' claim is conditional on a 200-line TCB component.","rationale":"I read the paper in good faith and found no circularity or internal inconsistency in the core refinement argument: Definition 2's trace-equivalence formulation is a reasonable formalization of contractual noninterference, and the existential driver/witness/leakage-transformer construction avoids the classical refinement pitfall because the driver is restricted to public data and the witness only affects unobserved outputs. Theorem 2's proof sketch is valid under the stated definitions. The reader's weakest-assumption list is accurate, but I would sharpen it: the policy-completeness part is actually discharged by the machine-checked proof for the specific verified design (if the hardware had a secret-dependent timing effect outside the leakage trace, no leakage transformer could explain the observation trace, so the trace-equivalence proof would be impossible). The genuinely load-bearing residual concern is the unverified translation from the verified model to actual RTL: the pretty-printer is in the TCB, so the machine-checked theorem does not cover the SystemVerilog artifact. Likewise, the abstract memory model is trusted, so the guarantee does not extend to a concrete memory hierarchy. Both are explicit limitations, but they directly weaken the strongest claim that the proof is 'foundational' down to synthesizable RTL. The reader's CONDITIONAL verdict already reflects these gaps; my analysis does not move it to REJECT or UNVERDICTED because the disclosed TCB components are small, clearly scoped, and standard in this line of work. The concrete test I propose would settle whether the pretty-printer gap actually lands by either closing it with a formal proof or exposing a real miscompilation risk.","tokens_in":26053,"tokens_out":16144,"duration_ms":175700,"concrete_test":"Formally verify the Quartz-to-SystemVerilog pretty-printer against a formal semantics for the generated SystemVerilog subset (e.g., the semantics of Choi et al., OOPSLA 2025, cited in the paper), proving that the cycle-level transition relation of the Quartz design is preserved. If this proof succeeds, the TCB gap is closed; if it fails, the end-to-end RTL claim is not established. A quicker but weaker check: run differential cycle-level testing between the generated SystemVerilog in a simulator and the Gallina/Quartz model on the Salsa20 binary with multiple random secret keys, comparing the full MMIO ready/valid trace; any mismatch would confirm the concern.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The strongest end-to-end claim is that a single Rocq theorem proves cycle-by-cycle confidentiality of a cryptographic implementation from source-level constant-time down to synthesizable RTL. But the proof chain in §7.2 terminates at a Quartz/Gallina model, not at the generated SystemVerilog: the 200-line syntax-mapping function is explicitly in the TCB. If that pretty-printer miscompiles any construct used by the processor, the fabricated RTL could exhibit a timing side channel that no Rocq theorem covers, while every machine-checked proof remains valid. The paper discloses this (§7.2), but it is still load-bearing because it is the only link between the verified model and the claimed artifact. A parallel trusted gap is the abstract memory spec (§5.2.2): the end-to-end theorem assumes a memory whose response time depends only on addresses, and no concrete memory implementation is verified. A real memory with data-dependent latency (e.g., DRAM refresh/row conflicts depending on stored values) would invalidate the practical guarantee without falsifying any Rocq statement. These are trust gaps rather than internal inconsistencies, but they mean the headline 'foundational verification of hardware-software leakage contracts' is conditional on unverified translation and memory models. The policy-completeness concern raised by the reader is less decisive: the machine-checked trace-equivalence proof itself certifies that the verified RTL has no timing dependency outside the leakage policy, so the policy is validated for this design, not merely assumed.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Granite, a methodology formalized in Rocq for verifying both functional correctness and nonleakage of processor RTL against ISA-level leakage contracts. The central construction is 'leakage-aware refinement via determinism': the authors lower a one-instruction-at-a-time ISA with a leakage function into a cycle-accurate deterministic specification machine parameterized by an untrusted secret-independent driver, an untrusted witness, and a leakage transformer. An implementation satisfies the contract if there exist instantiations of these parameters under which the implementation and specification traces are equivalent, thereby discharging both correctness and confidentiality as a single trace-equivalence obligation. The methodology is demonstrated on a four-stage pipelined RISC-V core with branch prediction, precise interrupts, MMIO, and a zero-skip multiplier, and composed with a certified static analysis to obtain a noninterference theorem for a Salsa20 binary. The authors are explicit that the Quartz-to-SystemVerilog pretty-printer and the abstract memory specification remain in the trusted computing base.","tokens_in":26336,"tokens_out":5072,"duration_ms":55324,"significance":"If the claims are accepted at face value, this is a substantial advance: it is the first modular, machine-checked connection between ISA-level leakage contracts and cycle-level microarchitectural behavior, supporting nondeterminism without the usual refinement-based leak-explanation problem. The case study is nontrivial—it includes speculation, precise interrupts, and I/O—and the paper's explicit TCB accounting is a strength. The modular substitution principle and the reuse of functional-correctness proof structure for confidentiality are valuable contributions. However, the headline 'foundational verification of hardware-software leakage contracts' is conditional on two trusted components: the Quartz-to-SystemVerilog pretty-printer and the abstract memory model. The policy-completeness concern raised in the stress-test note is real but less decisive: the machine-checked trace-equivalence proof does certify nonleakage relative to the stated declassification policy, but the policy itself is hand-written and was found incomplete during the authors' own verification. Overall, the central derivation appears sound, but the scope of the claims needs significant tightening.","major_comments":[{"comment":"The end-to-end theorem is proved for the Quartz/Gallina model, not for the generated SystemVerilog: the 200-line syntax-mapping function is explicitly in the TCB. Therefore the abstract's claim of 'a single Rocq theorem about cycle-by-cycle confidentiality of a hardware-and-software cryptographic implementation—eliminating every intermediate specification' is technically true only up to the pretty-printer. The synthesizable RTL artifact is not covered by the machine-checked theorem. This is disclosed, but it is load-bearing for the paper's 'synthesizable RTL' and 'foundational' claims. The authors should either verify the translation (e.g., by connecting to an RTL equivalence checker) or explicitly scope the main theorem to the Quartz model and present the RTL claim as conditional on translation correctness.","section":"§7.2 and Abstract"},{"comment":"The abstract memory specification is trusted: the end-to-end noninterference theorem assumes that memory response time depends only on public information (addresses). No concrete memory implementation is verified against this specification. Consequently, a memory with secret-dependent latency—e.g., DRAM row conflicts or refresh timing that depends on stored values—would invalidate the practical guarantee while leaving every Rocq statement true. The paper should either verify a concrete memory against the abstract spec or state prominently in the abstract/introduction that the guarantee excludes memory implementations not satisfying the abstract memory model.","section":"§5.2.2 and §8.1"},{"comment":"The leakage contract's declassification policy is hand-written and not proven complete. The authors' own experience in §6—the proof could not be completed without adding leakage of writes to mie/mtvec—demonstrates that the policy can omit timing-relevant architectural events. Thus the abstract's claim of 'conclusively rules out information leakage through known and unknown timing side channels' overstates the result: it rules out channels expressible in the contract's declassification events, but not channels omitted by the policy. To support the stronger claim, the paper would need a policy-completeness argument (e.g., a formal enumeration of all microarchitectural events that can influence cycle-level timing, mapped to leak events), or the claims should be weakened to 'no leakage beyond the declassified events specified by the contract.'","section":"§3.2 and §6"}],"minor_comments":[{"comment":"The starred nodes and the 'Focus' label in the proof-structure diagram are not explained; please clarify what the asterisks indicate or remove them.","section":"Figure 2"},{"comment":"The two definitions use different step counts (n for the ISA trace, m for the microarchitectural trace) without explicit comment. State clearly that these are independent and that the quantifier order matters.","section":"Definitions 1 and 2"},{"comment":"The Beq-Spin rule uses 'interruptsDisabled(st)' but there is no corresponding discussion of how interrupts are modeled in the static analysis; clarify whether interrupts are assumed disabled for the entire analyzed program or only for the spin loop.","section":"Figure 8"},{"comment":"The text refers to 'RISCV-COQ' in §3.2; please ensure that the citations [8,15] are presented consistently with their actual titles and venues.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"This is a strong methodology paper with credible machine-checked proofs and an unusually honest TCB section. My main concern is that the abstract and introduction overstate the end-to-end RTL claim given that the pretty-printer and the memory specification are trusted. The technical core is sound, but the central claims need to be scoped precisely; otherwise readers may take the 'synthesizable RTL' and 'foundational' statements to mean more than what is proved. The policy-completeness issue is inherent to leakage-contract approaches but should be acknowledged in the main text rather than left to the reader's inference from §6."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Granite is worth your time if you care about whether constant-time guarantees can be made to survive contact with real microarchitecture. The central move is to determinize the ISA-level specification with existential parameters — an untrusted secret-independent driver for resolution of nondeterminism and an untrusted witness for secret-dependent unspecified outputs — then prove trace equivalence between implementation and spec. The witness can depend on secrets because it only affects outputs the adversary is not allowed to observe. That sounds like a small trick, but it is the right one: it lets the proof go through without either underspecifying (allowing secret-dependent choice) or overspecifying (ruling out legitimately variable latencies).\n\nThe modularity story is also genuine. Submodules get their own leakage contracts, with a substitution principle, so the whole-processor proof goes through once. The case study — a four-stage pipelined RISC core with speculation, precise interrupts, and I/O, plus a Salsa20 binary through a certified static analysis — is exactly the kind of integration the field needs. I also give them credit for honesty: they report that the proof forced them to add CSR-write leakage to the contract. That is evidence the methodology catches policy omissions, not that the policy was rigged.\n\nThe weak spots are real but disclosed. The Quartz-to-SystemVerilog pretty-printer is in the TCB, so the synthesizable RTL claim is not machine-checked; and the abstract memory model is trusted, so data-dependent memory timing is out of scope. Those temper the \"single Rocq theorem\" slogan but don't undercut the contribution. The leakage policy is hand-written — the guarantee is relative to it — but the trace-equivalence proof does certify that the verified design has no timing dependence outside that policy. That is the best one can do without a formal theory of what the policy ought to be.\n\nI'd send this to peer review. The artifacts need to be checked — the Rocq development is the one thing I couldn't inspect from the text — and the TCB discussion should be sharpened, but the methodology is coherent and the result is new. It deserves a serious referee.","headline":"A serious, machine-checked advance in RTL leakage verification; the real caveats are the unverified pretty-printer and the hand-chosen policy, not the refinement story.","tokens_in":26879,"tokens_out":3261,"would_cite":true,"duration_ms":33759,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Granite claims that cycle-by-cycle timing of a verified pipelined RISC core provably depends only on the observables a hand-written ISA leakage contract declassifies, and that a constant-time Salsa20 binary running on the core leaks nothing","keywords":["timing side channels","noninterference","leakage contracts","RTL verification","refinement","constant-time programming","RISC-V","formal verification"],"falsifier":"Run the pretty-printed SystemVerilog on an FPGA or simulator with two secret inputs that agree on every declassified event (branch conditions, load/store addresses, multiplier zero flags, instruction bytes, and writes to interrupt-configuration CSRs) but differ in some other register or memory value, and check whether the cycle-by-cycle MMIO ready/valid traces diverge; any divergence would falsify the end-to-end noninterference theorem.","tokens_in":25890,"feed_emoji":"🔒","tokens_out":5519,"duration_ms":48489,"temperature":0.7,"pith_summary":"Granite argues that the timing side-channel problem for processors can be closed by a single, auditable, instruction-set-level leakage contract, provided the contract's nondeterminism is determinized rather than abstracted. The paper's central claim is that a pipelined RISC implementation—with speculation, precise interrupts, and MMIO—is functionally correct and non-leaking exactly when it is trace-equivalent to a cycle-accurate specification machine parameterized by three untrusted black boxes: a secret-independent driver, an unconstrained witness, and a leakage transformer. Composing this with a certified static analysis of constant-time code yields a machine-checked theorem that a Salsa20 binary's cycle-by-cycle MMIO observations are identical for any two secrets, with the ISA contract itself removed from the trusted computing base. A sympathetic reader should care because this is the first modular, foundational connection between ISA-level leakage contracts and wire-level cycle-accurate RTL—making timing leaks a proof obligation rather than an empirical hunt.","feed_headline":"Verified RISC core: cycle timing leaks only contract-allowed data","feed_subtitle":"A modular proof chain links constant-time Salsa20 to RTL, removing the ISA contract from the trusted base.","key_machinery":"The central device is leakage-aware refinement via determinism: a one-instruction-at-a-time ISA machine with a leakage function is lowered to a cycle-accurate Mealy machine and then determinized by existentially parameterizing it with three untrusted functions—a driver that resolves secret-independent choices (when to step, when to take an interrupt, when to issue I/O) from public data, a witness that supplies unspecified possibly-secret outputs, and a leakage transformer that maps declassified leakage events to adversary observations. The proof obligation is a single trace-equivalence statement between implementation and the parameterized spec machine, established by a cycle-by-cycle bisimu","core_discovery":"On Granite's terms: correctness and confidentiality are not separate properties but two faces of one trace-equivalence fact. An implementation satisfies a leakage-aware ISA contract when there exist a leakage transformer, a secret-independent driver, and an unconstrained witness such that for every cycle count and every public/secret input pair, the implementation's output trace equals the trace of the deterministic cycle-accurate specification built from the trusted ISA machine and those parameters. The paper reports this proof for a four-stage pipelined RISC-V core with branch prediction, precise exceptions and interrupts, and a ready/valid MMIO interface, and then extends it through a Qua","pith_inferences":["The driver/witness/leakage-transformer decomposition suggests a template for other declassification policies: any policy expressible as a public-trace function can be verified with the same shadow-core recipe, though policies that declassify richer data (for example, exponent values) would need a more informative shadow machine.","Because the guarantee is trace-equivalence against a cycle-accurate spec, the same machinery could in principle verify non-timing microarchitectural side channels by changing only the observation function—but power or EM observations would require a different observation boundary and likely a different leakage transformer, which the framework leaves unconstrained.","A practical negative test for transferability: apply the same contract to a different RISC-V core with a subtle secret-dependent stall not listed in the policy; the proof should fail to construct the shadow machine, providing evidence that the policy is incomplete.","The reliance on a deterministic HDL fragment and a single clock domain means multi-clock and asynchronous designs would require new machinery; one could probe whether the one-method-at-a-time semantics extends to synchronous clock-domain-crossing interfaces with handshake-based crossing points."],"forward_implications":["Any timing difference visible at the digital I/O boundary of the verified core is a function only of the declassified leakage; unknown future timing attacks of the same class are ruled out without enumerating them.","The RTL implementation and the existential parameters are removed from the trusted computing base; only the cycle-level ISA contract, memory model, external-world model, the proof kernel, and the pretty-printer remain trusted.","The methodology composes with software-level constant-time proofs, so the hardware-software contract is an intermediate specification rather than a trust anchor.","The same ISA contract admits multiple microarchitectures (such as the four-stage pipelined core and a three-stage multicycle core) without changes to the contract.","Submodule contracts capture both correctness and leakage independently, allowing designers to swap implementations or reason about early-stage designs and defenses without redoing the top-level proof."],"fun_headline_variants":["Verified RISC-V core: timing leaks only contract-allowed data","Modular proof ties constant-time code to RTL, no ISA trust","Leakage-aware refinement: one proof for correctness and confidentiality","Hardware-software leakage contracts proven from RTL to Rocq"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The hand-written leakage contract must list every architectural event that can influence cycle-level timing; a secret-dependent effect missing from the list would not be ruled out by the proof.","fun_headline_variants_meta":{"raw":{"variants":["Verified RISC-V core: timing leaks only contract-allowed data","Modular proof ties constant-time code to RTL, no ISA trust","Leakage-aware refinement: one proof for correctness and confidentiality","Hardware-software leakage contracts proven from RTL to Rocq"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000127,"raw_usage":{"total_tokens":990,"prompt_tokens":820,"completion_tokens":170,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":564,"completion_tokens_details":{"reasoning_tokens":95}},"tokens_in":564,"tokens_out":170,"duration_ms":2768,"temperature":1.0,"reasoning_tokens":95,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T07:11:36.941565+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the pretty-printed SystemVerilog on an FPGA or simulator with two secret inputs that agree on every declassified event (branch conditions, load/store addresses, multiplier zero flags, instruction bytes, and writes to interrupt-configuration CSRs) but differ in some other register or memory value, and check whether the cycle-by-cycle MMIO ready/valid traces diverge; any divergence would falsify the end-to-end noninterference theorem.","supporting_citations":[],"review_version":1}