Modular and automatic formal verification of a RISC-V processor with security mechanisms
Abstract
The security of computer systems eventually relies on the security of the underlying hardware and on the security mechanisms that it offers. We extend a simple RISC-V processor written in the Kôika Hardware Description Language (HDL) with security mechanisms, and prove that these mechanisms are correct. We do so by compiling Kôika circuits into a representation well-suited for automated theorem provers. We strive to make our proofs modular, i.e., function by function or rule by rule.
Fields of Study & Subjects
Security and Verification in Computing
Logic
programming
and type systems
Formal Methods in Verification
Publication details
- Journal / source
- HAL (Le Centre pour la Communication Scientifique Directe)
- Publication date
- 11 January 2026
- Language
- EN
- Document type
- Preprint