RISC-V处理器权限正确性验证与提权漏洞自动挖掘方法

唐时博; 朱嘉诚; 慕德俊; 胡伟

doi:10.11999/JEIT250362

RISC-V处理器权限正确性验证与提权漏洞自动挖掘方法

doi: 10.11999/JEIT250362 cstr: 32379.14.JEIT250362

西北工业大学网络空间安全学院西安 710072

基金项目: 国家自然科学基金(U23B2041, 62272389)

详细信息

作者简介:
唐时博：男，博士生，研究方向为处理器安全和形式化安全验证

朱嘉诚：男，博士生，研究方向为处理器安全和可重构硬件安全

慕德俊：男，教授，研究方向为网络信息安全、密码学和控制理论及应用等

胡伟：男，教授，研究方向为集成电路硬件安全、形式化安全验证、安全漏洞检测和密码学等

通讯作者:
胡伟　weihu@nwpu.edu.cn

中图分类号: TN407; TP309.1
计量
- 文章访问数: 18
- HTML全文浏览量: 12
- PDF下载量: 1
- 被引次数: 0
出版历程
- 收稿日期: 2025-05-06
- 修回日期: 2025-09-13
- 网络出版日期: 2025-09-18

Verification of Privilege Correctness and Automated Exploitation of Privilege Escalation Vulnerabilities in RISC-V Processors

College of Cyberspace Security, Northwestern Polytechnical University, Xi’an 710072, China

Funds: The National Natural Science Foundation of China (U23B2041, 62272389)

摘要

