2021-03774 - Post-Doctoral Research Visit F/M Deploying Proof-Oriented Programming at Scale

Contract type : Fixed-term contract

Level of qualifications required : PhD or equivalent

Fonction : Post-Doctoral Research Visit


Structuring programs with proofs in mind is a promising way to reduce the effort of building trustworthy software. Such an approach results in a myriad of benefits. On one side, the program can be structured to simplify proofs, reducing the burden on the developer while enabling strong, formal guarantees about its correctness and security. On the other hand, proofs can simplify and optimize the program, for instance by eliminating checks and cases that can be statically ruled out

Main activities

The research aims at applying a proof-oriented methodology to improve the reliability of real-world software. To this end, the candidate will investigate fundamental improvements to the expressiveness and programmability of proof-oriented languages, while demonstrating their usefulness on security-critical real-world systems. Secure communication protocols, for instance TLS, QUIC, or Wireguard, foundation of Internet security, are a prime target for verification. They build on secure cryptographic implementations such as EverCrypt, but use them to implement a protocol, commonly described as a state machine, while enabling communication with several parties at the same time; their implementations thus must be concurrent.

Benefits package

  • 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