# Not-quite-so-broken TLS in OCaml

*2014-01-01 — idea*


Status: Completed
Level: Any
Year: 2014
Project: Functional Internet Services
Supervisors: Anil Madhavapeddy, Peter Sewell
Students: Hannes Mehnert, David Kaloper-Mersinjak


Transport Layer Security (TLS) implementations have a history of security flaws. The immediate causes of these are often programming errors, e.g. in memory manage- ment, 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.

This internship was to work on nqsb-TLS, our re-engineered approach to security protocol specification and implementation that addresses the above root causes. The same source 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 (see [Unikernels](https://anil.recoil.org/projects/unikernels)) 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 achieved reasonable performance, with the same handshake performance as OpenSSL and 73%–84% for bulk throughput.

## Links

- [Hannes Mehnert](https://github.com/hannesm) and [David Kaloper-Mersinjak](https://github.com/pqwy) worked on this in an internship after discovering the MirageOS project online, and came over in the summer of 2014. The results have been hguely successful within the OCaml community, as the [ocaml-tls](https://github.com/mirleft/ocaml-tls) is still widely used as the defacto TLS stack in many popular OCaml applications.
- The paper was published in USENIX Security; see [Not-Quite-So-Broken TLS](https://anil.recoil.org/papers/2015-usenixsec-nqsb).
- For other stuff that happened during that internship period, see [Reviewing the second year of OCaml Labs in 2014](https://anil.recoil.org/notes/ocamllabs-2014-review).
  

## Related

- [An antibotty defensive testbed to protect network services](https://anil.recoil.org/ideas/antibotty-testbed) (idea, 2026-08-01)
  Available · MPhil
- [Not-Quite-So-Broken TLS](https://anil.recoil.org/papers/2015-usenixsec-nqsb) (paper, 2015-08-01)
  David Kaloper-Mersinjak, Hannes Mehnert et al. — 24th USENIX Security Symposium (USENIX Security 15)
- [Reviewing the second year of OCaml Labs in 2014](https://anil.recoil.org/notes/ocamllabs-2014-review) (note, 2015-04-02)
  Reviewing OCaml Labs' progress in 2014, covering tooling, compiler, community efforts, and research projects.
- [Unikernels](https://anil.recoil.org/projects/unikernels) (project, 2010-01-01)

---
Canonical: https://anil.recoil.org/ideas/nqsb-tls
Type: idea
License: CC BY 4.0 <https://creativecommons.org/licenses/by/4.0/>
Tags: security, mirageos, ocaml, tls, protocols