Post-Doctorant F/H Vérification formelle et caractérisation expérimentale pour la sécurité matérielle

Le centre Inria de l'Université de Rennes est un des neuf centres d’Inria et compte plus d'une trentaine d’équipes de recherche. Le centre Inria est un acteur majeur et reconnu dans le domaine des sciences numériques. Il est au cœur d'un riche écosystème de R&D et d’innovation : PME fortement innovantes, grands groupes industriels, pôles de compétitivité, acteurs de la recherche et de l’enseignement supérieur, laboratoires d'excellence, institut de recherche technologique.

La vérification formelle est un outil puissant pour attester la fonctionnalité des logiciels et des composants, et elle peut également être employée pour garantir formellement la sécurité d'un logiciel. Cette approche est aujourd'hui essentielle pour les produits nécessitant un niveau élevé de sécurité. Cependant, son application à la vérification des propriétés de sécurité des composants matériels en est encore à ses débuts.

Dans le cadre d’un partenariat entre Inria (équipe-projet PACAP et Laboratoire Haute Sécurité), l'ANSSI, le CEA, l'École des Mines de Saint-Étienne, le Laboratoire d’Informatique de Paris 6, SAFRAN, et THALES, le projet FORWARD vise à contribuer aux futurs standards d'évaluation de la sécurité des composants en faisant progresser les méthodes d’analyse, notamment utilisant de la vérification formelle, appliquées aux mécanismes de protection matériels (potentiellement assistés avec du logiciel) contre les attaques par injection de fautes. Pour atteindre cet objectif, le projet comprend une phase d'amélioration des outils existants d’analyse de contre-mesures pour leur permettre d’intégrer des modèles de fautes plus complexes mais également d’analyser un système sécurisé avec une combinaison de plusieurs contre-mesures.

En particulier, l'un des volets porte sur la recherche de chemins d’attaque par injection de fautes multiples. Les contremesures sélectionnées affecteront les modèles de fautes et d’attaquant qu’il faudra supporter en améliorant un outil précédemment développé dans l'équipe. Cet outil se limite actuellement à de l’analyse statique sur le flot de contrôle et donc au niveau instruction. L’impact sur le flot de données devra être intégré afin de modéliser comment la corruption de données interagit avec le flot d’exécution du programme et ainsi mieux explorer les possibilités des attaquants. Ceci se fera par une analyse potentiellement hybride pour permettre le passage à l’échelle tout en considérant des fautes multiples. Ces travaux de recherches pourront aussi prendre en compte de nouveaux modèles de fautes propres aux partenaires du projet.

Ce poste prévoit des déplacements pour assister aux réunions  périodiques du projet ainsi que pour des sessions de travail ponctuelles entre partenaires. Les frais de déplacements seront pris en charge dans la limite du barème en vigueur.

Missions :
La personne recrutée devra mener les travaux de recherche relatifs au context du projet FORWARD, ce qui inclut établir ou compléter l'état de l'art du domaine, proposer des solutions aux défis du projet, et publier les travaux dans des conférences ou journaux internationaux.

Collaboration :
La personne recrutée sera en lien avec les différents partenaires du projet pour établier les besoins, définir les interface et présenter les solutions.

Principales activés : 

• Suivi de l'état de l'art du domaine
• Développement des travaux de recherche
• Publication des résultats obtenus
• Contribution aux livrables du projet

Compétences techniques requises :

• langages C, C++, Python
• assembleurs Arm et RISC-V
• cybersécurité, en particulier injection de fautes

Langues :

• français (lu, écrit, parlé)
• anglais (lu, écrit, parlé)

Compétences relationnelles :

• capacité à travailler en équipe

Compétences additionnelles appréciées :

• FPGA

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
• Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle

2788€ Brut