En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR6074-STEDEL-001 - Ingénieur de recherche (H/F): développement d'un outil de vérification formelle

Research engineer (M / F): development of a formal verification tool

This offer is available in the following languages:
Français - Anglais

Date Limite Candidature : mardi 8 juin 2021

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler. Les informations de votre profil complètent celles associées à chaque candidature. Afin d’augmenter votre visibilité sur notre Portail Emploi et ainsi permettre aux recruteurs de consulter votre profil candidat, vous avez la possibilité de déposer votre CV dans notre CVThèque en un clic !

Faites connaître cette offre !

General information

Reference : UMR6074-STEDEL-001
Workplace : RENNES
Date of publication : Tuesday, May 18, 2021
Type of Contract : FTC Technical / Administrative
Contract Period : 12 months
Expected date of employment : 1 July 2021
Proportion of work : Full time
Remuneration : between 2400 and 3100 euros gross monthly depending on experience
Desired level of education : Higher than 5-year university degree
Experience required : Indifferent


The mission of the Research Engineer will be to contribute to the development of the Squirrel verification tool (https://github.com/squirrel-prover/squirrel-prover/), a tool dedicated to the verification of cryptographic protocols and whose foundations are based on logic.


In order to contribute to the development of the Squirrel tool, various activities may be carried out. This list is not exhaustive and can be discussed with the candidate.

- Improved user interface. Currently, the protocol and properties specification as well as the proofs are in text mode. We would like to set up a web output summarizing the results to allow the average user to access the results produced by the Squirrel Prover.
- Graphic representation during the development of the proof. When performing a proof with the Squirrel tool, the goal and the available hypotheses are displayed in text mode. We would like to provide a graphical representation to help the user to complete his proof as is done for example in the Tamarin tool.
- Executability of the specification. One difficulty in analyzing a protocol is to write a correct specification first. To verify that the specification produced is reasonable, one option is to simulate protocol executions. We would like to add this functionality to the Squirrel tool.


A computer engineering degree or doctorate is required.
We are looking for candidates with good Ocaml programming skills. In particular,
the ability to write, understand and debug clean and maintainable software code written in Ocaml is required.
Certain computer skills (logic, automated deduction, ...) will be appreciated. Some security knowledge is an asset but is not required. Knowledge of the French language is not compulsory for the position.

Work Context

The engineer will work at IRISA (Rennes).

Public research laboratory in computer science, automation, signal and image processing and robotics, located in Rennes, Lannion, Vannes and bringing together more than 800 people, IRISA manages around forty research teams, as well as several common services and technological platforms. Its resources are made up of staff, budgets, premises and equipment allocated individually by its 8 public institutions.

The engineer will join the SPICY team being created, whose activity targets research questions related to the security of cryptographic protocols.
The engineer worked with Stéphanie Delaune (IRISA, Rennes), Adrien Koutsos (Inria Paris, Prosecco), and David Baelde (ENS Paris-Saclay).

Additional Information


We talk about it on Twitter!