Design and Formal Verification of Hardware/software Security Mechanisms

**Design and Formal Verification of Hardware/Software Security Mechanisms**:

- Réf **ABG-128442**
- Sujet de Thèse
- 10/02/2025
- Contrat doctoral
- CentraleSupelec
- Lieu de travail- Rennes - Bretagne - France
- Intitulé du sujet- Design and Formal Verification of Hardware/Software Security Mechanisms
- Champs scientifiques- Informatique
- Mots clés- cyber-security, embedded systems, formal methods, computer architecture, fault-injection

**Description du sujet**:
**Context.**Embedded systems are increasingly targeted by attackers, facing not only traditional software attacks—such as those exploiting memory safety vulnerabilities like buffer overflows—but also hardware attacks. Among the last ones, fault-injection attacks exploit hardware perturbations to move a processor into unexpected states or execution paths, potentially exposing secrets or escalating privileges. Such attacks represent an effective threat to embedded systems and leverage faults inside the processor microarchitecture, resulting in various effects at the software level [5]. However, state-of-the-art countermeasures have only recently begun addressing the fault sensitivity of microarchitectural components. Furthermore, the formal verification of the security of a processor design in a threat model that includes fault injection remains an open challenge [9]. Security mechanisms, targeting not only fault injections pure also pure software attacks, must indeed be designed so that their implementations can be formally proven. This would enable systems to be evaluated, for instance, following Common Criteria (ISO 15408) at a high level of assurance (EAL 6 and above require formal proof). The national TwinSec research project, which frames this PhD proposal, brings together several French laboratories specializing in hardware and software security to model and analyze fault-injections’ effects at physical, hardware (HW), Instruction Set Architecture (ISA) and software (SW) levels. It focuses on physical attacks and mainly on fault injection using lasers. Existing modeling tools are not yet capable of efficiently predicting a embedded systems’ resistance to such attacks due to generic fault models. TwinSec proposes a more realistic attacker model through multi-level analysis to identify and cancel, at the design stage, microarchitecture-specific vulnerabilities. A key approach in this research involves HW/SW contracts [4, 6], which serve as formal abstractions at the ISA level. These contracts enables system designers to reason about security properties of HW implementations independently from SW implementations and vice versa. This PhD project seeks to leverage HW/SW contracts to design and formally verify hybrid security mechanisms that integrate both hardware and software components.

**Background**. In previous work, the SUSHI team relied on the Kˆoika language developed at MIT [2] and proposed a framework to formally specify and prove hardware security mechanism 1. We have explored implementing a formally proven Control Flow Integrity mechanism in a RISC-V CPU developed in Kˆoika 2, although in a limited setting [1]. In particular, we only ensure backward-edge security with a simple shadow stack, which is of fixed size and cannot be changed between processes. However, this forms a basis for proving more complex security mechanisms. Our current approach consists in automatically compiling Kˆoika designs to a more explicit representation, and then manually proving the properties of interest on this representation. The manual proof effort for this second step is still very high, and specific to each property and security mechanism. In order to automate this last step, we have started to leverage SMT (Satisfiability Modulo Theory) solvers. This approach looks promising: we have succeeded in automatically proving the security properties of the shadow stack described in [1]. Several academic and industrial actors have now adopted the Chisel HDL 3 to design their RISC-V core, e.g., SiFive, Berkeley, or Google. We are now designing a new formal HDL in Coq (COQQTL4 ) that directly maps FIRRTL 5, the intermediate language used in the compilation of circuits described in Chisel. This formal HDL could help the adoption of our verification framework to evaluate HW/SW security extensions. Concerning fault injection attacks, we propose to consider a recent countermeasure developed at the CEA, MAFIA [3], that protects the control signals of a processor microarchitecture against fault injection attacks, as a use case driving the research work in this thesis. MAFIA was originally implemented in RTL (System Verilog) and integrated into a RISC-V RV32IM 4-stage, in-order core, the CV32E40P processor. The implementation was formally verified in part [3], using µArchiFI, an open-source tool dedicated to the formal modeling and verification of microarchitecture-level fault injections and their effects on complex hardware/software systems [8].

**PhD Topic.**The