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

基于信息流分析的RISC-V幽灵漏洞检测方法

School of Cybersecurity, Northwestern Polytechnical University, Xi'an 710072, China

Received: 23 September 2025

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.

摘要

随着RISC-V指令集架构的快速发展, 其在高性能处理器设计中的广泛应用引发了严峻的安全性挑战。现代处理器中的推测执行机制虽然提升了计算性能, 但也为幽灵等瞬态执行攻击提供了可乘之机。针对传统验证方法在捕获推测执行路径信息泄露行为上的局限性, 提出了一种基于信息流分析的RISC-V处理器安全验证框架。该框架通过构建门级信息流模型, 定义了针对幽灵漏洞的3条通用安全属性: 推测性访存指令权限检查保护、微架构状态传播控制、微架构状态恢复一致性。在SonicBOOM和Xuantie-910 2种代表性RISC-V处理器上的验证实验表明, 所提方法能够有效检测幽灵漏洞风险, 并基于验证反例成功构建了8种攻击变种。实验结果验证了该框架在处理器设计安全验证中的有效性和通用性。