The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $\mu$SPEC models. Despite the efficacy of this approach, a verification gap between $\mu$SPEC models, which must be manually written, and RTL limits the Check tools' broad adoption. Our prior work, called RTL2$\mu$SPEC, narrows this gap by automatically synthesizing formally verified $\mu$SPEC models from SystemVerilog implementations of simple processors. But, RTL2$\mu$SPEC assumes input designs where an instruction (e.g., a load) cannot exhibit more than one microarchitectural execution path ($\mu$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$\mu$PATH, that resolves RTL2$\mu$SPEC's single-execution-path assumption. Given a SystemVerilog processor design, instruction encodings, and modest design metadata, RTL2M$\mu$PATH finds a complete set of formally verified $\mu$PATHs for each instruction. Next, we make an important observation: an instruction that can exhibit more than one $\mu$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$\mu$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.

翻译：Check工具通过分析称为$μ$SPEC模型的微架构抽象模型，实现了处理器形式化内存一致性模型与安全验证的自动化。尽管该方法有效，但需要手动编写的$μ$SPEC模型与RTL之间的验证鸿沟限制了Check工具的广泛采用。我们先前的工作RTL2$μ$SPEC通过从简单处理器的SystemVerilog实现中自动综合形式化验证的$μ$SPEC模型，缩小了这一鸿沟。然而，RTL2$μ$SPEC假设输入设计中一条指令（例如加载指令）不能表现出超过一种微架构执行路径（$μ$PATH，例如缓存命中或未命中路径）——即其单执行路径假设。在本文中，我们首先提出了一种自动化方法与工具RTL2M$μ$PATH，以解决RTL2$μ$SPEC的单执行路径假设。给定一个SystemVerilog处理器设计、指令编码及适度的设计元数据，RTL2M$μ$PATH可为每条指令找到一组完整的形式化验证的$μ$PATH。接着，我们提出一个重要观察：一条能够表现出超过一种$μ$PATH的指令，强烈暗示输入设计中存在微架构侧信道。基于此观察，我们进一步提出了一种自动化方法与工具SynthLC，它扩展了RTL2M$μ$PATH，通过符号化信息流分析来支持从SystemVerilog处理器设计中综合多种形式化验证的泄漏契约。泄漏契约是当前最先进的硬件侧信道攻击防御措施的基础。SynthLC是首个用于形式化验证硬件是否遵循泄漏契约的自动化方法。