摘要: 处理器安全是近年来的热点前沿研究领域，各种处理器安全漏洞层出不穷。然而，现有处理器漏洞挖掘主要采取各类测试手段，存在自动化程度低、漏洞挖掘效率和完备性不高等局限性，特别是在权限正确性验证与漏洞挖掘方面。该文提出一种基于符号执行和属性验证的RISC-V处理器权限正确性验证与提权漏洞自动挖掘方法。首先，对于特权级访问控制机制，形式化地定义了访问保护(AP)、异常处理(EH)、指令解码(ID)、寄存器安全(RS)和特权绕过(PB)5类特权提升漏洞类型；该文还提出了属性驱动的状态空间归约、路径引导等策略，有效提升了安全验证效率；设计了一个权限正确性验证与提权漏洞挖掘自动化框架，实现了对处理器设计的软硬件联合安全验证、特权提升漏洞检测和概念验证(PoC)自动生成。在OR1200, Ibex, PicoRV32和PULPino 4款开源处理器上的实验结果表明本文所提方法能够实现权限正确性属性的形式化验证并有效捕捉提权类漏洞，验证效率平均提升66.1%，同时能够自动生成高质量PoC。该文所提方法能够显著提升RISC-V处理器特权提升漏洞的自动化挖掘能力，为处理器设计安全评估提供一种新思路和技术手段。
- RISC-V处理器 /
- 特权提升漏洞 /
- 符号执行 /
- 形式化验证 /
- 安全属性
Abstract: Objective The rapid expansion of RISC-V processors across domains ranging from embedded systems to high-performance computing has heightened the urgency of rigorous security verification. Privilege escalation vulnerabilities represent one of the most severe threats, enabling attackers to bypass hardware-enforced boundaries and obtain unauthorized access to privileged system resources. Such vulnerabilities can compromise the entire security foundation of computing systems, rendering even the most advanced software-level defenses ineffective. Existing hardware verification methods depend heavily on manual testing and traditional simulation, which suffer from limited automation, insufficient test coverage, high verification costs, and poor scalability for complex modern processor architectures. To address these challenges, this study develops an automated verification framework specifically designed to detect privilege escalation vulnerabilities in RISC-V processor implementations. Methods This study presents a systematic framework for automated verification of privilege escalation vulnerabilities in RISC-V processors, combining formal methods with symbolic execution. The approach begins with a detailed analysis of the RISC-V privilege architecture specification, which provides the basis for formally defining five categories of privilege escalation vulnerabilities: Access Protection (AP) violations caused by improper privilege-level configuration; Exception Handling (EH) vulnerabilities arising in exception processing; Instruction Decoding (ID) issues that permit unauthorized execution of privileged instructions; Register Security (RS) violations enabling unauthorized access to privileged registers; and Privilege Bypass (PB) vulnerabilities that circumvent privilege-checking mechanisms. Each category is rigorously formalized using mathematical models and temporal logic specifications to enable precise automated detection. The verification framework employs symbolic execution as the core analysis engine, enhanced with hardware-specific optimizations tailored to processor verification. To address the state explosion problem, a property-driven state-space reduction algorithm prioritizes execution paths most likely to violate security properties. In addition, intelligent path-guidance techniques incorporate domain knowledge of suspicious privilege operation patterns to steer symbolic execution toward potentially vulnerable regions of code. The verification pipeline begins by converting Register Transfer Level (RTL) hardware descriptions into LLVM intermediate representation using Verilator, followed by symbolic analysis with a customized version of the KLEE symbolic execution engine. A key innovation of this framework is the integration of automated Proof-of-Concept (PoC) generation within the verification workflow. When a potential vulnerability is identified, the system automatically generates minimal test cases that demonstrate exploitability. The PoC process applies constraint-simplification algorithms to extract essential triggering conditions from symbolic execution paths, then instantiates assembly code templates to produce executable test programs. These PoCs are designed to run in minimal simulation environments, thereby enabling efficient validation of identified vulnerabilities. Results and Discussions The proposed methodology is evaluated on four representative open-source RISC-V processors: OR1200, Ibex, PicoRV32, and PULPino. These implementations represent diverse design philosophies within the RISC-V ecosystem and together form a robust evaluation testbed. Five categories of privilege escalation vulnerabilities are detected across the tested processors, including previously undocumented flaws. Cross-processor vulnerability patterns are also observed, with certain weaknesses recurring in multiple implementations, suggesting systematic issues in prevailing design practices. Performance evaluation indicates substantial efficiency gains over existing verification approaches. On average, verification time is reduced by 66.1% compared with traditional techniques, with the most significant improvements observed in detecting register-access vulnerabilities. When compared with Symbiotic EDA and the standard KLEE framework, the optimized approach consistently achieves superior performance across all vulnerability categories. These gains are attributed to the property-guided state-space reduction and intelligent path-search strategies, which concentrate computational resources on execution paths most likely to violate security properties. The integrated PoC generation system produces executable exploits for all identified vulnerabilities. The generated assembly code is validated through waveform analysis in ModelSim simulation, confirming reproducibility and effectiveness. Designed as minimal test cases, the PoCs demonstrate the triggering conditions of vulnerabilities while maintaining readability and value for security researchers. Conclusions This study advances automated security verification for RISC-V processors by introducing a comprehensive framework that integrates formal modeling, optimized symbolic execution, and automated exploit generation. Hardware-specific optimizations effectively address computational challenges such as state explosion, a major limitation to the scalability of formal verification. The framework enables systematic detection of privilege escalation vulnerabilities and the generation of concrete exploits, substantially improving upon existing verification methodologies. The practical significance extends beyond academic research, providing processor designers, security researchers, and verification engineers with a tool that reduces manual verification effort while enhancing coverage and reliability. By embedding automated PoC generation, the approach not only identifies vulnerabilities but also demonstrates their exploitability in a reproducible manner. Future work will expand support to complex processor features, including multi-issue execution, out-of-order processing, and advanced microarchitectural optimizations, while also exploring hybrid verification paradigms that combine formal methods with targeted testing.
- RISC-V processor /
- Privilege escalation vulnerabilities /
- Symbolic execution /
- Formal verification /
- Security property

HTML全文

图 1 特权提升漏洞验证框架

下载: 全尺寸图片幻灯片

图 2 PoC自动生成框架结构图

下载: 全尺寸图片幻灯片

图 3 特殊寄存器访问漏洞PoC重放

下载: 全尺寸图片幻灯片

图 4 调试电路利用漏洞PoC重放

下载: 全尺寸图片幻灯片

1 合法特权提升路径

(1) s0 = (0, 0x1000, {···}, {SR=0x8000}, mem, 0) // 用户模式
(2) s1 = (0, 0x1004, {···}, {SR=0x8000}, mem, TRAP) // 执行　l.trap
(3) s2 = (1, 0x200, {···}, {SR=0x8001}, mem, TRAP) // 跳转到异常处理程序，切换到监督模式

