Ingénieur scientifique contractuel / Sécurité matérielle par vérification formelle et caractérisation expérimentale

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ériel (potentiellement assisté 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.

Ces améliorations seront validées à travers plusieurs cas d'étude et confrontées à des résultats obtenus par le biais d'expérimentations réelles. Ces dernières consisteront à effectuer des caractérisations de la sécurité sur un processeur réel intégrant des contre-mesures
spécifiques pour contrer les attaques par injection de fautes. Elles apporteront une perspective scientifique et opérationnelle essentielle sur la complémentarité entre l’analyse par vérification formelle des processeurs et leur caractérisation au moyen d'attaques effectuées sur des bancs d'évaluation. Seules ces dernières sont actuellement intégrées aux processus opérationnels des Critères Communs, standard incontournable pour les produits de sécurité, tandis que l'utilisation des méthodes formelles pour la caractérisation de la sécurité des composants matériels est encore à définir.

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 :
Avec l'aide de l'encadrement de l'équipe PACAP, la personne recrutée sera amenée à établier l'état de l'art du domaine, proposer des solutions techniques aux défis du projet FORWARD, et développer les prototypes validant ces solutions.

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 :

• Analyser les besoins des partenaires industriels
• Établir l'état de l'art du domaine
• Porter la plateforme expérimentale d'analyse de vulnérabilité sur le jeu d'instructions RISC-V
• Adapter la plateforme d'injection de fautes Traitor à un processeur RISC-V implanté en FPGA
• Rédiger la documentation et les rapports

Compétences techniques :

• 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
• Sécurité sociale

Selon expériences