Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts

본문 미리보기

arXiv:2607.27480v1 Announce Type: new 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 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