Ingénieur·e de recherche et développement en méthodes formelles

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)