RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security Verification

The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called μSPEC models. Despite the efficacy of this approach, a verification gap between μSPEC models, which must be manually written, and RTL limits the Check tools' broad adoption. Our prior work, called RTL2μSPEC, narrows this gap by automatically synthesizing formally verified μSPEC models from System Verilog implementations of simple processors. But, RTL2μSPEC assumes input designs where an instruction (e.g., a load) cannot exhibit more than one microarchitectural execution path (μPATH, 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 RTL2MμPATH, that resolves RTL2μSPEC's single-execution-path assumption. Given a System Verilog processor design, instruction encodings, and modest design metadata, RTL2MμPATH finds a complete set of formally verified μPATHS for each instruction. Next, we make an important observation: an instruction that can exhibit more than one μPATH strongly indicates the presence of a microarchitectural side channel in the input design. Based on this observation, we then propose an automated approach and tool, called Synthlc, that extends RTL2MμPATH with a symbolic information flow analysis to support synthesizing a variety of formally verified leakage contracts from System Verilog processor designs. Leakage contracts are foundational to state-of-the-art defenses against hardware side-channel attacks. SYnthlcis the first automated methodology for formally verifying hardware adherence to them.