Design and Formal Verification of Hardware/Software Security Mechanisms

Organisation/Company: CentraleSupélec

Research Field: Computer science » Computer architecture

Researcher Profile: First Stage Researcher (R1)

Country: France

Application Deadline: 20 Dec 2025 - 00:00 (UTC)

Type of Contract: To be defined

Job Status: Negotiable

Is the job funded through the EU Research Framework Programme? Not funded by a EU programme

Is the Job related to staff position within a Research Infrastructure? No

Offer Description

We are seeking a highly motivated PhD student to work on formal verification of security mechanisms against fault-injection attacks. This PhD is part of the TwinSec national research project and a collaboration between CentraleSupélec and CEA, focusing on hardware/software security.

Location: CentraleSupélec Rennes (IRISA Lab, Inria SUSHI team)
Collaboration: CentraleSupélec & CEA
Start date: Before the end of 2025 (possibility of a Master’s internship before the PhD)

Research Areas:

• Formal verification of security mechanisms
• Hardware/software contracts for security
• Fault injection attacks and countermeasures

Required Skills/Interests:

• Hardware design (Verilog/VHDL) or formal methods (Coq, SMT solvers)
• Interest in hardware security and fault attacks (prior experience is a plus, but not required)