Open post-doc/engineer position on Protocol Verification in the Computational Model
Environment
The post-doc will work in the Prosecco project of the INRIA Paris research center, located at 2 rue Simone Iff,
75012 Paris (near Gare de Lyon). The Prosecco project offers an
exciting research environment. It deals with formal and practical
security research on cryptographic protocols, software security, web
security, and hardware protection mechanisms. To this end, we design
and implement programming languages, formal verification tools,
dynamic monitors, testing frameworks, verified compilers, etc.
Planed work
The Prosecco project-team develops CryptoVerif (http://cryptoverif.inria.fr), a computational security
protocol verifier that generates proofs by sequences of games, like
the proofs manually written by cryptographers.
This verifier is implemented in OCaml.
The post-doc will work on improvements and extensions of CryptoVerif,
in the frame of the ANR project TECAP.
Possible work includes:
- new game transformations, for instance to guess the tested session,
or to remove parts of the cryptographic game such that the adversary
never wins when he executes them.
- extensions to reduce the size of games, which tends to grow too much
on complex examples.
- specialized prover to simplify random oracle calls, based on indifferentiability
lemmas (this simplification will be used before the rest of the
CryptoVerif proof, to simplify the initial game).
- extensions to deal with protocols with mutable state and loops.
- extensions to improve the compatibility with the symbolic
cryptographic protocol verifier ProVerif (another of our
protocol verifiers),
that is, add to CryptoVerif features that ProVerif has.
- extensions to interface with the prover EasyCrypt, for instance to delegate to EasyCrypt
the proof of assumptions on primitives or to delegate parts of the
proof that CryptoVerif cannot do. This work would be done in
collaboration with EasyCrypt authors and their team (Pierre-Yves
Strub, Benjamin Grégoire, Clément Sartori).
- protocol case studies using CryptoVerif, which may in turn
suggest further extensions.
The post-doc will design, prove correct, and implement these extensions.
He/she will obviously publish his/her work in high quality computer science
conferences. He/she will collaborate with other members of the team
working on CryptoVerif and related topics (Bruno Blanchet, Benjamin
Lipp, Karthikeyan Bhargavan).
It is unlikely that he/she will have time to work on all these extensions,
they are possible directions among which he/she will be able to choose,
and his/her own ideas of possible extensions and research directions
will also be most welcome.
We will also consider applications of research engineers. In this case,
the design and proof part would mostly be done by other members of the team,
and the engineer would focus mainly on the implementation part.
Required expertise
- knowledge in cryptography and/or in formal methods: program
semantics, static analysis, program transformations.
- knowledge of the OCaml language. (The knowledge of the object part
of Ocaml is not required.)
- fluency in English (or French for an engineer).
- a PhD in computer science is required.
Further information
- Duration: the initial contract will be for 1 year, with possibility
of further extensions (for a total duration of less than 6 years),
subject to available funding.
- Expected Start Date: beginning of 2019 (We have a 2 months hiring delay.)
- Contact: please send detailed curriculum vitae, motivation letter, and
references to Bruno Blanchet, bruno DOT blanchet AT inria DOT fr
Bruno Blanchet