下载: 导出CSV

2 寄存器信息泄露路径

(1) s0 = (0, 0x1000, {r3=0x0, ···}, {SR=0x8000, ···}, mem, 0)
// 用户模式正常执行
(2) s1 = (0, 0x1004, {r3=0x0, ···}, {SR=0x8000, ···}, mem, 0) 　// 执行l.mfspr指令尝试读取PPC寄存器
// l.mfspr r3, r0, SPR_PPC (PPC寄存器存储上一条指令地　　址，通常只在监督模式可访问)
(3) s2 = (0, 0x1008, {r3=0x2FFC, ···}, {SR=0x8000, ···}, mem, 　　0) // 由于权限检查缺失，用户成功读取监督模式指令地址
(4) s3 = (0, 0x100C, {r3=0x2FFC, r4=0x1, ···}, {SR=0x8000, 　　···}, mem, 0) // 攻击者将读取的地址与已知操作系统代码比　　对// l.addi r4, r0, 1
(5) s4 = (0, 0x1010, {r3=0x2FFC, r4=0x1, ···}, {SR=0x8000, 　　···}, mem, 0) // 执行系统调用 // l.sys
(6) s5 = (1, 0x200, {r3=0x2FFC, r4=0x1, ···}, {SR=0x8001, 　　···}, mem, SYSCALL) // 进入系统调用，但攻击者已获知关　　键地址信息

下载: 导出CSV

表 1 RISC-V特权提升漏洞分类及属性

漏洞类型	违反属性	安全影响	典型场景	操作实例
特权级配置不当 (Allow Privilege, AP)	低特权态不能访问高特权态资源	允许低特权程序获取高特权	寄存器权限检查缺失	用户模式可直接修改SR 寄存器中的SM位
异常处理不安全 (Exception Handling, EH)	异常处理程序不能获得比引发异常指令更高的特权级	异常处理可被利用提升特权	异常向量表可被用户修改	用户模式可修改EPCR0寄存器控制异常处理入口
指令非法使用 (Instruction Deference, ID)	特权指令只能在适当特权级下使用	用户模式执行特权指令	指令解码缺少相关权限检查	用户模式下可执行l.rfe指令
寄存器信息泄露 (Register Security, RS)	低特权态不能读取高特权态CSR敏感域	敏感特权信息泄露	CSR寄存器读取无正确权限检查	用户模式可读取SPR_PPC寄存器获取监督模式指令信息
特权级检查绕过 (Privilege Bypass, PB)	漏洞允许绕过特权检查访问特权功能	绕过安全机制访问受限资源	缓存一致性问题导致权限检查被绕过	TLB缓存未正确失效导致内存保护被绕过

下载: 导出CSV

3 AP属性(特权级配置不当)

AP := ∀i ∈ [0, n–1] : priviledge_check(si, si+1)
priviledge_check(s1, s2) :=
(s2.csr[mstatus].mpp = s1.priviledge) ∧ (s2.priviledge > 　s1.priviledge)
→ 　(legal_change(s1.priviledge, s2.priviledge) ∨ 　csr_access_legal(s2.pc, s2.priviledge))
legal_change(p1, p2) := (p1 = U ∧ p2 = S) ∨ (p1 = S ∧ p2 　= M) ∨ (p1 = U ∧ p2 = M)
csr_access_legal(pc,p) := ∀r ∈ CSR : load(r) ∨ store(r) → 　(r.priviledge ≤ p)

下载: 导出CSV

4 EH属性(异常处理不安全)

EH := ∀ i ∈ [0, n–1] : exception_handling_check(si, si+1)
exception_handling_check(s1, s2) := (s1.exception ≠ 0) →
(s2.pc ∈ SecureExceptionVectors) ∧ (∀reg ∈ 　ExceptionControlRegs : (s1.privilege < reg.min_privilege) →
(s1.csr[reg] = s2.csr[reg]))

下载: 导出CSV

5 ID属性(指令非法使用)

ID := ∀ i ∈ [0, n–1] : instruction_privilege_check(si, si+1)
instruction_privilege_check(s1, s2) := (∀instr ∈ 　PrivilegedInstructions :(s1.instruction = instr) →
(s1.privilege ≥ instr.min_privilege))

