Institute of Information Science, Academia Sinica

The Check Tools automate formal memory consistency model and security verification of processors by analyzing abstract axiomatic 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’ adoption. A core set of axioms that comprise a μSPEC model encode all reachable microarchitectural execution paths (μPATH) per implemented instruction. Towards narrowing the μSPEC-RTL verification gap, we propose RTL2MμPATH, an automated approach/tool for synthesizing (uncovering) a complete set of formally verified μPATHs (and their corresponding μSPEC axioms) per instruction on a given SystemVerilog processor design. In designing RTL2MμPATH, we make an important security-related 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 propose an automated approach/tool, called SynthLC, that extends RTL2MμPATH to synthesize a comprehensive set of formally verified leakage signatures from SystemVerilog processor designs. Leakage signatures capture all microarchitectural features required to implement state-of-the-art defenses against hardware side-channel attacks. SynthLC is the first/only automated methodology for formally verifying hardware adherence to them.

Yao Hsiao is a Ph.D. student at Stanford University advised by Prof. Caroline Trippel. Her research focuses on design of new methodologies and tools for formally verifying the memory consistency model implementations and side-channel security of microarchitectures.