What does this research mean for the field?

A design-stage security verification framework integrating gate-level information flow tracking (GLIFT) with formal verification effectively detects and enables the validation of Spectre-class vulnerabilities in high-performance RISC-V processors. Novelty: ClaimNovelty.METHODOLOGICAL. Consensus alignment: ConsensusAlignment.NEUTRAL.

What question did this study set out to answer?

This work aims to develop a framework that detects Spectre vulnerabilities in RISC-V processors at the design stage.

June 17, 2026Open Access

Information-flow-analysis-based detection of spectre vulnerabilities in RISC-V processors

Key Points

This work aims to develop a framework that detects Spectre vulnerabilities in RISC-V processors at the design stage.
Integrates gate-level information flow tracking with formal verification.
Develops GLIFT models from synthesized RTL netlists to track confidentiality tags.
Instantiates Spectre-oriented properties as system verilog assertions verified with exhaustive state exploration.
Identifies violations of permission checks for speculative memory accesses across architectures.
Uncovers flaws in speculative propagation of microarchitectural state, leading to residual effects post-misspeculation.
Demonstrates practical exploits that can recover secrets through various cache and timing channel methods.

Abstract

RISC-V's openness and modularity have accelerated adoption in high-performance processors, yet deep microarchitectural optimizations such as speculative execution and advanced prediction expose designs to Spectre-class transient execution attacks. This paper presents a design-stage security verification framework that integrates gate-level information flow tracking (GLIFT) with formal verification to proactively detect Spectre vulnerabilities in RISC-V processors. From synthesized RTL netlists (via Yosys), this paper automatically derive GLIFT models that track bit-precise confidentiality tags across logic, and this paper formalize three generic, Spectre-oriented properties: enforcing permission checks for speculative memory accesses, constraining speculative propagation of microarchitectural state (e.g., caches and TLB), and guaranteeing post-misspeculation recovery consistency. These properties are instantiated as system verilog assertions within the load-store unit and data cache and verified using questa formal with exhaustive state exploration. On SonicBOOM and Xuantie-910, the framework uncovers violations of all three properties, showing that speculative loads can bypass authorization, taint cache state during speculation, and leave residual effects that are not fully rolled back. Guided by formal counterexamples, this paper implement practical exploits to validate impact: a port-contention timing channel on SonicBOOM and a Flush+Reload cache channel on Xuantie-910, and we realize eight Spectre variants (PHT, BTB, RSB, SSB) that successfully recover secrets with quantifiable leakage. Empirical results indicate higher throughput for variants requiring limited predictor mistraining, while cache-based channels entail broader probing than contention channels but remain reliable with calibrated thresholds. The proposed approach bridges ISA intent and concrete microarchitectural effects, offering reusable properties, automated GLIFT modeling, and a closed loop from verification to exploit validation, thereby informing principled, proactive hardening of future RISC-V microarchitectures.

AIに質問

Bookmark

View Full Paper