Please
welcome Jonathan Protzenko as our speaker this
month! Sponsor details coming soon!
Time and Location
July
17th, 2019 at 7:00 PM
Microsoft
Campus,
156th
Ave NE,
Redmond, WA 98052.
Title
EverCrypt: a no-excuses, industrial-grade
cryptographic library, with full verification
Abstract
Project Everest is a large,
multi-year, collaborative research effort spread
between Microsoft Research, Carnegie Mellon,
INRIA and University of Edinburgh. The aim of
Project Everest is to deploy formally verified
implementations of the TLS protocol, which now
powers the majority of online communications.
Project Everest is about half-way through its
projected five year lifespan.
After a brief presentation of Everest at large,
I will focus on EverCrypt, the cryptographic
provider that powers our TLS implementation,
offering a variety of cryptographic algorithms
written in a mixture of C and assembly. I will
detail the various techniques we used, the
verification APIs we offer, and the state-of-the
art performance we obtain. EverCrypt is suitable
for use by verified and unverified clients
alike, using an agile and multiplexing API.
Parts of EverCrypt have been deployed, among
others, in Firefox, the Wireguard VPN, Windows,
and the Tezos blockchain.
Speaker Bio
Jonathan
Protzenko is a Researcher in the RiSE
group at Microsoft Research Redmond, which he
joined in Fall 2014.
Jonathan's research
focuses on formally verifying critical software,
i.e. showing with mathematical certainty that
the software has no bugs and exhibits the
intended behavior. To that end, I use the F*
programming language, and its new Low*
toolchain. It allows compiling a subset of F*
programs to C for integration into existing
software ecosystems. Code written in Low* and
compiled by KReMLin has been integrated into
Windows, Firefox, mbedTLS, and the Tezos
blockchain, among others.
Jonathan's flagship
project is EverCrypt, a complete cryptographic
library that offers abstraction, multiplexing,
agility and CPU auto-detection, verified in F*,
compiled to C and assembly. My work is part of
the larger Everest Project, an ambitious
research effort spanning three continents, five
institutions and twelve timezones.
In his spare time, he maintains several
open-source projects, including a Thunderbird
addon that is now the 4th most-used addon with
200,000 users.
A Word From Our Sponsor
Paul is also our pizza sponsor this
month! Thanks Paul!!!!