RTL2MuPATH: Multi-uPATH Synthesis with Applications to Hardware Security Verification

From bibtex.

Abstract

The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called uSPEC models. Despite the efficacy of this approach, a verification gap between uSPEC models, which must be manually written, and RTL limits the Check tools' broad adoption. Our prior work, called RTL2uSPEC, narrows this gap by automatically synthesizing formally verified uSPEC models from SystemVerilog implementations of simple processors. But RTL2uSPEC assumes input designs where an instruction (e.g., a load) cannot exhibit more than one microarchitectural execution path (uPATH, e.g., a cache hit or miss path) -- its single-execution-path assumption. In this paper, we first propose an automated approach and tool, called RTL2MuPATH, that resolves RTL2uSPEC's single-execution-path assumption. Given a SystemVerilog processor design, instruction encodings, and modest design metadata, RTL2MuPATH finds a complete set of formally verified uPATHs for each instruction. Next, we make an important observation: an instruction that can exhibit more than one uPATH strongly indicates the presence of a microarchitectural side channel.