下载: 导出CSV

6 RS属性(寄存器信息泄露)

RS := ∀ i ∈ [0, n–1] : register_security(si, si+1)
register_security(s1, s2) := (∀reg ∈ CSRs : (s1.instruction = 　read(reg) ∧ s1.privilege < reg.min_privilege) →
(s2.exception ≠ 0 ∨ s2.gpr[rd] = 0))

下载: 导出CSV

7 PB属性(特权级检查绕过)

PB := ∀ i ∈ [0, n–1] : privilege_bypass_check(si, si+1)
privilege_bypass_check(s1, s2) := (s1.privilege < s2.privilege) 　→
(s1.exception ≠ 0) ∧(s1.privilege = 0) →
((s1.mem_access = 1) → (address_translation(s1.mem_addr) ∈ UserAccessibleMemory))

下载: 导出CSV

8 基于属性的状态空间归约

输入：当前状态curState，特权安全属性集合privAttrs
输出：排序后的下一步待探索状态列表nextStates
1: function PRIORITIZE_STATES(curState, privAttrs)
2: 　allNextStates ← COMPUTE_NEXT_STATES(curState) 　// 计算当前状态的所有可能后继状态
3: 　highPriorityStates ← [] // 初始化高低优先级状态队列
4: 　lowPriorityStates ← []
5: 　for each state in allNextStates do // 遍历所有后继状态，　　　评估其违反特权属性的可能性
6: 　if MAY_VIOLATE(state, privAttrs)then // 检查状态是　　　否可能违反任何特权安全属性
7: 　　　highPriorityStates.append(state) // 可能违反特权属　　　　　性的状态获得高优先级
8: 　　else
9: 　　　lowPriorityStates.append(state) // 其他状态获得低优　　　　　先级
10: 　 end if
11: end for
12: 　 return highPriorityStates + lowPriorityStates // 先返回　　　　高优先级状态，再返回低优先级状态
13: end function

下载: 导出CSV

表 2 面向特权安全的可疑操作规则(节选)

编号	规则描述
R1	低特权态对高特权态寄存器的写操作
R2	用户态代码中出现监管指令(Supervisor Instructions)
R3	机器态代码执行后特权级发生降低(M→S/U)
R4	特权态降低后未清除敏感信息
R5	异常发生后未跳转到合法向量
R6	低特权态访问调试模块
R7	特权内存的非授权访问
R8	TLB操作期间的特权检查异常
···	······

下载: 导出CSV

9 汇编程序模板

.section .text, "ax"
.org 0x100 # default address
.global start
start:
# 第1部分：初始化设置
# 设置处理器初始状态，初始化关键寄存器和配置信号
# 第2部分：触发序列
# 添加尝试触发漏洞的指令序列
# 第3部分：验证检查
# 读取相关寄存器或信号并与预期值比较
# 第4部分：错误处理和报告
# 处理违反情况的检测结果
# 程序结束
l.nop 0x0001

下载: 导出CSV

10 PoC模板实例化

输入：漏洞描述(vul_desc)，触发指令(trigger_instr)，关键寄　存器(key_regs)
输出：实例化的汇编程序(asm_program)
(1) 根据vul_desc选择合适的模板
(2) 填充初始化部分:
- 设置处理器为需要的特权模式(通常为用户模式)
- 初始化关键寄存器的值
(3) 插入trigger_instr作为触发序列的核心
- 对于l.mfspr等指令，填入正确的寄存器地址和目标
(4) 添加程序结束部分

下载: 导出CSV

11 OR1200 SPR寄存器访问

; SPR寄存器访问需要复杂的地址译码
define i32 @spr_read(i32 %spr_addr) {
entry:
%group = lshr i32 %spr_addr, 11 ; 提取组号
%index = and i32 %spr_addr, 2047 ; 提取索引
switch i32 %group, label %default [
i32 0, label %group0_sys ; 系统寄存器组
i32 1, label %group1_dmmu ; 数据MMU组
i32 2, label %group2_immu ··· ] ; 指令MMU组
group0_sys:
switch i32 %index, label %invalid [
i32 17, label %read_sr ; SR寄存器
i32 18, label %read_epc ··· ]} ; 异常PC

