19/04/2021
The Human Resources Strategy for Researchers
European Research Council

CDD researcher (M / F): Foundation and Development of a formal verification tool

This job offer has expired


  • ORGANISATION/COMPANY
    CNRS
  • RESEARCH FIELD
    Computer science
    MathematicsAlgorithms
  • RESEARCHER PROFILE
    First Stage Researcher (R1)
  • APPLICATION DEADLINE
    08/06/2021 23:59 - Europe/Brussels
  • LOCATION
    France › RENNES
  • TYPE OF CONTRACT
    Temporary
  • JOB STATUS
    Full-time
  • HOURS PER WEEK
    35
  • OFFER STARTING DATE
    01/07/2021
  • EU RESEARCH FRAMEWORK PROGRAMME
    H2020 / ERC

OFFER DESCRIPTION

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

- 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. For that, it will be necessary to understand the functioning of a Squirrel proof in order to be able to put forward in graphic form the essential elements.

- 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. We must begin by defining this notion of executability.

- Interfacing with SMT solvers. We would like to make the tool as automatic as possible especially for the proof of simple objectives. Some dedicated algorithms have already been implemented. However, to go further, we would like to propose an interface towards SMT solvers such as for example the Why3 solver. Again, a theoretical work will have to be done upstream to understand how an SMT solver can be used in this context.

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

The researcher 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 researcher will join the SPICY team being created, whose activity targets research questions related to the security of cryptographic protocols.
The researcher will work with Stéphanie Delaune (IRISA, Rennes), Adrien Koutsos (Inria Paris, Prosecco), and David Baelde (ENS Paris-Saclay).

More Information

Eligibility criteria

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

Additional comments

Web site for additional job details

Required Research Experiences

  • RESEARCH FIELD
    Computer science
  • YEARS OF RESEARCH EXPERIENCE
    None
  • RESEARCH FIELD
    MathematicsAlgorithms
  • YEARS OF RESEARCH EXPERIENCE
    None

Offer Requirements

  • REQUIRED EDUCATION LEVEL
    Computer science: PhD or equivalent
    Mathematics: PhD or equivalent
  • REQUIRED LANGUAGES
    FRENCH: Basic
Work location(s)
1 position(s) available at
Institut de Recherche en Informatique et Systèmes Aléatoires
France
RENNES

EURAXESS offer ID: 630871
Posting organisation offer ID: 21037

Disclaimer:

The responsibility for the jobs published on this website, including the job description, lies entirely with the publishing institutions. The application is handled uniquely by the employer, who is also fully responsible for the recruitment and selection processes.

 

Please contact support@euraxess.org if you wish to download all jobs in XML.