Verifying RISC-V Privilege Transition Integrity Through Symbolic Execution

Ensuring privilege transition integrity during execution context switch is crucial for protecting the processor from unauthorized access and malicious actions. However, existing methods fall short in covering potential attack paths and vectors in a complete manner. In this work, we propose a method for formal verification of privilege correctness targeting privilege escalation attacks, where the program processes on non-privileged mode may access the sensitive information stored in Special purpose registers (SPRs). We specify assertion property and utilize the Klee symbolic execution engine to formally check the consistency in privilege when accessing contents in critical registers. The formal solver performs state space exploration through heuristic search to identify the possible integrity violation test cases that can trigger an illegal privilege escalation, which further allows creating a minimal simulation system consisting of the CPU and Quick Memory (QMEM) modules to replay the privilege violation process. Experimental results have demonstrated that our method can systematically verify the privilege validity to protect the system from privilege escalation attacks on a RISC-V processor.