Transport Layer Security (TLS) is probably the most widely deployed security protocol on the Internet. It is used to setup virtual private networks, secure various services such as web and email, etc. For MirageOS, we developed a clean slate TLS implementation developed in OCaml. Our motivating goals are reliability, robustness, and API conciseness.
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);
- Difficulty in encoding state machines (OpenSSL change cipher suite attack, CVE-2014-0224).
OCaml as a trusty 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).
The OCaml runtime, 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.
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.
- Paper: Not-quite-so-broken TLS 1.3 mechanised conformance checking - Tron - Feb 2016
- Blog: Why OCaml TLS? - Jun 2015
- Paper: Transport layer security purely in OCaml - OCaml Meeting - Sep 2014
- Blog: OCaml-TLS - The protocol implementation and mitigations to known attacks - Jul 2014
- Blog: OCaml-TLS - Building the nocrypto library core - Jul 2014
- Blog: Introducing transport layer security (TLS) in pure OCaml - Jul 2014
- Not Quite So Broken TLS 1.3 - Tron - Feb 2016
- Not-So-Broken TLS: Re-engineering TLS in a Purely Functional Setting - LAMBDA World - Oct 2015
- Not-Quite-So-Broken TLS: Lessons in Re-engineering a Security Protocol Specification and Implementation - USENIX Security - Video- Aug 2015
- Nqsb-TLS - ARM Lunch 'n Learn - Jun 2015
- Safe TLS stack work - FMATS - Jun 2015
- Not-Quite-So-Broken TLS - HCSS - May 2015
- Lightning Talk on Nqsb-TLS - Real World Crypto - Jan 2015
- Trustworth Secure Modular Operating System Engineering - Video - CCC - Dec 2014
- MirageOS and OCaml TLS: Fun Operating System Engineering - IT Copenhagen - Sep 2014
- Transport Layer Security Purely in OCaml - OCaml Workshop 2014 - Sep 2014
0.7.1 March 2016
- remove camlp4 dependency (use cstruct ppx and sexplib ppx instead)
- sort client extensions, there are servers which dislike an extension without data at the end, thus try to send extensions with data at the end (#319)
- initial GCM support (#310)
- fix hs_can_handle_appdata (#315): Initially we allowed application data always after the first handshake.
Turns out, between CCS and Finished there is new crypto_context in place which has not yet been authenticated -- bad idea to accept application data at that point (beginning of 2015 in OCaml TLS).
The fix was to only allow application data in Established state (and block in Tls_lwt/Tls_mirage when the user requested renegotiation) (December 2015 in OCaml-TLS).
Renegotiation was also turned off by default when we introduced resumption (mid October 2015): both features together (without mitigating via session hash) allow the triple handshake.
It turns out, the server side can happily accept application data from the other side when it just sent a HelloRequest (and waits for the ClientHello; same is true for the client side, waiting for the ServerHello in renegotiation case might be interleaved with application data) to let the client initiate a new handshake. By this commit, OCaml-TLS allows application data then.
In the end, it is a pretty academic thing anyways, since nobody uses renegotiation with OCaml-TLS in the field.
during verification of a digitally signed: checked that the used hash algorithm is one of the configured ones (#313) unify return type of handshake and change cipher spec handler (#314) separate client and server extensions (#317) type equality (no longer generative error type), use result (#318) removed Printer (was barely useful)
0.7.0 December 2015
- session resumption (via session ID) support (#283) Config contains session_cache : SessionID.t -> epoch_data option and cached_session : epoch_data option
- session hash and extended master secret (RFC 7627) support (#287)
- semantic changes
- disable renegotiation by default (#300)
- blocking semantics (both Mirage and Lwt) while renegotiating (#304)
- Engine.handshake_in_progress no longer exist
- Hex_fingerprint /Fingerprint authenticators no longer exist
- Mirage X509 does no longer prefix keys and trust anchors with "tls/" in the path
- minor fixes
- fix concurrent read/write in tls_mirage (#303)
- expose own_random and peer_random in epoch_data (@cfcs, #297)
- public key pinning (X509_lwt) via Hex_key_fingerprint /Key_fingerprint (#301)
- certificate chain and peer certificate are exposed via epoch_data (new path-building X.509 interface)
0.6.0 July 2015
- API: dropped 'perfect' from forward secrecy in Config.Ciphers: fs instead of pfs, fs_of instead of pfs_of
- API: type epoch_data moved from Engine to Core
- removed Cstruct_s now that cstruct (since 1.6.0) provides s-expression marshalling
- require at least 1024 bit DH group, use FFDHE 2048 bit DH group by default instead of oakley2 (logjam)
- more specific alerts:
- UNRECOGNIZED_NAME: if hostname in SNI does not match
- UNSUPPORTED_EXTENSION: if server hello has an extension not present in client hello
- ILLEGAL_PARAMETER: if a parse error occured
- encrypt outgoing alerts
- fix off-by-one in handling empty TLS records: if a record is less than 5 bytes, treat as a fragment. exactly 5 bytes might already be a valid application data frame
0.5.0 May 2015
- updates to extension enum (contributed by Dave Garrett #264)
- removed entropy feeding (done by nocrypto) #265
- Tls_lwt file descriptor lifecycle: not eagerly close file descriptors #266
0.4.0 March 2015
- client authentication (both client and server side)
- server side SNI configuration (see sni.md)
- SCSV server-side downgrade prevention (by Gabriel de Perthuis @g2p #5)
- remove RC4 ciphers from default config #8
- support for AEAD ciphers, currently CCM #191
- proper bounds checking of handshake fragments #255
- disable application data between CCS and Finished #237
- remove secure renegotiation configuration option #256
- expose epoch in mirage interface, implement 2.3.0 API (error_message)
- error reporting (type failure in engine.mli) #246
- hook into Lwt event loop to feed RNG #254
0.3.0 December 2014
- X509_lwt provides Fingerprints andHex_fingerprints constructor for checking fingerprints of certificates instead of trusting trust anchors #206 #207
- client configuration requires an authenticator #202
- server certificate must be at least Config.min_rsa_key_size bits
- expose epoch via lwt interface #208
- mirage-2.2.0 compatibility #212
- cleanups of mirage interface #213
- nocrypto-0.3.0 compatibility #194 #209 #210
0.2.0 October 2014
- distinguish between supported hash and mac algorithms (using Nocrypto.Hash) and those which may occur on the wire #189
- expose trust anchor when authenticating certificate (requires x509 >=0.2) #178
- information about the active session is exposed via epoch : state -> epoch
- distinguish between supported ciphersuites (type ciphersuite) and known ciphersuites (type any_ciphersuite) #173
- distinguish between supported versions by the stack (type tls_version) and readable versions (tls_any_version), which might occur in a tls record or client_hello read from the network #179 #172
- support > TLS-1.2 client hellos (as reported by ssllabs.com #161)
- support iOS 6 devices (who propose NULL ciphers - reported in #160)
- send minimal protocol version in record layer of client hello (maximum version is in the client hello itself) (RFC5246, E.1) #165
0.1.0 July 2014
- initial beta release