Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan, Gustavo Petri, Christopher W. Fletcher, Caroline Trippel

TL;DR

This work addresses the gap between manually specified $μ$SPEC models and RTL implementations by introducing rtl2$m$u$path, which automatically synthesizes a complete set of cycle-accurate $μ$paths from SystemVerilog RTL. It then extends this analysis with SynthLC, a symbolic information-flow framework that derives leakage signatures and formally verified leakage contracts, enabling hardware-side-channel defenses to be applied to realistic cores such as CVA6. The CVA6 case study demonstrates 72 transponders and 26 transmitters producing 94 leakage signatures in the core and reveals leakage channels in the cache, illustrating scalability and practical relevance for hardware security verification. Together, these tools provide a fully automated pipeline from RTL to leakage-contract verification, supporting more robust defenses against microarchitectural side channels. The work advances formal verification by connecting RTL-level execution variability directly to concrete leakage contracts and defense mechanisms, with implications for both software- and hardware-based countermeasures.

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.

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

TL;DR

This work addresses the gap between manually specified SPEC models and RTL implementations by introducing rtl2uμ$paths from SystemVerilog RTL. It then extends this analysis with SynthLC, a symbolic information-flow framework that derives leakage signatures and formally verified leakage contracts, enabling hardware-side-channel defenses to be applied to realistic cores such as CVA6. The CVA6 case study demonstrates 72 transponders and 26 transmitters producing 94 leakage signatures in the core and reveals leakage channels in the cache, illustrating scalability and practical relevance for hardware security verification. Together, these tools provide a fully automated pipeline from RTL to leakage-contract verification, supporting more robust defenses against microarchitectural side channels. The work advances formal verification by connecting RTL-level execution variability directly to concrete leakage contracts and defense mechanisms, with implications for both software- and hardware-based countermeasures.

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 RTL2SPEC, narrows this gap by automatically synthesizing formally verified SPEC models from SystemVerilog implementations of simple processors. But, RTL2SPEC 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 RTL2MPATH, that resolves RTL2SPEC's single-execution-path assumption. Given a SystemVerilog processor design, instruction encodings, and modest design metadata, RTL2MPATH 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 RTL2MPATH 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.
Paper Structure (46 sections, 5 equations, 8 figures, 2 tables)

This paper contains 46 sections, 5 equations, 8 figures, 2 tables.

Table of Contents

  1. Introduction
  2. This Paper
  3. Background
  4. Hardware Side-Channel Attacks
  5. Hardware Side-Channel Defenses & Leakage Contracts
  6. SynthLC Approach: Formalizing Microarchitectural Execution Paths
  7. Motivating Example: Operand Packing
  8. Extending $\mu$hb Graphs with Cycle-Accurate Timing
  9. Recognizing $\mu$hb Nodes with Performing Locations
  10. SynthLC Approach: Applying Multi-upath Synthesis to Hardware Security Verification
  11. Illustrative Example: Store-to-Load Stalling
  12. Formalizing Instances of upath Variability with Decisions
  13. Selecting a Decision with a Path Selector Function
  14. Unifying Leakage Contracts with Leakage Signatures
  15. SynthLC Tool: Using RTL2MuPATH to Synthesize Leakage Signatures from Processor RTL
  16. ...and 31 more sections

Figures (8)

  • Figure 1: Two $\mu$paths for $\mathtt{MUL}$ on CVA6-MUL (§\ref{['sec:intro:thispaper']}) and a leakage signature, which defines transponder $\mathtt{MUL}$'s $\mu$path variability as a function of its own operands following its visit to the $\mathtt{mulU}$ PL. Row($\mathtt{1}$/$l$): 1st/$l$-th visit to Row. Node label: value of $l$ for the $\mu$path.
  • Figure 2: $\mathtt{ADD}$$\mu$paths on CVA6-OP (§\ref{['sec:upath_formal']}), using standard $\mu$hb graphs from prior work (\ref{['fig:add_standard']}) and our new cycle-accurate $\mu$hb graphs (\ref{['fig:add_path_1']}, \ref{['fig:add_path_2']}). Row($\mathtt{1}$/$l$): 1st/$l$-th visit to Row. Node label: value of $l$ for $\mu$path.
  • Figure 3: Close proximity of $\mu$FSMs' $\mathtt{iir}$ and $\mathtt{vars}$ components (§\ref{['sec:pls']}). PCRs are added (+) near IIRs that do not hold PCs (§\ref{['sec:both-tool']}).
  • Figure 4: A sampling of $\mu$paths for the CVA6 core (for $\mathtt{BEQ}$, $\mathtt{LD}$) and data cache (for $\mathtt{ST}$), synthesized by rtl2m$\mu$path (§\ref{['sec:results']}). Row($\mathtt{1}$/$l$): 1st/$l$-th visit to Row. Node label: value of $l$ for $\mu$path.
  • Figure 5: Leakage function examples. Implicit inputs and leakage signature components are highlighted. $T^\mathtt{N}/T^\mathtt{D}_\mathtt{O|Y}/T^\mathtt{S}$: intrinsic / older or younger dynamic / static transmitters. PO: program order. $\mathsf{msb}$: most significant bit. $\mathtt{ite(c,t,f)}$: $t$ if $c$ is true; else, $f$.
  • ...and 3 more figures

Theorems & Definitions (1)

  • Definition 5.1: Hardware Side-Channel Safe