Not-quite-so-broken TLS: Lessons in Re-engineering a Security Protocol Specification and Implementation

Presented as part of the 2015 HCSS conference.

Abstract:

Transport Layer Security (TLS) implementations have a history of security flaws.  The immediate causes of these range from simple programming errors, such as memory management, to subtle violations of the protocol logic.  Deeper causes can be seen in the challenges of interpreting the ambiguous prose specification, the complexities inherent in large APIs and code bases, unsafe performance-oriented programming choices, and the impossibility of directly testing conformance between implementations and the specification.

We present nqsb-TLS, the result of our re-engineering approach to improve the quality of security protocol implementations.  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 secure and usable executable implementation of TLS.  nqsb-TLS employs a modular and declarative programming style that also allows it to be compiled into a Xen unikernel (a specialised virtual machine image) with a TCB that is 2.5% of a standalone system running a standard Linux/OpenSSL stack, with all network traffic being handled in a memory-safe language.

nqsb-TLS focuses on protocol-level interoperability, and makes no effort to be compatible with existing (and often poorly designed) library APIs such as OpenSSL.  The higher-level API in nqsb-TLS makes it harder to misuse the library, and is demonstrated via several unikernel applications ranging over HTTPS, IMAP, Git, Websocket clients and servers.

This is joint work by David Kaloper Mersinjak, Anil Madhavapeddy, Hannes Mehnert and Peter Sewell.  It is funded in part by the EPSRC REMS grant (Rigorous Engineering of Mainstream Systems), EP/K008528/1.

Biography:

David Kaloper Mersinjak is a research assistant at the University of Cambridge. After studying at the University of Zagreb and working as a software developer, he started contributing to MirageOS and co-developed its TLS stack, eventually joining OCaml Labs. A functional programming enthusiast, his current interests include application of programming languages to trustworthy security engineering. David is living in Cambridge, UK.