What is TLS?

Transport Layer Security (TLS) is probably the most widely deployed security protocol on the Internet. It provides communication privacy to prevent eavesdropping, tampering, and message forgery. Furthermore, it optionally provides authentication of the involved endpoints. TLS is commonly deployed for securing web services (HTTPS), emails, virtual private networks, and wireless networks.

TLS uses asymmetric cryptography to exchange a symmetric key, and optionally authenticate (using X.509) either or both endpoints. It provides algorithmic agility, which means that the key exchange method, symmetric encryption algorithm, and hash algorithm are negotiated.

TLS in OCaml

Our implementation ocaml-tls is already able to interoperate with existing TLS implementations, and supports several important TLS extensions such as server name indication (RFC4366, enabling virtual hosting) and secure renegotiation (RFC5746).

Our demonstration server runs ocaml-tls and renders exchanged TLS messages in nearly real time by receiving a trace of the TLS session setup. If you encounter any problems, please give us feedback.

ocaml-tls and all dependent libraries are available via OPAM (opam install tls). The source is available under a BSD license. We are primarily working towards completeness of protocol features, such as client authentication, session resumption, elliptic curve and GCM cipher suites, and have not yet optimised for performance.

ocaml-tls depends on the following independent libraries: ocaml-nocrypto implements the cryptographic primitives, ocaml-asn1-combinators provides ASN.1 parsers/unparsers, and ocaml-x509 implements the X509 grammar and certificate validation (RFC5280). ocaml-tls implements TLS (1.0 RFC2246, 1.1 RFC4346, and 1.2 RFC5246).

We invite the community to audit and run our code, and we are particularly interested in discussion of our APIs. Please use the mirage-devel mailing list for discussions.

Please be aware that this software is beta and is missing external code audits. It is not yet intended for use in any security critical applications.

In our issue tracker we transparently document known attacks against TLS and our mitigations (checked and unchecked). We have not yet implemented mitigations against either the Lucky13 timing attack or traffic analysis (e.g. length-hiding padding).

You can read more about attacks and our mitigations. We also documented the design of ocaml-tls.

Trusted code base

Designed to run on Mirage, the trusted code base of ocaml-tls is small. It includes the libraries already mentioned, ocaml-tls, ocaml-asn1-combinators, ocaml-x509, and ocaml-nocrypto (which uses C implementations of block ciphers and hash algorithms). For arbitrary precision integers needed in asymmetric cryptography, we rely on zarith, which wraps libgmp. As underlying byte array structure we use cstruct (which uses OCaml Bigarray as storage).

We should also mention the OCaml runtime, the OCaml compiler, the operating system on which the source is compiled and the binary is executed, as well as the underlying hardware. Two effectful frontends for the pure TLS core are implemented, dealing with side-effects such as reading and writing from the network: Lwt_unix and Mirage, so applications can run directly as a Xen unikernel.

Why a new TLS implementation?

There are only a few TLS implementations publicly available and most programming languages bind to OpenSSL, an open source implementation written in C. There are valid reasons to interface with an existing TLS library, rather than developing one from scratch, including protocol complexity and compatibility with different TLS versions and implementations. But from our perspective the disadvantage of most existing libraries is that they are written in C, leading to:

• Memory safety issues, as recently observed by Heartbleed and GnuTLS session identifier memory corruption (CVE-2014-3466) bugs;
• Control flow complexity (Apple's goto fail, CVE-2014-1266);
• And difficulty in encoding state machines (OpenSSL change cipher suite attack, CVE-2014-0224).

Our main reasons for ocaml-tls are that OCaml is a modern functional language, which allows concise and declarative descriptions of the complex protocol logic and provides type safety and memory safety to help guard against programming errors. Its functional nature is extensively employed in our code: the core of the protocol is written in purely functional style, without any side effects.

---

Posts in the TLS series:

• Introducing transport layer security (TLS) in pure OCaml
• OCaml-TLS: building the nocrypto library core
• OCaml-TLS: adventures in X.509 certificate parsing and validation
• OCaml-TLS: ASN.1 and notation embedding
• OCaml-TLS: the protocol implementation and mitigations to known attacks

Implemented standards

• RFC 2246 - TLS Protocol version 1.0
• RFC 2818 - HTTP over TLS (notably wildcard domain names in X509 certificates)
• RFC 3268 - AES Ciphersuites for TLS
• RFC 4346 - TLS Protocol version 1.1
• RFC 4366 - TLS Extensions (notably Server Name Indication - SNI)
• RFC 5246 - TLS Protocol version 1.2
• RFC 5746 - TLS Renegotiation Indication Extension
• draft-agl-tls-padding-03 - A TLS padding extension
• draft-mathewson-no-gmtunixtime - No UNIX time in client and server hello

Acknowledgements

Since this is the final post in our series, we would like to thank all people who reported issues so far: Anil Madhavapeddy, Török Edwin, Daniel Bünzli, Andreas Bogk, Gregor Kopf, Graham Steel, Jerome Vouillon, Amir Chaudhry, Ashish Agarwal. Additionally, we want to thank the miTLS team (especially Cedric and Karthikeyan) for fruitful discussions, as well as the OCaml Labs and Mirage teams. And thanks to Peter Sewell and Richard Mortier for funding within the REMS, UCN, and Horizon projects. The software was started in Aftas beach house in Mirleft, Morocco.