License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SNAPL.2017.1
URN: urn:nbn:de:0030-drops-71196
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7119/
Bhargavan, Karthikeyan ;
Bond, Barry ;
Delignat-Lavaud, Antoine ;
Fournet, Cédric ;
Hawblitzel, Chris ;
Hritcu, Catalin ;
Ishtiaq, Samin ;
Kohlweiss, Markulf ;
Leino, Rustan ;
Lorch, Jay ;
Maillard, Kenji ;
Pan, Jianyang ;
Parno, Bryan ;
Protzenko, Jonathan ;
Ramananandro, Tahina ;
Rane, Ashay ;
Rastogi, Aseem ;
Swamy, Nikhil ;
Thompson, Laure ;
Wang, Peng ;
Zanella-Béguelin, Santiago ;
Zinzindohoué, Jean-Karim
Everest: Towards a Verified, Drop-in Replacement of HTTPS
Abstract
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.
BibTeX - Entry
@InProceedings{bhargavan_et_al:LIPIcs:2017:7119,
author = {Karthikeyan Bhargavan and Barry Bond and Antoine Delignat-Lavaud and C{\'e}dric Fournet and Chris Hawblitzel and Catalin Hritcu and Samin Ishtiaq and Markulf Kohlweiss and Rustan Leino and Jay Lorch and Kenji Maillard and Jianyang Pan and Bryan Parno and Jonathan Protzenko and Tahina Ramananandro and Ashay Rane and Aseem Rastogi and Nikhil Swamy and Laure Thompson and Peng Wang and Santiago Zanella-B{\'e}guelin and Jean-Karim Zinzindohou{\'e}},
title = {{Everest: Towards a Verified, Drop-in Replacement of HTTPS}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {1:1--1:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-032-3},
ISSN = {1868-8969},
year = {2017},
volume = {71},
editor = {Benjamin S. Lerner and Rastislav Bod{\'i}k and Shriram Krishnamurthi},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7119},
URN = {urn:nbn:de:0030-drops-71196},
doi = {10.4230/LIPIcs.SNAPL.2017.1},
annote = {Keywords: Security, Cryptography, Verification, TLS}
}
|
Keywords: |
|
Security, Cryptography, Verification, TLS |
|
Collection: |
|
2nd Summit on Advances in Programming Languages (SNAPL 2017) |
|
Issue Date: |
|
2017 |
|
Date of publication: |
|
05.05.2017 |
