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

TANG Shibo; ZHU Jiacheng; MU Dejun; HU Wei

doi:10.11999/JEIT250362

Article Contents

Article Navigation > Journal of Electronics & Information Technology > 2025 >

TANG Shibo, ZHU Jiacheng, MU Dejun, HU Wei. Verification of Privilege Correctness and Automated Exploitation of Privilege Escalation Vulnerabilities in RISC-V Processors[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT250362

Citation:

TANG Shibo, ZHU Jiacheng, MU Dejun, HU Wei. Verification of Privilege Correctness and Automated Exploitation of Privilege Escalation Vulnerabilities in RISC-V Processors[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT250362

Citation:

TANG Shibo, ZHU Jiacheng, MU Dejun, HU Wei. Verification of Privilege Correctness and Automated Exploitation of Privilege Escalation Vulnerabilities in RISC-V Processors[J]. Journal of Electronics & Information Technology. doi: 10.11999/JEIT250362

PDF( 1877 KB)

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

doi: 10.11999/JEIT250362 cstr: 32379.14.JEIT250362

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

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

Received Date: 2025-05-06
Rev Recd Date: 2025-09-13

Available Online: 2025-09-18

Abstract

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

FullText(HTML)

References(29)

References

[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.