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

The RISC-V SBI (Supervisor Binary Interface) standard defines the interface specification between the RISC-V bottom-level hardware and the operating system. Compared with mainstream architectures such as x86 and ARM, RISC-V SBI is more compliant and more reliable. However, the existing SBI firmware implementations have the security vulnerabilities that have emerged, such as the trusted execution environment verification problem in startup process. To this end, this paper proposes a formal verification framework based on theorem proof to develop a fully formally verified SBI firmware-SeSBI. By integrating Dafny with Isabelle/HOL, at both the abstract and executable levels, this study formally specifies and hierarchically verifies the SBI firmware’s state transitions and functional characteristics across privilege modes. Since the SBI firmware program interacts with the hardware, in order to optimize the verification efficiency, this paper adopts a hardware simulation strategy in the formal description, which significantly reduces the computational overhead of the verification process. Finally, the security properties and functional correctness of the SeSBI firmware are successfully verified at different layers. The results show that SeSBI implements some SBI standard interfaces with more concise code and has high reliability. This paper provides a formally verified and highly trusted SBI firmware implementation for the RISC-V ecosystem. In the future, the verification scope will be expanded to cover more advanced properties, and the formal development and verification of the SeSBI firmware will be further improved.