Researchers from MIT, Google, and University of Washington published a technical paper titled “Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts.” Abstract Excerpt: “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.” Find the technical paper here. July 2026. Lau, Stella, Andres Erbsen, and Adam Chlipala. “Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts.” arXiv, July 2026. https://doi.org/10.48550/arXiv.2607.27480. The post Modular Verification of RTL Processors Against ISA Contracts (MIT, Google, UW) appeared first on Semiconductor Engineering.
Source: https://semiengineering.com/modular-ver ... google-uw/