FlagThis

Abstract

Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts. We prove that the cycle-by-cycle timing of a pipelined RISC designwith speculation, precise interrupts, and I/Ois determined solely by observables specified in an ISA leakage contract. For programs that keep observables independent of secrets (i.e., following the cryptographic-constanttime discipline), this result conclusively rules out information leakage through known and unknown timing side channels. Granites specifications only constrain functional correctness and information-flow dependencies: not how many cycles an instruction takes, at which instruction an interrupt is handled, or the exact latencies of submodules such as multipliers and memory. Granites central technique is _leakage-aware refinement via determinism_ , which establishes correctness and confidentiality together as trace equivalence with respect to a family of cycle-level, deterministic spec machines. Secret-independent nondeterminism is handled by _existentially parameterizing_ specifications with untrusted, deterministic functions acting only on public data. Submodules are proved against their own leakage-aware specifications, and these proofs compose into the whole-design guaranteewhich therefore holds over a space of secure implementations. We believe this work is the first to achieve modular and foundational connection between instruction-setlevel leakage contracts and microarchitecture-specific cycle-by-cycle execution with wire-level observations. Our proofs compose with a certified static analysis that recognizes cryptographic-constant-time code to derive a single Rocq theorem about the cycle-by-cycle confidentiality of a hardware-and-software cryptographic implementationeliminating every intermediate specification, including the ISA contract itself, from the trusted computing base.