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 proof assistant and the Jasmin language), as well as to the development of formal proofs establishing the correctness of cryptographic implementations. A significant aspect of the position concerns Rust: on the one hand, the development of tooling in Rust (translation and verification components), and on the other, the verification of Rust code in EasyCrypt through a transpilation pipeline targeting the proof assistant. This is a highly technical software engineering role at the intersection of programming languages, compilation, and formal methods. The resulting developments will be released as open-source software and will subsequently support PQShield's industrial cryptographic products.

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 Pierre-Yves Strub, the successful candidate will be responsible for extending and improving the reliability of the formal verification tools used in FORMASK. This includes extending proof languages and program logics to support constructs from systems programming languages, developing a translation pipeline from Rust to the proof assistant, building reusable abstract libraries of cryptographic components (gadgets), and formally establishing the correspondence between concrete implementations and high-level specifications.

Learning resources:

A literature review and key scientific references (EasyCrypt, Jasmin, Why3, SNI/PINI security properties, verification of masked implementations) 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 Pierre-Yves Strub and with researchers and engineers from all three consortium partners, including the authors and maintainers of EasyCrypt and Jasmin, contributing to the evolution and consolidation of these tools.

Ownership:

The successful candidate will be responsible for the design, implementation, and validation of robust and maintainable software components (particularly in Rust), together with their associated formal proofs. They will proactively improve the generality, automation, and reusability of both the proofs and the supporting 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 Rust tooling (translation and verification components), including a transpilation pipeline enabling the verification of Rust programs in EasyCrypt.
• Develop formal proofs of correctness and equivalence between concrete implementations and abstract specifications, and build reusable libraries of cryptographic components.
• 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.
• Improve proof automation through the integration of SMT solvers and automated reasoning engines.
• Contribute to the dissemination of project results (public documentation, project website) and prepare the application of the developed tools to industrial use cases.

• Strong proficiency in Rust (tooling development and verification of Rust code). Required or highly desirable.
• Solid background in functional programming, ideally using OCaml (the implementation language of EasyCrypt and Jasmin). Required.
• Experience with a proof assistant or formal verification framework (ideally EasyCrypt, or Rocq/Coq, F*, Why3, etc.).Desirable.
• Strong knowledge of programming language theory, including semantics, program logics, language design, or compiler construction. Required.
• Familiarity with SMT solvers (such as CVC5 or Z3) and automated reasoning engines. Desirable.
• Knowledge of cryptography, masking techniques, and side-channel security. Desirable (training can be provided on the job).

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 large-scale research software or formal proofs, publications, or a PhD in a related field.

• Subsidized meals
• Partial reimbursement of public transport costs
• Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
• Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
• Professional equipment available (videoconferencing, loan of computer equipment, etc.)
• Social, cultural and sports events and activities
• Access to vocational training
• Social security coverage

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