skip to main content
10.1145/2993600.2996279acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
invited-talk

Verified Secure Implementations for the HTTPS Ecosystem: Invited Talk

Published: 24 October 2016 Publication History

Abstract

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.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security
October 2016
116 pages
ISBN:9781450345743
DOI:10.1145/2993600
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2016

Check for updates

Author Tags

  1. HTTPs
  2. TLS
  3. Z3
  4. cryptography
  5. dafny
  6. fstar
  7. lean
  8. protocol
  9. security
  10. verification

Qualifiers

  • Invited-talk

Conference

CCS'16
Sponsor:

Acceptance Rates

PLAS '16 Paper Acceptance Rate 6 of 11 submissions, 55%;
Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 146
    Total Downloads
  • Downloads (Last 12 months)9
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media