下载: 导出CSV

12 Ibex标准CSR访问

; 标准RISC-V CSR访问，直接12位寻址
define i32 @csr_read(i32 %csr_addr) {
entry:
%is_mstatus = icmp eq i32 %csr_addr, 0x300
%is_mie = icmp eq i32 %csr_addr, 0x304
%is_mtvec = icmp eq i32 %csr_addr, 0x305
; 使用select指令选择对应寄存器
%result = select i1 %is_mstatus, i32 %mstatus_val,
select i1 %is_mie, i32 %mie_val, ···
ret i32 %result}

下载: 导出CSV

13 PicoRV32最小CSR集合

; 仅支持必要的性能计数器
define i32 @csr_read_simple(i32 %csr_addr) {
entry:
%is_cycle = icmp eq i32 %csr_addr, 0xC00
%is_instret = icmp eq i32 %csr_addr, 0xC02
%result = select i1 %is_cycle, i32 %cycle_cnt,
select i1 %is_instret, i32 %inst_cnt, i32 0
ret i32 %result}

下载: 导出CSV

14 PULPino包含PULP特定寄存器

; 扩展的CSR实现，包含硬件循环
define i32 @csr_read_pulp(i32 %csr_addr) {
entry:
; 检查是否为PULP扩展CSR(0x780-0x7FF)
%is_pulp = icmp uge i32 %csr_addr, 0x780
br i1 %is_pulp, label %pulp_csr, label %standard_csr
pulp_csr:
; 硬件循环寄存器：lpstart, lpend, lpcount
%pulp_idx = sub i32 %csr_addr, 0x780
switch i32 %pulp_idx, label %default [
i32 0, label %read_lpstart
i32 1, label %read_lpend
i32 2, label %read_lpcount ··· ]}

下载: 导出CSV

表 3 已知特权相关漏洞列表

漏洞 ID	处理器	漏洞类型	违反属性	漏洞描述
V1	OR1200	越权访问调试寄存器	RS	用户模式可访问调试寄存器(DSR)，违反了“低特权模式不应直接访问高特权寄存器”的属性。
V2	OR1200	越权访问特殊寄存器	RS	用户模式可读取特殊寄存器(SPR)，违反了“系统关键寄存器必须受特权保护”的属性。
V3	Ibex	特权状态保持	PB	mret指令保持在机器模式而非切换到用户模式，违反了“特权转换指令必须正确改变特权级别”的属性。
V4	Ibex	PMP配置缺陷	AP	当mseccfg.MML设置时错误允许特定写入，违反了“内存保护配置必须被正确执行”的属性。
V5	PicoRV32	CSR访问异常缺失	EH/ID	访问不存在的CSR不抛出异常，违反了"非法操作必须触发正确的异常处理"的属性。

下载: 导出CSV

表 4 漏洞存在情况与验证所需时间(min)

漏洞ID	OR1200	Ibex	PicoRV32	PULPino	Symbiotic EDA	KLEE(原版)	本文框架
V1	原生√	×	×	×	33	>60	12
V2	原生√	×	×	×	>60	>60	13
V3	×	原生√	×	×	42	>60	17
V4	×	原生√	×	×	>60	>60	12
V5	√	√	原生√	×	38	>60	24

下载: 导出CSV

15 特殊寄存器访问漏洞PoC

.section .text, "ax"
.org 0x100 # default address
.global _start
_start:
l.andi r0, r0, 0
l.extwz r1, r0
l.extwz r2, r0
l.extwz r3, r0 # 清除寄存器r0～r3
l.mfspr r1, r0, 0x0011 # 读取SR寄存器，SR[0] = 1
l.movhi r2, 0xffff
l.ori r2, r2, 0xfffe
l.and r3, r2, r1
l.mtspr r0, r3, 0x0011 # 设置为用户模式 SR[0] = 0
l.ori r4, r0, 0x0012 # PPC寄存器地址 = 0x12
l.mfspr r5, r4, r0 # 尝试读取PPC寄存器
l.nop 0x0001

下载: 导出CSV

16 调试电路利用漏洞PoC

