Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle C334, bâtiment C Lundi 17 octobre, 10h30 ------------------ Jonathan Protzenko ------------------ Microsoft Research ======================= Extracting from F* to C ======================= As part of the greatest Everest expedition, we are setting out to implement, verify and deploy a TLS implementation -- TLS is the successor to SSL and is the prevalent secure communication protocol on the internet. If we do wish people to adopt our cryptography, we need to make it competitive with existing implementations -- that is, make it fast. The current extraction from F* to OCaml (and F#) was hitting severe performance limitations for cryptographic code. Indeed, we are competing with hand-optimized C code that uses native machine integers. Our approach essentially consists of a shallow embedding of C in F*; our new monad of effects called HyperStack models stack-based allocation. We take the original C code, hand-transcribe it in F*, then prove it memory-safe, functionally-correct, and cryptographically sound. The code can then be extracted back to C where is has very competitive performance, and enjoys verification.