heRVé: towards a formally verified RISC-V processor with security mechanisms

From bibtex.

Abstract

Ultimately, the safety of systems is contingent on the security of the hardware platforms they operate on. To achieve the highest degree of confidence in the hardware's security, specifically processors, we advocate the use of formal methods. In this paper, we build upon the work by Baty et al., which introduces a RISC-V processor enhanced with a shadow stack. This processor is designed in Kôika, a Hardware Description Language embedded into the Rocq proof assistant, and includes formal security proofs for the implemented shadow stack. We enhance this processor to incorporate support for traps, various privilege levels, and physical memory protection (PMP). Additionally, we automate the proofs of the shadow stack by relying on a SMT solver, improving both scalability and maintenance. Our processor is sufficiently rich to run Zephyr, a small real-time operating system for embedded processors.