International Association
for Cryptologic Research

Context Our team develops pre-silicon analysis tools to: 1) identify exploitable vulnerabilities at the software level based on these interactions between a software and a microarchitecture, or 2) formally prove the security, for a given attacker model, of a system embedding hardware/software countermeasures against fault injections. These tools implement a methodology that has shown to be successful to find microarchitectural vulnerabilities and/or prove the robustness, for a given fault model, of various RISC-V based processors [S. Tollec et al. FMCAD 2023]. For instance, we have formally proven the security of OpenTitan's processor to single bit-flip injections [S. Tollec et al. TCHES 2024].

Scientific Challenge In this thesis, we aim to formalize HW/SW contracts dedicated to the security analysis of embedded systems in the context of fault injection attacks.

Goals and Expected Contributions The long-term goal is to create efficient techniques and tools that contribute to the design and assessment of secured systems, reducing the time-to-market during the design phase of secure systems. We foresee the investigation of several research questions:

Requirements Masters’s Degree in Electronics or Computer Science. Excellent interpersonal and communication skills, and a solid background in any of the following fields is expected: computer architecture, programming languages, formal methods, cyber-security. Knowledge or French (spoken or written) is not required but may be helpful on a day-to-day basis.

Application Detailed version of this research position upon demand. Please send the following documents: CV, cover letter (in French or English), transcript of records