Sites Inria

English version

Séminaire des équipes de recherche

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
  • 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.

Mots-clés : Research Inria de Paris Science Gallium Séminaire Cryptographic EverCrypt

Haut de page

Suivez Inria