RTL2M$\mu$PATH: Multi-$\mu$PATH Synthesis with Applications to Hardware Security Verification
<|reference_start|>RTL2M$\mu$PATH: Multi-$\mu$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 $\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.<|reference_end|>
@article{hsiao2024rtl2m$\mu$path:,
    title={RTL2M$\mu$PATH: Multi-$\mu$PATH Synthesis with Applications to Hardware
  Security Verification},
    author={Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan, Gustavo
  Petri, Christopher W. Fletcher, and Caroline Trippel},
    journal={arXiv preprint arXiv:2409.19478},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.19478},
    primaryClass={cs.CR cs.AR}
}