Formalizing the RISC-V Hypervisor Extension in Sail

Formal ISA specifications improve security of software systems by reducing the risk of incorrect developer assumptions and by enabling testing and verification of hardware and (security-critical) software. RISC-V International offers an official formal specification of the RISC-V ISA, intended to be unambiguous, executable, easy to understand and well-suited for formal analysis. Unfortunately, it does not yet implement all ratified RISC-V standard extensions. This work presents an implementation of the missing, security-critical hypervisor extension into the official model, implemented in the Sail programming language. The extended model has been validated in various ways, including regression-checked using bundled tests. The hypervisor extension has been verified with an accompanying test suite developed together with the model and also by two third-party test suites. Finally, the extracted emulator is able to boot Linux on top of a type-1 hypervisor. The extensions to the Sail model are in the process of being merged into the official specification. The formal model and the test suite support the testing and verification of secure hardware and software that implements or uses the hypervisor extension. Additionally, we offer some thoughts and observations about the process of formally specifying this extension and the engineering process of formal ISA specifications for RISC-V and elsewhere.