Grand établissement public d'enseignement supérieur, pôle de recherche reconnu, élément fondateur de l'écosystème grenoblois : Grenoble INP, l'institut d'ingénierie et de management de l’Université Grenoble Alpes (UGA), occupe une place de premier plan dans la communauté scientifique et industrielle. Grenoble INP - UGA est membre de réseaux internationaux de formation et recherche en ingénierie et management. Il est reconnu dans les classements nationaux et internationaux.
VERIMAG est un laboratoire grenoblois spécialisé dans les méthodes formelles pour la conception de systèmes critiques.
Fondé en 1993, il est rattaché à l’Université Grenoble Alpes et au CNRS. Ses recherches portent sur la vérification, la génération de tests et l’analyse de systèmes temps réel et distribués. Le laboratoire collabore avec des partenaires industriels et académiques, et participe à des projets nationaux et européens. Situé sur le campus de Grenoble, VERIMAG contribue aussi à la formation et à la recherche doctorale.
Les travaux sur l’analyse de contre-mesures en isolation, au niveau code source, ont déjà été menés à VERIMAG, ces analyses visant à garantir un placement robuste des contre-mesures [1]. L’objectif est de développer et outiller une telle méthodologie dans le jumeau numérique TwinSec, au niveau binaire, en s’appuyant sur a plate-forme open-source BinSec du CEA [2] et son greffon ASE [3] et en développant les recherches suivantes :
- définir un langage d’assertions permettant de spécifier les modèles de fautes considérés et les contre-mesures
- mettre en place des méthodes d’équivalence de programmes par exécution symbolique permettant de vérifier des propriétés de correction et de robustesse des contre- mesures
Ce travail s’inscrit dans le cadre du projet AUDACE/Twinsec opéré par le CEA
Niveau d'études minimum exigé: Bac +8 Doctorat
Pré-requis : connaissance du domaine de l'injection de fautes (attaques, contre-mesures) et des outils d'analyse de code basée sur les méthodes formelles et (C, llvm, binaire).
Travail en équipe attendue (postdoc commun VERIMAG-CEA), rédaction de livrables et participation/animation aux réunions de projet.