Formal Specification and Verification of Security Mechanisms for RISC-V Processors

From bibtex.

Abstract

In this thesis, we consider the verification of security mechanisms for processors described at the register-transfer level (RTL). We propose an approach based on interactive theorem provers, generalist tools used for producing high-assurance proofs. This approach has two key benefits over the current state of formal methods in the industry. First, interactive theorem provers come with a very small trusted computing base (TCB). For this reason, the French certification authorities for Common Criteria for Information Technology Security Evaluation recognize interactive theorem provers for the highest Evaluation Assurance Level. Second, whereas formal verification in the industry is based around a set of distinct tools with a focused scope, interactive theorem provers can express and verify very general properties in a single, unified environment. Our reliance on interactive theorem provers comes with distinct challenges, such as the fact that all the domain-specific knowledge about hardware needs to formalized before any verification work can proceed. Furthermore, they are arcane tools that come with a prohibitive learning curve and a number of performance issues. Our contributions are twofold. 1/ We design a verification framework around Kôika, a hardware description language with a formal semantics. We use this framework to verify the implementation of a shadow stack added to a RISC-V processor. We explore the integration of SMT solvers into this framework as a means of automating the process. 2/ We port FIRRTL, a hardware description language with use in the industry, into the Coq proof assistant.