Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. (arXiv:2305.06979v1 [cs.CR])

Leakage contracts have recently been proposed as a new security abstraction
at the Instruction Set Architecture (ISA) level. Such contracts aim to
faithfully capture the information processors may leak through side effects of
their microarchitectural implementations. However, so far, we lack a
verification methodology to check that a processor actually satisfies a given
leakage contract. In this paper, we address this problem by developing LeaVe,
the first tool for verifying register-transfer-level (RTL) processor designs
against ISA-level leakage contracts. To this …

abstraction aim architecture capture channel check information isa leak may processors security side-channel side effects verification