Research and Development Engineer in Formal Methods

Inria is the French National Institute for Research in Digital Science, of which the Inria Côte d'Azur University Center is a part. With strong expertise in computer science and applied mathematics, the research projects of the Inria Côte d'Azur University Center cover all aspects of digital science and technology and generate innovation. Based mainly in Sophia Antipolis, but also in Nice and Montpellier, it brings together 47 research teams and nine support services. It is active in the fields of artificial intelligence, data science, IT system security, robotics, network engineering, natural risk prevention, ecological transition, digital biology, computational neuroscience, health data, and more. The Inria Center at Université Côte d'Azur is a major player in terms of scientific excellence, thanks to the results it has achieved and its collaborations at both European and international level.

This position is part of the FORMASK project, carried out within a consortium bringing together Inria, PQShield, and CryptoExperts, and supported by the Programme de Transfert au Campus Cyber (PTCC).

FORMASK aims to strengthen the security of cryptographic implementations against side-channel attacks (power consumption, electromagnetic radiation, execution time). Masking is currently one of the most effective software countermeasures, but implementing it correctly remains challenging. The project's goal is to develop an open, industrial-grade formal verification toolchain that guarantees both the functional correctness and the physical attack resistance of masked cryptographic implementations.

The successful candidate will primarily contribute to the development and extension of the consortium's formal verification tools (the EasyCrypt, Jasmin, and maskVerif frameworks), which form the core technical infrastructure of the project. A significant part of the work will focus on the Jasmin compiler (a low-level language for high-assurance cryptography whose semantics are formalized in Rocq/Coq): extending its formal model, sharing architecture descriptions with EasyCrypt, and improving the associated verification toolchains. This is a highly technical software engineering position at the intersection of programming languages, compiler construction, and formal methods, with developments released as open-source software.

Occasional travel (monthly consortium meetings and seminars) is expected. Travel expenses will be reimbursed in accordance with the applicable reimbursement policy.

Main responsibilities:

 With the support of the project team and under the supervision of Benjamin Grégoire, the successful candidate will be responsible for extending and improving the reliability of the formal verification tools developed within FORMASK. This includes extending proof languages and program logics to support constructs from systems programming languages, sharing hardware architecture descriptions across the consortium's tools, and strengthening the automated verification capabilities for masking countermeasures.

Learning resources:

A literature review and key scientific references (EasyCrypt, Jasmin, maskVerif, SNI/PINI security properties) will be provided to the successful candidate. These resources are also available through the team's website and the consortium's publications.

Collaboration:

The successful candidate will work closely with researchers and engineers from all three consortium partners, including the authors and maintainers of EasyCrypt and Jasmin, contributing to the continued development and consolidation of these tools.

Ownership:

The successful candidate will be responsible for designing, implementing, and validating robust and maintainable software components, while proactively improving the reliability, consistency, and reusability of the resulting tooling.

Technical leadership:

The successful candidate will independently manage the technical follow-up of their developments, ensure proper documentation, and integrate their contributions into the consortium's shared repositories.

• Design and implement extensions to programming languages and program logics within proof assistants.
• Develop compilation and translation components between multiple representations (source languages, intermediate representations, and architecture descriptions).
• Strengthen automated verification tools for the security properties of masked implementations.
• Test, validate, document, and integrate developments into the project's open-source repositories.
• Present progress and technical results to the consortium partners.

Additional activities:

• Contribute to the maintenance and overall robustness of the shared tooling.
• Participate in the dissemination of project results (public documentation, project website).
• Engage with the user community of the project's tools.

• Strong background in functional programming, ideally using OCaml (the implementation language of EasyCrypt and Jasmin). Required.
• Solid knowledge of programming language theory, including semantics, type systems, language design, or compiler construction. Required.
• Experience with a proof assistant, particularly Rocq/Coq (the semantics of the Jasmin compiler are formalized in Rocq/Coq). Strongly preferred.
• Familiarity with formal methods and verification frameworks (EasyCrypt, maskVerif). Required or strongly preferred.
• Knowledge of hardware security, side-channel attacks, and masking techniques. Desirable (training can be provided on the job).
• Familiarity with low-level programming (assembly language, instruction set architectures). A plus.

Languages: French or English (reading scientific literature and collaborating within an international consortium). Required.

Interpersonal skills: autonomy, attention to detail, ability to collaborate with distributed teams, and strong technical communication skills.

Additional desirable qualifications: contributions to open-source projects, experience developing research software, publications, or a PhD in a related field.

• 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

From 2692 € gross monthly (according to degree and experience)