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 [1]. For instance, we have formally proven the security of OpenTitan's processor to single bit-flip injections [2].

[1] S. Tollec et al. μArchiIFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections. FMCAD 2023

[2] S. Tollec et al.. Fault-Resistant Partitioning of Secure CPUs for System Co-Verification against Faults. TCHES 2024

Objectives

Your main missions will be:

- To design and extend our pre-silicon methodology and associated tools to support different secured processors. In particular, leverage the specificities of the countermeasures embedded by such secured processors to speedup analysis techniques, but also integrate in our methodology and tools post-synthesis netlist level analyses of hardware architectures.

- To participate to a project-scale experimental evaluation aiming to fill the gap between pre-silicon tools and post-silicon security evaluations.

Location Saclay (Paris area) or Grenoble.

Requirements PhD or a 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 Please send the following documents: CV, cover letter (in French or English), transcrpit of records

Closing date for applications:

Contact: Mathieu Jan (mathieu.jan@cea.fr) and Damien Couroussé (damien.courousse@cea.fr). Reviewing of applications will continue until the position is filled.