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 fonctionnelle

L’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 poste

Ce poste s'inscrit dans le projet FORMASK, mené en partenariat au sein d'un consortium réunissant Inria, PQShield et 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 œuvre 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érification du consortium (les assistants et langages EasyCrypt, Jasmin et maskVerif), au cœur de l'infrastructure technique du projet. Une part importante des travaux portera sur le compilateur Jasmin (langage bas niveau pour la cryptographie à haute assurance, dont la sémantique est formalisée en Rocq/Coq) : extension de sa modélisation, mutualisation des descriptions d'architecture avec EasyCrypt, et amélioration des chaînes de vérification associées. 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.

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ée

Missions :

Avec l'aide de l'équipe projet et sous la supervision de Benjamin Grégoire, la personne recrutée aura la charge d'étendre et de fiabiliser les outils de vérification formelle utilisés dans FORMASK. Il s'agit d'enrichir les langages et logiques de preuve pour couvrir des constructions issues des langages système, de mutualiser les descriptions d'architectures matérielles entre outils, et de renforcer les capacités de vérification automatique des contre-mesures de masquage.

Pour une meilleure connaissance du sujet :

Un état de l'art et des références scientifiques (EasyCrypt, Jasmin, maskVerif, propriétés SNI/PINI) 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 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, et prendra des initiatives pour améliorer la fiabilité, la cohérence et la réutilisabilité de l'outillage produit.

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és

Concevoir et implémenter des extensions de langages et de logiques de programme au sein d'assistants de preuve.

Développer des composants de compilation / traduction entre représentations (langages source, langages intermédiaires, descriptions d'architecture).

Renforcer les outils de vérification automatique de propriétés de sécurité d'implémentations masquées.

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é.

Participer à la diffusion des résultats (documentation publique, site du projet).

Échanger avec la communauté d'utilisateurs des outils.

Compétences

Solide maîtrise de la programmation fonctionnelle, idéalement en OCaml (langage d'implémentation d'EasyCrypt et de Jasmin). Requis.

Bonnes connaissances en théorie des langages de programmation : sémantique, systèmes de types, conception de langages ou de compilateurs. Requis.

Expérience d'un assistant de preuve, en particulier Rocq/Coq (sémantique du compilateur Jasmin formalisée en Rocq/Coq). Fortement recommandée.

Familiarité avec les méthodes formelles et les outils de vérification (EasyCrypt, maskVerif). Appréciée.

Notions de sécurité matérielle / attaques par canaux auxiliaires et de masquage. Appréciées (formation possible en poste).

Connaissance de la programmation bas niveau (assembleur, ISA). Un plus.

Langues : français et 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, publications ou doctorat dans un domaine connexe.

Avantages

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

Rémunération

A partir de 2692 € brut mensuel (selon diplôme et expérience)

Informations générales

Thème/Domaine : Sécurité et confidentialité

Ingénierie logicielle (BAP E)

Ville : Sophia Antipolis

Centre Inria : Centre Inria d'Université Côte d'Azur

Date de prise de fonction souhaitée : 2026-12-01

Durée de contrat : 2 ans

Date limite pour postuler : 2026-08-30

Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.

Consignes pour postuler

Sécurité défense :

Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.

Politique de recrutement :

Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.

Contacts

Équipe Inria : SPLITS

Recruteur :

Grégoire Benjamin / Benjamin.Gregoire@inria.fr

L'essentiel pour réussir

Nous recherchons un·e ingénieur·e R&D confirmé·e, à l'aise dans le développement logiciel exigeant comme dans un environnement de recherche. La personne idéale prend plaisir à travailler sur des bases de code complexes, aime concevoir des outils fiables et bien structurés, et sait apprendre en continu au contact d'un domaine scientifique pointu. Rigueur, autonomie, curiosité et goût du travail en équipe au sein d'un consortium sont essentiels pour réussir cette mission. Une thèse dans un domaine connexe (méthodes formelles, langages de programmation, cryptographie, compilation) constitue un réel atout, sans être indispensable.

A propos d'Inria