Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-Located Workshops
  • Program
    • At a Glance
    • Technical Sessions
    • Poster Session
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
    • WiPs
  • Participate
    • Call for Papers
      • Important Dates
      • Symposium Organizers
      • Symposium Topics
      • Refereed Papers
      • Shadow PC
      • Symposium Activities
      • Submitting Papers
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Services
    • Questions
    • Help Promote!
    • Past Symposia
  • Home
  • Attend
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-Located Workshops
  • Program
  • Activities
  • Participate
    • Call for Papers
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Services
    • Questions
    • Help Promote!
    • Past Symposia

sponsors

Platinum Sponsor
Gold Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
General Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner
Industry Partner

help promote

USENIX Security '16 button

Get more
Help Promote graphics!

connect with usenix


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by USENIXSecurity

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation
Tweet

connect with us

Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation

Authors: 

David Kaloper-Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell, University of Cambridge

Abstract: 

Transport Layer Security (TLS) implementations have a history of security flaws. The immediate causes of these are often programming errors, e.g. in memory management, but the root causes are more fundamental: the challenges of interpreting the ambiguous prose specification, the complexities inherent in large APIs and code bases, inherently unsafe programming choices, and the impossibility of directly testing conformance between implementations and the specification.

We present nqsb-TLS, the result of our re-engineered approach to security protocol specification and implementation that addresses these root causes. The same code serves two roles: it is both a specification of TLS, executable as a test oracle to check conformance of traces from arbitrary implementations, and a usable implementation of TLS; a modular and declarative programming style provides clean separation between its components. Many security flaws are thus excluded by construction.

nqsb-TLS can be used in standalone Unix applications, which we demonstrate with a messaging client, and can also be compiled into Xen unikernels (specialised virtual machine image) with a trusted computing base (TCB) that is 4% of a standalone system running a standard Linux/OpenSSL stack, with all network traffic being handled in a memory-safe language; this supports applications including HTTPS, IMAP, Git, and Websocket clients and servers. Despite the dual-role design, the high-level implementation style, and the functional programming language we still achieve reasonable performance, with the same handshake performance as OpenSSL and 73% – 84% for bulk throughput.

David Kaloper-Meršinjak, University of Cambridge

Hannes Mehnert, University of Cambridge

Anil Madhavapeddy, University of Cambridge

Peter Sewell, University of Cambridge

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {190896,
author = {David Kaloper-Mer{\v s}injak and Hannes Mehnert and Anil Madhavapeddy and Peter Sewell},
title = {{Not-Quite-So-Broken} {TLS}: Lessons in {Re-Engineering} a Security Protocol Specification and Implementation},
booktitle = {24th USENIX Security Symposium (USENIX Security 15)},
year = {2015},
isbn = {978-1-939133-11-3},
address = {Washington, D.C.},
pages = {223--238},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak},
publisher = {USENIX Association},
month = aug,
}
Download
Kaloper-Mersinjak PDF
View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

  • Log in or    Register to post comments

Open access to the USENIX Security '15 videos sponsored by Symantec.

Platinum Sponsors

Gold Sponsors

Silver Sponsors

Bronze Sponsors

General Sponsors

Media Sponsors & Industry Partners

Open Access Publishing Partner

© USENIX

  • Privacy Policy
  • Contact Us