Formal Verification for Safe Startup Process of the RISC-V SBI Firmware

The RISC-V SBI (supervisor binary interface) specification establishes a standardized interface between RISC-V hardware architectures and operating systems. In comparison to traditional firmware implementations for x86 and ARM platforms, the RISC-V SBI firmware demonstrates superior compliance with architectural standards and offers enhanced reliability. However, the current SBI implementations still exhibit significant security concerns, particularly regarding unverified boot process correctness and vulnerabilities in PMP (physical memory protection) mechanisms for physical address access control. To this end, a closed-loop formal verification framework driven by theorem proving is proposed, developing the first formally verified SBI firmware—SeSBI. By integrating Dafny and Isabelle/HOL, a layered strategy is employed to formally verify specification properties across startup process. And to improve verification efficiency, a RISC-V hardware simulation strategy is introduced, unifying the modeling of firmware-hardware interactions, thereby significantly reducing verification overhead. Finally, the functional correctness of SeSBI in the boot process is successfully verified. The results demonstrate that SeSBI implements the SBI standard boot interface with more concise code and high reliability, providing the first formally verified, trusted SBI firmware implementation for the RISC-V ecosystem. Future work will expand verification coverage to more advanced properties and optimize tooling for greater efficiency.