Séminaire des équipes de recherche
Séminaire Gallium : The EverCrypt verified cryptographic provider
EverCrypt is a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API.
- Date : 14/10/2019
- Lieu : Inria de Paris, Salle Lions 1, bâtiment C - 10h30
- Intervenant(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.