Ingénieur·e de Recherche et Développement en Méthodes Formelles H/F - INRIA

A propos d'Inria Inria est l'institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l'interface d'autres disciplines. L'institut fait appel à de nombreux talents dans plus d'une quarantaine de métiers différents. 900 personnels d'appui à la recherche et à l'innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'eorce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.
Ingénieur·e de recherche et développement en méthodes formelles Type de contrat : CDD Niveau de diplôme exigé : Bac +5 ou équivalent Autre diplôme apprécié : Doctorat Fonction : Ingénieur scientifique contractuel A propos du centre ou de la direction fonctionnelleL'Inria est l'Institut national de recherche en sciences du numérique, dont le centre Inria d'Université Côte d'Azur fait partie. Avec une forte expertise en informatique et mathématiques appliquées, les projets de recherche du centre Inria d'Université Côte d'Azur touchent toutes les dimensions des sciences et technologies du numérique, et génèrent de l'innovation. Implanté principalement à Sophia Antipolis, mais également à Nice ou Montpellier, il regroupe 47 équipes de recherche et neuf services d'appui. Il est présent dans les domaines de l'intelligence artificielle, la science des données, la sécurité des systèmes informatiques, la robotique, l'ingénierie de réseaux, la prévention des risques naturels, la transition écologique, la biologie numérique, les neurosciences computationnelles, les données de santé... Le Centre Inria d'Université Côte d'Azur est un acteur majeur en termes d'excellence scientifique par les résultats obtenus et les collaborations tant au niveau européen qu'international.Contexte et atouts du posteCe poste s'inscrit dans le projet FORMASK, mené en partenariat au sein d'un consortium réunissant Inria, PQShieldet CryptoExperts, et soutenu par le Programme de Transfert au Campus Cyber (PTCC).FORMASK vise à renforcer la sécurité des implémentations cryptographiques face aux attaques par canaux auxiliaires(consommation électrique, rayonnement électromagnétique, temps d'exécution). Le masquage est aujourd'hui l'une des contre-mesures logicielles les plus efficaces, mais sa mise en oeuvre correcte reste délicate. L'objectif du projet est de développer une chaîne d'outils de vérification formelle, ouverte et industrialisable, garantissant à la fois la correction fonctionnelle et la résistance aux attaques physiques de ces implémentations.La personne recrutée contribuera principalement au développement et à l'extension des outils de vérificationdu consortium (les assistants et langages EasyCrypt** et Jasmin), ainsi qu'à l'écriture de preuves formelles qui garantissent la correction des implémentations. Une dimension importante du poste concerne le langage Rust: d'une part le développement d'outillage en Rust(composants de traduction et de vérification), d'autre part la vérification de code Rust dans EasyCrypt, via une chaîne de transpilation vers l'assistant de preuve. C'est un poste à forte composante ingénierie logicielle de haut niveau, à l'interface entre langages de programmation, compilation et méthodes formelles, avec des développements publiés en open source, qui pourront ensuite être appliqués aux produits cryptographiques de PQShield.Des déplacements ponctuels (réunions mensuelles du consortium, séminaires) sont à prévoir ; les frais de déplacement seront pris en charge dans la limite du barème en vigueur.Mission confiéeMissions:Avec l'aide de l'équipe projet et sous la supervision de Pierre-Yves Strub, la personne recrutée aura la charge d'étendre et de fiabiliser les outils de vérification formelleutilisés dans FORMASK.Il s'agit d'enrichir les langages et logiques de preuve pour couvrir des constructions issues des langages système, de développer une chaîne de traduction depuis Rust vers l'assistant de preuve, de construire des bibliothèques abstraites et réutilisables de composants cryptographiques (gadgets), et d'établir la correspondance formelle entre implémentations concrètes et spécifications de haut niveau.Pour une meilleure connaissance du sujet :Un état de l'art et des références scientifiques (EasyCrypt, Jasmin, Why3, propriétés SNI/PINI, vérification d'implémentations masquées) pourront être communiqués au candidat ; ils sont accessibles via le site de l'équipe et les publications du consortium.Collaboration :La personne recrutée travaillera en lien étroit avec Pierre-Yves Strub et les chercheurs et ingénieurs des trois partenaires (notamment les auteurs et mainteneurs d'EasyCrypt et de Jasmin), dont elle prolongera et consolidera les développements.Responsabilités :Elle est responsable de la conception, de l'implémentation et de la validation de composants logiciels robustes et maintenables (en particulier en Rust), ainsi que des preuves formelles associées ; elle prendra des initiatives pour rendre ces preuves et cet outillage plus génériques, automatisés et réutilisables.Pilotage :Elle assurera le suivi technique de ses développements, leur documentation et leur intégration dans les dépôts partagés du consortium, en autonomie sur son périmètre.Principales activitésConcevoir et implémenter des extensions de langages et de logiques de programme au sein d'assistants de preuve.Développer, en Rust, des composants d'outillage (traduction, vérification) et une chaîne de transpilation permettant la vérification de code Rust en EasyCrypt.Écrire des preuves formelles de correction et d'équivalence entre implémentations concrètes et spécifications abstraites, et construire des bibliothèques réutilisables de composants cryptographiques.Tester, valider et documenter les développements ; les intégrer dans les dépôts open source du projet.Présenter l'avancement des travaux aux partenaires du consortium.Activités complémentaires :Contribuer à la maintenance et à la robustesse générale de l'outillage partagé.Renforcer l'automatisation des preuves via l'intégration de solveurs (SMT) et de moteurs de raisonnement.Participer à la diffusion des résultats (documentation publique, site du projet) et préparer l'application des outils à des cas d'usage industriels.CompétencesBonne maîtrise du langage Rust(développement d'outillage et vérification de code Rust). Requise ou fortement appréciée.Solide maîtrise de la programmation fonctionnelle, idéalement en OCaml(langage d'implémentation d'EasyCrypt et de Jasmin). Requis.Expérience d'un assistant de preuve ou d'un outil de vérification formelle(idéalement **EasyCrypt**, ou Rocq/Coq, F*, Why3...). Fortement appréciée.Bonnes connaissances en théorie des langages de programmation: sémantique, logiques de programme, conception de langages ou de compilateurs. Fortement appréciée.Familiarité avec les solveurs SMT(CVC5, Z3) et les moteurs de raisonnement automatique. Appréciée.Notions de cryptographieet de masquage / sécurité contre les canaux auxiliaires. Appréciées (formation possible en poste).Langues :françaisou anglais(lecture de littérature scientifique et échanges au sein du consortium international). Requis.Compétences relationnelles :autonomie, rigueur, capacité à collaborer avec des équipes réparties, sens de la communication technique.Compétences additionnelles appréciées :contribution à des projets open source, expérience de développement d'outils de recherche ou de preuves formelles à l'échelle, publications ou doctorat dans un domaine connexe.AvantagesRestauration subventionnéeTransports publics remboursés partiellementCongé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 oeuvres sociales d'Inria)Accès à la formation professionnelleSécurité socialeRémunérationA partir de 2692 €brut mensuel (selon diplôme et expérience)

• Programmation
• Sécurité du Système informatique
• Anglais
• Intelligence artificielle
• Autonomie
• Plan de prévention
• Traduction
• Langages de programmation
• Mathématiques
• Robotique