Formal analysis of fault-injection countermeasures within a secure RISC-V processor H/F

Vacancy details

General information

Organisation

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development and innovation in four main areas :
• defence and security,
• nuclear energy (fission and fusion),
• technological research for industry,
• fundamental research in the physical sciences and life sciences.

Drawing on its widely acknowledged expertise, and thanks to its 16000 technicians, engineers, researchers and staff, the CEA actively participates in collaborative projects with a large number of academic and industrial partners.

The CEA is established in ten centers spread throughout France
  

Reference

2024-33935  

Description de l'unité

The French Atomic Energy and Alternative Energies Commission (CEA) is a major player in research, development and innovation. This technological research organization is active in three main areas: energy, information and health technologies, and defense. Recognized as an expert in its fields, CEA is fully integrated into the European research area and is expanding its presence internationally. The Laboratory for Systems and Technology Integration (LIST), located in the southern Île-de-France region (Saclay), has the mission of contributing to technology transfer and promoting innovation in the field of parallel computing systems.

The Environmental Design and Architecture Laboratory (LECA), within the Digital Systems and Integrated Circuits Department (DSCIN), is a multidisciplinary technological research team comprising experts in hardware IP design and simulation tools.

Position description

Category

Mathematics, information, scientific, software

Contract

Internship

Job title

Formal analysis of fault-injection countermeasures within a secure RISC-V processor H/F

Subject

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, devel-opment and innovation in four main areas: defense and security, nuclear and renewable energies, tech-nological research for industry, fundamental research in the physical sciences and life sciences. Drawing on its widely acknowledged expertise, the CEA actively participates in collaborative projects with a large number of academic and industrial partners. One of three institutes that comprise CEA Tech, the List institute is committed to technological innovation in digital systems. Within the DSCIN department of CEA List, the LECA and LFIM laboratories invest R&D efforts in the analysis of the robustness of embedded systems against fault-injection attacks.
http://www-list.cea.fr/
This is a joint internship with LIP6.

Contract duration (months)

6

Job description

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

Applicant Profile

This position is aimed at students seeking an ambitious technical internship, eager to gain significant experience in industry-related technological research. It is particularly well-suited to students considering a doctorate, with new funded positions offered each year within the department. The internship is aimed at students in their final year of engineering school (or Master 2) in computer science or microelectronics, or equivalent levels, preferably with a specialization in processor systems/architecture or formal methods. Knowledge of micro-architecture or cybersecurity is an asset, but not a prerequisite. A strong capacity for personal work, ability to work in a team and motivation to take on technical challenges are essential.

 

In line with CEA's commitment to integrating people with disabilities, this job is open to all.

 

Position location

Site

Saclay

Job location

France, Ile-de-France, Essonne (91)

Location

  Palaiseau

Candidate criteria

Languages

English (Fluent)

Prepared diploma

Bac+5 - Master of Science

PhD opportunity

Non