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

Stella Lau, Andres Erbsen, Adam Chlipala

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…