2020-02738 - PhD Position F/M Preservation of the constant time property for the Jasmin compiler
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

A propos du centre ou de la direction fonctionnelle

The Inria Sophia Antipolis - Méditerranée center counts 34 research teams as well as 8 support departments. The center's staff (about 500 people including 320 Inria employees) is made up of scientists of different nationalities (250 foreigners of 50 nationalities), engineers, technicians and administrative staff. 1/3 of the staff are civil servants, the others are contractual agents. The majority of the center’s research teams are located in Sophia Antipolis and Nice in the Alpes-Maritimes. Four teams are based in Montpellier and two teams are hosted in Bologna in Italy and Athens. The Center is a founding member of Université Côte d'Azur and partner of the I-site MUSE supported by the University of Montpellier.

Contexte et atouts du poste

Side-channel attacks are physical attacks in which malicious parties extract confidential and otherwise protected data from observing the physical behavior of systems. Side-channel attacks are also among the most effective attack vectors against cryptographic implementations, as witnessed by an impressive stream of side-channel attacks against prominent cryptographic libraries.
Many of these attacks fall under the general class of timing-based attacks, i.e. they exploit the execution time of programs. In their simplest form, timing- based side-channel attacks only use very elementary facts about
execution time: for instance, branching on secrets may leak confidential information, as the two branches may have different execution times.
Formally verifying that software-based countermeasures are correctly implemented is particularly important, given the ease of introducing subtle bugs, even for expert programmers.
Some work has been done for verifying that the counter-measure are correctly implemented at the assembly level, some other work considered the problem of carrying software-based countermeasures along the compilation chain.

Mission confiée

The Phd student will study the state of the art of side-channel attacks, counter-measures like cryptographic constant time, and preservation of cryptographic constant time. Then the first step of the thesis will be to find new methods to formally verify that the Jasmin compiler preserves the cryptographic constant time. The second step, will be to understand if we can use these methods to provide a bound in the cost of the target program in term of the cost of the source program.

For a better understanding of the problem:

  • Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
    Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time".
  • Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu:
    Formal verification of a constant-time preserving C compiler.

Principales activités

Phd Thesis

Compétences

Technical skills and level required :

Languages : English

Relational skills : Motivation

Avantages

  • 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

Rémunération

Duration: 36 months
Location: Sophia Antipolis, France
Gross Salary per month: 1982€brut per month (year 1 & 2) and 2085€ brut/month (year 3)