.section .text, "ax"
.org 0x100 # default address
.global _start
_start:
l.andi r0, r0, 0
l.extwz r1, r0
l.extwz r2, r0
l.extwz r3, r0 # 清除寄存器r0～r3
l.mfspr r1, r0, 0x0011 # 读取SR寄存器，SR[0] = 1
l.movhi r2, 0xffff
l.ori r2, r2, 0xfffe
l.and r3, r2, r1
l.mtspr r0, r3, 0x0011 # 设置为用户模式 SR[0] = 0
l.extwz r30, r0
l.ori r30, r0, 0x0014 # DSR寄存器地址 = 0x14
l.mfspr r31, r30, r0 # 尝试读取DSR寄存器
l.nop 0x0001

下载: 导出CSV

参考文献(29)

[1]	MENTENS N. Hardware security in the era of emerging device and system technologies[J]. IEEE Security & Privacy, 2024, 22(3): 4–6. doi: 10.1109/MSEC.2024.3379768.
[2]	RANDAL A. This is how you lose the transient execution war[EB/OL]. https://arxiv.org/abs/2309.03376, 2023.
[3]	YAMAUCHI T, AKAO Y, YOSHITANI R, et al. Additional kernel observer: Privilege escalation attack prevention mechanism focusing on system call privilege changes[J]. International Journal of Information Security, 2021, 20(4): 461–473. doi: 10.1007/s10207-020-00514-7.
[4]	CUI Enfang, LI Tianzheng, and WEI Qian. RISC-V instruction set architecture extensions: A survey[J]. IEEE Access, 2023, 11: 24696–24711. doi: 10.1109/ACCESS.2023.3246491.
[5]	HARRIS A, VERMA T, WEI Shijia, et al. Morpheus II: A RISC-V security extension for protecting vulnerable software and hardware[C]. 2021 IEEE International Symposium on Hardware Oriented Security and Trust (HOST), Tysons Corner, USA, 2021: 226–238. doi: 10.1109/HOST49136.2021.9702275.
[6]	ERATA F, DENG Shuwen, ZAGHLOUL F, et al. Survey of approaches and techniques for security verification of computer systems[J]. ACM Journal on Emerging Technologies in Computing Systems, 2023, 19(1): 6. doi: 10.1145/3564785.
[7]	RYAN K and STURTON C. Sylvia: Countering the path explosion problem in the symbolic execution of hardware designs[C]. 2023 Formal Methods in Computer-Aided Design (FMCAD), Ames, USA, 2023: 110–121. doi: 10.34727/2023/isbn.978-3-85448-060-0_19.
[8]	包云岗, 孙凝晖. 开源芯片生态技术体系构建面临的机遇与挑战[J]. 中国科学院院刊, 2022, 37(1): 24–29. doi: 10.16418/j.issn.1000-3045.20211117003. BAO Yungang and SUN Ninghui. Opportunities and challenges of building CPU ecosystem with open-source mode[J]. Bulletin of Chinese Academy of Sciences, 2022, 37(1): 24–29. doi: 10.16418/j.issn.1000-3045.20211117003.
[9]	SHEN Qintao, MENG Guozhu, and CHEN Kai. Revealing the exploitability of heap overflow through PoC analysis[J]. Cybersecurity, 2024, 7(1): 47. doi: 10.1186/s42400-024-00244-6.
[10]	BROOKES S and TAYLOR S. Containing a confused deputy on x86: A survey of privilege escalation mitigation techniques[J]. (IJACSA) International Journal of Advanced Computer Science and Applications, 2016, 7(4): 476–484. doi: 10.14569/IJACSA.2016.070463.
[11]	ERMOLOV M, SKLYAROV D, and GORYACHY M. Undocumented x86 instructions to control the CPU at the microarchitecture level in modern Intel processors[J]. Journal of Computer Virology and Hacking Techniques, 2023, 19(3): 351–365. doi: 10.1007/s11416-022-00438-x.
[12]	MEZGER B W, SANTOS D A, DILILLO L, et al. A survey of the RISC-V architecture software support[J]. IEEE Access, 2022, 10: 51394–51411. doi: 10.1109/ACCESS.2022.3174125.
[13]	EASDON C. Undocumented CPU behaviour on x86 and RISC-V microarchitectures: A security perspective[D]. [Master dissertation], University of Bristol, 2019.
[14]	SHEN Lixiang, MU Dejun, CAO Guo, et al. Symbolic execution based test-patterns generation algorithm for hardware Trojan detection[J]. Computers & Security, 2018, 78: 267–280. doi: 10.1016/j.cose.2018.07.006.
[15]	DUDINA I A and BELEVANTSEV A A. Using static symbolic execution to detect buffer overflows[J]. Programming and Computer Software, 2017, 43(5): 277–288. doi: 10.1134/S0361768817050024.
[16]	BROTZMAN R, LIU Shen, ZHANG Danfeng, et al. CaSym: Cache aware symbolic execution for side channel detection and mitigation[C]. 2019 IEEE Symposium on Security and Privacy (SP), San Francisco, USA, 2019: 505–521. doi: 10.1109/SP.2019.00022.
[17]	FOWZE F, CHOUDHURY M, and FORTE D. EISec: Exhaustive information flow security of hardware intellectual property utilizing symbolic execution[C]. 2022 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), Singapore, Singapore, 2022: 1–6. doi: 10.1109/AsianHOST56390.2022.10022071.
[18]	ZHANG Rui and STURTON C. A recursive strategy for symbolic execution to find exploits in hardware designs[C]. The 2018 ACM SIGPLAN International Workshop on Formal Methods and Security, Philadelphia, USA, 2018: 1–9. doi: 10.1145/3219763.3219764.
[19]	BRUNS N, HERDT V, and DRECHSLER R. Processor verification using symbolic execution: A RISC-V case-study[C]. 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), Antwerp, Belgium, 2023: 1–6. doi: 10.23919/DATE56975.2023.10137202.
[20]	FAROOQUI N, SCHWAN K, and YALAMANCHILI S. Efficient instrumentation of GPGPU applications using information flow analysis and symbolic execution[C]. Workshop on General Purpose Processing Using GPUs, Salt Lake City, USA, 2014: 19–27. doi: 10.1145/2588768.257678.
[21]	BUCUR S, URECHE V, ZAMFIR C, et al. Parallel symbolic execution for automated real-world software testing[C]. The 6th Conference on Computer Systems, Salzburg, Austria, 2011: 183–198. doi: 10.1145/1966445.1966463.
[22]	CADAR C, GANESH V, PAWLOWSKI P M, et al. EXE: Automatically generating inputs of death[J]. ACM Transactions on Information and System Security (TISSEC), 2008, 12(2): 10. doi: 10.1145/1455518.1455522.
[23]	KURIAN E, BRIOLA D, BRAIONE P, et al. Automatically generating test cases for safety-critical software via symbolic execution[J]. Journal of Systems and Software, 2023, 199: 111629. doi: 10.1016/j.jss.2023.111629.
[24]	YOU Wei, ZONG Peiyuan, CHEN Kai, et al. SemFuzz: Semantics-based automatic generation of proof-of-concept exploits[C]. The 2017 ACM SIGSAC Conference on Computer and Communications Security, Dallas, USA, 2017: 2139–2154. doi: 10.1145/3133956.3134085.
[25]	ZHANG Rui, DEUTSCHBEIN C, HUANG Peng, et al. End-to-end automated exploit generation for validating the security of processor designs[C]. 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), Fukuoka, Japan, 2018: 815–827. doi: 10.1109/MICRO.2018.00071.
[26]	WATERMAN A, LEE Y, AVIZIENIS R, et al. The RISC-V instruction set manual volume II: Privileged architecture version 1.7[R]. UCB/EECS-2015-49, 2015.
[27]	JAYASENA A and MISHRA P. Directed test generation for hardware validation: A survey[J]. ACM Computing Surveys, 2024, 56(5): 132. doi: 10.1145/3638046.
[28]	BOURGEAT T, CLESTER I, ERBSEN A, et al. A multipurpose formal RISC-V specification[EB/OL]. https://arxiv.org/abs/2104.00762v1, 2021.
[29]	CADAR C, DUNBAR D, and ENGLER D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs[C]. The 8th USENIX Conference on Operating Systems Design and Implementation, San Diego, USA, 2008: 209–224.