Spécification et vérification formelle de mécanismes de sécurité pour processeurs RISC-V: Version non-finale
Matthieu Baty · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
In this thesis, we consider the problem of hardware verification, with a focus on security properties of security mechanims of RISC-V processors. We target proofs at the microarchitectural level, reasoning directly on the hardware's definition. Our proposed approach is based on proof assistants, versatile tools used for producing highconfidence proofs. Their flexibility allows us to express and verify arbitrary properties on designs. This differs from the more rigid approach to formal verification commonly used in the industry, which relies on specialized tools. The flexibility of proof assistants comes at a cost. First, they are not specialized to the problem of hardware verificationall the domain-specific knowledge needs to be formalized before any verification work can proceed. Furthermore, they are arcane tools with a prohibitive learning curve. We consider both of these concerns in this thesis. The first concern we outlined was that proof assistants must be taught about hardware design. Before anything else, the required notions must be defined within the system -critically, a formal semantics of a hardware description language must be given. In this thesis, we work with an academic language built from the ground up with a formal semantics (Kôika) and a more industrial language whose semantics we had to formalize ourselves (FIRRTL). The second concern was related to the complexity of proof assistants. Our answer consists of frameworks built around the semantics of hardware description languages. Both manual and automatic (chiefly SMT-based) options are explored. In principle, such frameworks can cover the same ground as formal tools used in the industry and some more. We illustrate this methodology by formally verifying security properties of a RISC-V processor within the Coq proof assistant.