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

Abstract

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 SystemVerilog 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 SystemVerilog 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 SystemVerilog processor designs. Leakage contracts are foundational to state-of-the-art defenses against hardware side-channel attacks. SynthLC is the first automated methodology for formally verifying hardware adherence to them.