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

Missions :

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

• Concevoir 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étences

• Bonne 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 cryptographie et de masquage / sécurité contre les canaux auxiliaires. Appréciées (formation possible en poste).

Langues : français ou 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.

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)