works on
constant-time discipline 1leakage contracts 1modular verification 1refinement 1timing side channels 1

From the 1 of 1 linked paper with an AI index.

collaborators

1 paper

cs.CR2026

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

Stella Lau, Andres Erbsen, Adam Chlipala

Granite provides a modular framework for formally verifying both functional correctness and the absence of timing side‑channel leaks in RTL processor designs against ISA‑level leak…