@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: /usr/bin/bib2bib -c topic:"TLS" -ob topic.TLS.bib sewellbib2.bib}}
  author = {David Kaloper{-}Mersinjak 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},
  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 \emph{nqsb-TLS}, the result of our re-engineered approach to security protocol specification and implementation that addresses these root causes.  The same code serves dual 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 applications, which we demonstrate with a messaging client, and can also be compiled into a Xen unikernel (a specialised virtual machine image) with a 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.
  conf = {USENIX Security 2015},
  booktitle = {24th {USENIX} Security Symposium,  Washington,
               D.C., USA},
  pages = {223--238},
  year = {2015},
  month = aug,
  optcrossref = {DBLP:conf/uss/2015},
  url = {},
  project = {},
  pdf = {},
  timestamp = {Thu, 20 Aug 2015 14:07:40 +0200},
  biburl = {},
  bibsource = {dblp computer science bibliography,},
  topic = {TLS}