Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan (Prosecco, INRIA, Paris, France)
Barry Bond (RiSE, Microsoft Research, Redmond, WA, USA)
Antoine Delignat-Lavaud (Programming Principles and Tools, Microsoft Research, Cambridge, United
Kingdom)
Cédric
Fournet (Programming Principles and Tools)
Chris
Hawblitzel (Systems Research Group, Microsoft Research, Redmond,
WA, USA)
Catalin
Hritcu (Prosecco)
Samin
Ishtiaq (Programming Principles and Tools)
Markulf
Kohlweiss (Programming Principles and Tools)
Rustan
Leino (RiSE)
Jay Lorch(Systems Research Group)
Kenji Maillard (Prosecco; RiSE)
Jianyang Pang (RiSE)
Bryan Parno
(RiSE; Computer Science Department, Carnegie Mellon University,
Pittsburgh, PA, USA; Electrical and Computer Engineering Department,
Carnegie Mellon University)
Jonathan Protzenko (RiSE)
Tahina Ramananandro (RiSE)
Ashay Rane (RiSE)
Aseem
Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Nikhil
Swamy (RiSE)
Laure Thompson (RiSE)
Peng Wang (RiSE;
CSAIL, MIT, Cambridge, MA, USA)
Santiago
Zanella-Béguelin (Programming Principles and Tools)
Jean-Karim Zinzindohoué (Prosecco)
The HTTPS ecosystem is the foundation on which Internet security is
built. At the heart of this ecosystem is the Transport Layer Security
(TLS) protocol, which in turn uses the X.509 public-key infrastructure
and numerous cryptographic constructions and algorithms. Unfortunately,
this ecosystem is extremely brittle, with headline-grabbing attacks and
emergency patches many times a year. We describe our ongoing efforts in
Everest (The Everest VERified End-to-end Secure Transport) a project that
aims to build and deploy a verified version of TLS and other components
of HTTPS, replacing the current infrastructure with proven, secure
software.
Aiming both at full verification and usability, we conduct high-level
code-based, game-playing proofs of security on cryptographic
implementations that yield efficient, deployable code, at the level of C
and assembly. Concretely, we use F*, a dependently typed language for
programming, meta-programming, and proving at a high level, while relying
on low-level DSLs embedded within F* for programming low-level components
when necessary for performance and, sometimes, side-channel
resistance. To compose the pieces, we compile all our code to source-like
C and assembly, suitable for deployment and integration with existing
code bases, as well as audit by independent security experts.
Our main results so far include (1) the design of Low*, a subset of F*
designed for C-like imperative programming but with high-level
verification support, and KreMLin, a compiler that extracts Low* programs
to C; (2) an implementation of the TLS-1.3 record layer in Low*, together
with a proof of its concrete cryptographic security; (3) Vale, a new DSL
for verified assembly language, and several optimized cryptographic
primitives proven functionally correct and side-channel resistant. In an
early deployment, all our verified software is integrated and deployed
within libcurl, a widely used library of networking protocols.