Formal analysis of fault-injection countermeasures within a secure risc-v processor h/f

Le CEA est un acteur majeur de la recherche, au service des citoyens, de l'économie et de l'Etat.

Il apporte des solutions concrètes à leurs besoins dans quatre domaines principaux : transition énergétique, transition numérique, technologies pour la médecine du futur, défense et sécurité sur un socle de recherche fondamentale. Le CEA s'engage depuis plus de 75 ans au service de la souveraineté scientifique, technologique et industrielle de la France et de l'Europe pour un présent et un avenir mieux maîtrisés et plus sûrs.

Implanté au coeur des territoires équipés de très grandes infrastructures de recherche, le CEA dispose d'un large éventail de partenaires académiques et industriels en France, en Europe et à l'international.

Les 20 000 collaboratrices et collaborateurs du CEA partagent trois valeurs fondamentales :

- La conscience des responsabilités
- La coopération
- La curiosité With the rise of new development models based on open source, secure hardware components are increasingly being developed in public implementations, notably within the OpenHW Group [1]. The possibility of building a complete system from publicly available, open-source components is becoming a reality. For example, the CV32E40S RISC-V processor [2], derived from the CV32E40P [3], incorporates several hardware countermeasures against fault injection and side-channel attacks. However, a significant challenge lies in evaluating both the security level of each individual countermeasure and the overall effectiveness of these countermeasures when combined.

In [4], we introduced a method for partitioning hardware designs to formally prove the security guarantees of hardware countermeasures. This approach helps to reduce the residual attack surface that needs to BE analyzed when checking vulnerabilities at the software level. However, the types and granularity of the hardware countermeasures in the CV32E40S differ from those discussed in [4].

The goal of this internship is to adapt this partitioning methodology to the CV32E40S processor. A key challenge will BE composing the produced countermeasure-level partitions to assess the overall security of the processor against a specific fault-injection model. Additionally, the partitioning methodology could BE optimized through structural analysis of the hardware circuits, though these potential improvements have not yet been fully evaluated. Benchmarking the impact of these optimizations when building partitions could BE another possible outcome of this internship.

Opportunities :
Practical Application : Work on an open-source, real-world processor, the CV32E40S, and apply advanced methodologies to enhance its security
Technical Skills : Develop expertise in formal analysis, security verification, and countermeasures.
Publication : Potential to publish results in renowned conferences
Collaboration : Work alongside experienced researchers and engineers from CEA and LIP6
Resources : Access to state-of-the-art facilities and infrastructure.

[1] OpenHW Group. https://www.openhwgroup.org
[2] Processeur RISC-V CV32E40S. https://github.com/openhwgroup/cv32e40s
[3] Processeur RISC-V CV32E40P. https://github.com/openhwgroup/cv32e40p
[4] Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults. S. Tollec, V. Hadzic, P. Nasahl, M. Asavoae, R. Bloem, D. Couroussé, K. Heydemann, M. Jan, S. Mangard. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024(4) : 179-204 (2024)
[5] µArchiFI : Formal Modeling and Verification Strategies for Microarchitectural Fault Injections. S. Tollec, M. Asavoae, D. Couroussé, K. Heydemann, et M. Jan. in FMCAD. 2023 https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_18