Two PhD students supervised by members of the team will defend soon:
Matthieu Baty
Formal Specification and Verification of Security Mechanisms for RISC-V Processors
Supervised by Guillaume Hiet, Alix Trieu (ANSSI) and Pierre Wilke.
Defense will be December 10th, 1pm, at CentraleSupélec, room 213.
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.
Jean-Loup Hatchikian-Houdot
Constant time security through cooperation between software and embedded hardware
Supervised by Guillaume Hiet, Frédéric Besson (Epicure, Inria) and Pierre Wilke.
Defense will be December 16th, 9am, at Irisa, room Petri-Turing. Also remote on Webex.
Abstract:
Constant-time programming is used to produce programs immune to timing attacks. However, this discipline imposes several constraints on the software developer, making implementation complex and sometimes slow. We propose a new protection mechanism specialized for embedded systems and implemented in hardware but usable from software. With this protection, the constraints of constant-time programming can be relaxed, making constant-time secure programs easier to produce and faster in several cases. This protection works by locking chunks of the memory in the cache, such that memory accesses toward these chunks are protected against timing attacks. We reuse proof techniques used to formally verify the CompCert compiler. In our case, we use it to certify that no cache attacks could expose our protected memory accesses. We show the performance gain allowed by our new protection on several cryptographic algorithms, and we propose a new fast sorting method that is constant-time with this cache-locking mechanism.
