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.

Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. Dijkstra monads for free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 515-529. ACM, January 2017. URL: https://www.fstar-lang.org/papers/dm4free/, URL: http://dx.doi.org/10.1145/3009837.3009878.
Daniel J. Bernstein. The Poly1305-AES message-authentication code. In International Workshop on Fast Software Encryption, pages 32-49. Springer, 2005.
Daniel J. Bernstein. Curve25519: new Diffie-Hellman speed records. In International Workshop on Public Key Cryptography, pages 207-228. Springer, 2006.
Daniel J Bernstein. The Salsa20 family of stream ciphers. In New stream cipher designs, pages 84-97. Springer, 2008.
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Cătălin Hriţcu, Jonathan Protzenko, Tahina Ramanandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella-Béguelin, and Jean Karim Zinzindohoué. Verified low-level programming embedded in F^⋆. Preprint, 2016. URL: https://arxiv.org/abs/1703.00053.
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, and Jean Karim Zinzindohoué. Implementing and proving the tls 1.3 record layer. Cryptology ePrint Archive, Report 2016/1178, 2016. URL: http://eprint.iacr.org/2016/1178.
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. Implementing TLS with verified cryptographic security. In 2013 IEEE Symposium on Security and Privacy, pages 445-459, 2013.
Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009.
Barry Bond, Chris Hawblitzel, Jay Lorch, Rustan Leino, Bryan Parno, Ashay Rane, and Laure Thompson. Verifying high-performance cryptographic assembly code. https://project-everest.github.io/papers/, 2016.
J. Clark and P. C. van Oorschot. SoK: SSL and HTTPS: Revisiting Past Challenges and Evaluating Certificate Trust Model Enhancements. In 2013 IEEE Symposium on Security and Privacy, pages 511-525, May 2013. URL: http://dx.doi.org/10.1109/SP.2013.41.
Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_24,
Martin Georgiev, Subodh Iyengar, Suman Jana, Rishita Anubhai, Dan Boneh, and Vitaly Shmatikov. The most dangerous code in the world: Validating ssl certificates in non-browser software. In Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS '12, pages 38-49, New York, NY, USA, 2012. ACM. URL: http://doi.acm.org/10.1145/2382196.2382204, URL: http://dx.doi.org/10.1145/2382196.2382204.
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. Certikos: An extensible architecture for building certified concurrent os kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI'16, pages 653-669, Berkeley, CA, USA, 2016. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=3026877.3026928.
Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI'14, pages 165-181, Berkeley, CA, USA, 2014. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=2685048.2685062.
David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. Not-quite-so-broken TLS: Lessons in re-engineering a security protocol specification and implementation. In 24th USENIX Security Symposium (USENIX Security 15), pages 223-238, 2015.
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP'09, pages 207-220, New York, NY, USA, 2009. ACM. URL: http://doi.acm.org/10.1145/1629575.1629596, URL: http://dx.doi.org/10.1145/1629575.1629596.
K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'10, pages 348-370, Berlin, Heidelberg, 2010. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1939141.1939161.
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009.
Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012. URL: http://hal.inria.fr/hal-00703441.
Pierre Letouzey. A new extraction for Coq. In Types for proofs and programs, pages 200-219. Springer, 2002.
Christopher Meyer and Jörg Schwenk. Sok: Lessons learned from ssl/tls attacks. In Revised Selected Papers of the 14th International Workshop on Information Security Applications - Volume 8267, WISA 2013, pages 189-209, New York, NY, USA, 2014. Springer-Verlag New York, Inc. URL: http://dx.doi.org/10.1007/978-3-319-05149-9_12,
Yoav Nir and Adam Langley. ChaCha20 and Poly1305 for IETF protocols. IETF RFC 7539, 2015.
Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram Rajamani, Sanjit A. Seshia, and Kapil Vaswani. A design and verification methodology for secure isolated regions. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '16, pages 665-681, New York, NY, USA, 2016. ACM. URL: http://doi.acm.org/10.1145/2908080.2908113, URL: http://dx.doi.org/10.1145/2908080.2908113.
The Sodium crypto library (libsodium). URL: https://www.gitbook.com/book/jedisct1/libsodium/details.
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256-270. ACM, 2016. URL: https://www.fstar-lang.org/papers/mumon/.
Jean Karim Zinzindohoué, Evmorfia-Iro Bartzia, and Karthikeyan Bhargavan. A verified extensible library of elliptic curves. In IEEE Computer Security Foundations Symposium (CSF), 2016.

Everest: Towards a Verified, Drop-in Replacement of HTTPS

File

Document Identifiers

Author Details

Cite AsGet BibTex

Abstract

Keywords

Metrics

References

Thanks for your feedback!

Could not send message