AI 中文总结
Granite 是用于验证 RTL 处理器功能正确性与无泄露性的模块化方法，通过泄露感知精化技术建立指令集级泄露契约与微架构执行的关联，结合认证静态分析实现软硬件密码实现的保密性证明。
AI 中文摘要
Granite 是一种用于对 RTL 处理器针对 ISA 契约的功能正确性与无泄露性进行模块化验证的方法。我们证明，具备推测、精确中断及 I/O 的流水线 RISC 设计的逐周期时序，仅由 ISA 泄露契约中指定的可观测变量决定。对于保持可观测变量与秘密无关（即遵循密码学常量时间准则）的程序，该结果排除了通过已知及未知时序侧信道的信息泄露。Granite 的规约仅约束功能正确性与信息流依赖关系，不限制指令周期数、中断处理的指令位置，或乘法器、存储器等子模块的精确延迟。其核心技术是通过确定性实现泄露感知精化，该技术将正确性与保密性共同确立为相对于一系列周期级确定性规范机的迹等价。与秘密无关的不确定性通过用仅作用于公开数据的不可信确定性函数对规范进行存在量化来处理。子模块针对自身的泄露感知规范进行证明，且这些证明可组合为整体设计保证——因此该保证适用于一系列安全实现。我们认为，本工作首次在指令集级泄露契约与微架构特定的逐周期执行及线级观测之间建立了模块化且基础的关联。我们的证明与识别密码学常量时间代码的已认证静态分析相结合，推导得出关于软硬件密码实现逐周期保密性的单一 Rocq 定理——从而将包括 ISA 契约在内的所有中间规范排除在可信计算基之外。
英文摘要
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 design--with speculation, precise interrupts, and I/O--is determined solely by observables specified in an ISA leakage contract. For programs that keep observables independent of secrets (i.e., following the cryptographic-constant-time discipline), this result rules out information leakage through known and unknown timing side channels. Granite's 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. Granite's 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 specs with untrusted, deterministic functions acting only on public data. Submodules are proved against their own leakage-aware specs, and these proofs compose into the whole-design guarantee--which therefore holds over a space of secure implementations. We believe this work is the first to achieve modular and foundational connection between instruction-set-level 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 implementation--eliminating every intermediate specification, including the ISA contract itself, from the trusted computing base.
