URL
BibTeX
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 imple- mentation 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 de- sign, 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.
Authors. David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy and Peter Sewell
See Also. This publication was part of my Unikernels project.
News Updates
» Delivered the distinguished seminar series at St Andrews on rebuilding Operating Systems with functional principles / «» Part 2 / «» Part 3.» DockerCon talk on unikernels and MirageOS.» Interviewed by The New Stack at OSCON in Austin, Texas / «
» Updated the MirageOS community about the 2016 hack retreat.» Announced HyperKit, VPNKit and DataKit for the Docker ecosystem.» Announced that Unikernel Systems is now part of Docker.» Invited talk at NetPL on Immutable Distributed Infrastructure with Unikernels.» Paper on rebuilding TLS securely but practically at USENIX Security 2015.» Talk at Esper on functional programming with unikernels.» Updated the OCaml community on annual OCaml Labs activities for 2014.» Gave BOB 2015 keynote on functional Operating Systems.» New Directions in Operating Systems talk on Jitsu.» At the Xen Summit speaking about branch consistency for Xen Stub Domains.» Gave Haskell Symposium 2014 Keynote on functional OS design.» Announced the release of MirageOS 1.2, and a roadmap towards MirageOS 2.0 / «» Announced the long-awaited release of MirageOS 2.0 / «» Appeared on FLOSS Weekly 302 about Open Mirage.» Appeared on SE Radio Episode 204 about Mirage and OCaml.» Note on the discussions around my recent CACM article on unikernels.» MirageOS and XAPI project update at XenSummit / «» Note on integrating Docker and opam more effectively.» Mirage Developer Preview 1 screencast.» Discussing how we disaggregated MirageOS into opam packages.» Note on how to build XenStore stub domains using MirageOS.» Note on using ARM Dreamplugs with OCaml published.» At the OCaml Meeting 2011 speaking about MirageOS.» Liveblog on the talks at CUFP 2011.» Note discussing an OCaml interface to our new CIEL dataflow engine / «» Published a note on delimited continuations vs Lwt in OCaml for MirageOS.» Announced that the MirageOS website now self-hosted on MirageOS! / «» At LinkedIn giving tech talk about Mirage.» At HotCloud for the first talk about MirageOS.