Research and Development Engineer in Formal Methods

Inria; Paris; Sur place; EUR 27 338 - 32 746; Plein temps

Avantages offerts par ce poste

Partial reimbursement of public travel

Leave: 7 weeks annual leave + RTT days

Teleworking after 6 months

Professional equipment

Social, cultural and sports events

Vocational training

Social security coverage

Résumé du poste

Inria is seeking an experienced Research and Development Engineer to join the FORMASK project, focusing on formal verification of cryptographic implementations. The role emphasizes extending Rust tooling, translating Rust to a proof assistant, and building reusable libraries for cryptographic components.

The candidate will work with EasyCrypt, Jasmin, OCaml, and SMT solvers, contributing to open-source tooling and ensuring high-quality software engineering within a multidisciplinary consortium.

Qualifications

• PhD in formal methods, programming languages, cryptography, or related field preferred.
• Strong proficiency in Rust and OCaml.
• Experience with a proof assistant (EasyCrypt, Coq, Why3) desirable.
• Knowledge of SMT solvers (CVC5, Z3) and side-channel security desirable.

Responsabilités

• Extend and improve reliability of formal verification tools (EasyCrypt, Jasmin).
• Translate and verify Rust code within a transpilation pipeline.
• Develop reusable libraries of cryptographic components.
• Present progress to consortium partners.
• Document and integrate developments into open-source repositories.

Connaissances

Rust programming

OCaml

Formal methods

Proof engineering

Formation

Graduate degree

PhD preferred

Outils

EasyCrypt

Jasmin

Coq/Why3

SMT solvers

Rust tooling

Description du poste

Research and Development Engineer in Formal Methods

Level of qualifications required : Graduate degree or equivalent

Other valued qualifications : Phd these

Fonction : Temporary scientific engineer

About the research centre or Inria department

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.

Context

This position is part of the FORMASKproject, 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 EasyCryptthrough 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.

Assignment

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.

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.

Main activities

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

Skills

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

Benefits package

• 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

Remuneration

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

• Theme/Domain :Security and Confidentiality
  Software engineering(BAP E)

Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.

Instruction to apply

Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST). Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.

Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.

We are looking for an experienced R&D engineer who is equally comfortable with high-quality software engineeringand research-oriented development. The ideal candidate enjoys working with complex codebases, designing reliable and well-structured tools, developing mechanized proofs, and continuously learning in a scientifically demanding environment. Rigor, autonomy, curiosity, and the ability to collaborate effectively within a multidisciplinary consortium are essential. A PhD in a related field (formal methods, programming languages, cryptography, or compilation) is a strong asset but is not required.

About Inria

Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.