Visible to the public Verified Secure Implementations for the HTTPS Ecosystem: Invited Talk

TitleVerified Secure Implementations for the HTTPS Ecosystem: Invited Talk
Publication TypeConference Paper
Year of Publication2016
AuthorsFournet, Cédric
Conference NameProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security
Date PublishedOctober 2016
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-4574-3
KeywordsCollaboration, compositionality, cryptography, dafny, fstar, HTTPs, lean, privacy, protocol, protocol verification, pubcrawl, security, TLS, verification, Z3

The HTTPS ecosystem, including the SSL/TLS protocol, the X.509 public-key infrastructure, and their cryptographic libraries, is the standardized foundation of Internet Security. Despite 20 years of progress and extensions, however, its practical security remains controversial, as witnessed by recent efforts to improve its design and implementations, as well as recent disclosures of attacks against its deployments. The Everest project is a collaboration between Microsoft Research, INRIA, and the community at large that aims at modelling, programming, and verifying the main HTTPS components with strong machine-checked security guarantees, down to core system and cryptographic assumptions. Although HTTPS involves a relatively small amount of code, it requires efficient low-level programming and intricate proofs of functional correctness and security. To this end, we are also improving our verifications tools (F*, Dafny, Lean, Z3) and developing new ones. In my talk, I will present our project, review our experience with miTLS, a verified reference implementation of TLS coded in F*, and describe current work towards verified, secure, efficient HTTPS.

Citation Keyfournet_verified_2016