Lieu
Rennes
Type de contrat
CDD
Département
Equipe de recherche
Contexte
The security of applications eventually depends on the security of all the abstraction layers upon which they are built. Formal methods allow for high confidence in such systems and have been successfully applied to prove
functional properties at various levels: at the compiler (e.g., CompCert), OS (seL4, CertiKOS), and hardware level (e.g. Kami, Kôika).
Formal methods can also be applied to security properties to prove the absence of certain classes of vulnerabilities. Such approaches are mandatory for high assurance levels (e.g., EAL6-7 in the Common Criteria, ISO/IEC 15408). One of the challenges is considering the different attacker models and their implications at each layer of the software/hardware stack.
Researchers in the Inria SUSHI group have been using formal methods to prove security properties at the software/hardware interface: at the compiler, OS, and hardware level.
functional properties at various levels: at the compiler (e.g., CompCert), OS (seL4, CertiKOS), and hardware level (e.g. Kami, Kôika).
Formal methods can also be applied to security properties to prove the absence of certain classes of vulnerabilities. Such approaches are mandatory for high assurance levels (e.g., EAL6-7 in the Common Criteria, ISO/IEC 15408). One of the challenges is considering the different attacker models and their implications at each layer of the software/hardware stack.
Researchers in the Inria SUSHI group have been using formal methods to prove security properties at the software/hardware interface: at the compiler, OS, and hardware level.
Mission
We seek a postdoc candidate to conduct research using formal methods to prove security at various software/hardware interface levels. A nonexhaustive list of topics that could be explored would be
• proofs mixing compiler (e.g., CompCert) and hardware support to enforce CFI
• proving security of RISC-V enclaves
• proving that our hardware implementation of a RISC-V processor correctly implements the RISC-V ISA (e.g., with SAIL)
• stating and proving software/hardware contracts
• proofs mixing OS and hardware support for isolation
Profil / Compétences
The candidate should have a strong background with formal methods in general and proof assistants in particular.
Knowledge and experience with computer security, compilers, operating systems, or hardware design languages are
welcome.
Knowledge and experience with computer security, compilers, operating systems, or hardware design languages are
welcome.
Durée du contrat (en mois)
24
Quotité
100%
Lieu de travail
CentraleSupélec Rennes
Diplôme requis
Doctorat en Informatique
Salaire brut mensuel
3000-3200
Date prévisionnelle d'embauche
octobre 2025
Date limite de candidature
Candidater
Please send your application to Pierre Wilke and Guillaume Hiet (firstname.lastname@irisa.fr). Your application should contain
a resume, a link to your Ph.D. thesis or the presumed defense date, and recommendation letters.
a resume, a link to your Ph.D. thesis or the presumed defense date, and recommendation letters.
Pièce jointe à l'offre d'emploi