Sites Inria

Version française

Research Teams Seminar

Séminaire Gallium : The EverCrypt verified cryptographic provider

© INRIA Sophie Auvin - G comme Grille

EverCrypt is a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. 

  • Date : 14/10/2019
  • Place : Inria de Paris, Room Jacques Louis Lions 1, building C - 10:30am
  • Guest(s) : Jonathan Protzenko, Microsoft Research

The API provably supports agility (choosing between multiple algorithms for the same functionality) and multiplexing (choosing between multiple implementations of the same algorithm). 

I will first give a high-level overview: supported algorithms, performance, general architecture of the library. I will then switch to a more PL perspective, showing how the judicious use of meta-programming allows us to avoid a lot of effort. I will also dwell on our style of stateful abstract invariants stated against abstract specifications.

Keywords: EverCrypt Cryptographic Seminar Gallium Science Inria de Paris Research