hannes.robur.coop/Posts/EC

---
title: Cryptography updates in OCaml and MirageOS
author: hannes
tags: mirageos, security, tls
abstract: Elliptic curves (ECDSA/ECDH) are supported in a maintainable and secure way.
---

## Introduction

Tl;DR: mirage-crypto-ec, with x509 0.12.0, and tls 0.13.0, provide fast and secure elliptic curve support in OCaml and MirageOS - using the verified [fiat-crypto](https://github.com/mit-plv/fiat-crypto/) stack (Coq to OCaml to executable which generates C code that is interfaced by OCaml). In x509, a long standing issue (countryName encoding), and archive (PKCS 12) format is now supported, in addition to EC keys. In tls, ECDH key exchanges are supported, and ECDSA and EdDSA certificates.

## Elliptic curve cryptography

[Since May 2020](https://mirage.io/blog/tls-1-3-mirageos), our [OCaml-TLS](https://usenix15.nqsb.io) stack supports TLS 1.3 (since tls version 0.12.0 on opam).

TLS 1.3 requires elliptic curve cryptography - which was not available in [mirage-crypto](https://github.com/mirage/mirage-crypto) (the maintained fork of [nocrypto](https://github.com/mirleft/ocaml-nocrypto)).

There are two major uses of elliptic curves: [key exchange (ECDH)](https://en.wikipedia.org/wiki/Elliptic-curve_Diffie%E2%80%93Hellman) for establishing a shared secret over an insecure channel, and [digital signature (ECDSA)](https://en.wikipedia.org/wiki/Elliptic_Curve_Digital_Signature_Algorithm) for authentication, integrity, and non-repudiation. (Please note that the construction of digital signatures on Edwards curves (Curve25519, Ed448) is called EdDSA instead of ECDSA.)

Elliptic curve cryptoraphy is [vulnerable](https://eprint.iacr.org/2020/615) [to](https://raccoon-attack.com/) [various](https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2018-5407) [timing](https://github.com/mimoo/timing_attack_ecdsa_tls) [attacks](https://minerva.crocs.fi.muni.cz/) - have a read of the [overview article on ECDSA](https://blog.trailofbits.com/2020/06/11/ecdsa-handle-with-care/). When implementing elliptic curve cryptography, it is best to avoid these known attacks. Gladly, there are some projects which address these issues by construction.

In addition, to use the code in MirageOS, it should be boring C code: no heap allocations, only using a very small amount of C library functions -- the code needs to be compiled in an environment with [nolibc](https://github.com/mirage/ocaml-freestanding/tree/v0.6.4/nolibc).

Two projects started in semantics, to solve the issue from the grounds up: [fiat-crypto](https://github.com/mit-plv/fiat-crypto/) and [hacl-star](https://github.com/project-everest/hacl-star/): their approach is to use a proof system ([Coq](https://coq.inria.fr) or [F*](https://www.fstar-lang.org/) to verify that the code executes in constant time, not depending on data input. Both projects provide as output of their proof systems C code.

For our initial TLS 1.3 stack, [Clément](https://github.com/pascutto/), [Nathan](https://github.com/NathanReb/) and [Etienne](https://github.com/emillon/) developed [fiat-p256](https://github.com/mirage/fiat) and [hacl_x5519](https://github.com/mirage/hacl). Both were one-shot interfaces for a narrow use case (ECDH for NIST P-256 and X25519), worked well for their purpose, and allowed to gather some experience from the development side.

### Changed requirements

Revisiting our cryptography stack with the elliptic curve perspective had several reasons, on the one side the customer project [NetHSM](https://www.nitrokey.com/products/nethsm) asked for feasibility of ECDSA/EdDSA for various elliptic curves, on the other side [DNSSec](https://github.com/mirage/ocaml-dns/pull/251) uses elliptic curve cryptography (ECDSA), and also [wireguard](https://www.wireguard.com/) relies on elliptic curve cryptography. The number of X.509 certificates using elliptic curves is increasing, and we don't want to leave our TLS stack in a state where it can barely talk to a growing number of services on the Internet.

Looking at [*hacl-star*](https://github.com/project-everest/hacl-star/), their [support](https://hacl-star.github.io/Supported.html) is limited to P-256 and Curve25519, any new curve requires writing F*. Another issue with hacl-star is C code quality: their C code does neither [compile with older C compilers (found on Oracle Linux 7 / CentOS 7)](https://github.com/mirage/hacl/issues/46), nor when enabling all warnings (> 150 are generated). We consider the C compiler as useful resource to figure out undefined behaviour (and other problems), and when shipping C code we ensure that it compiles with `-Wall -Wextra -Wpedantic --std=c99 -Werror`. The hacl project [ships](https://github.com/mirage/hacl/tree/master/src/kremlin) a bunch of header files and helper functions to work on all platforms, which is a clunky `ifdef` desert. The hacl approach is to generate a whole algorithm solution: from arithmetic primitives, group operations, up to cryptographic protocol - everything included.

In contrast, [*fiat-crypto*](https://github.com/mit-plv/fiat-crypto/) is a Coq development, which as part of compilation (proof verification) generates executables (via OCaml code extraction from Coq). These executables are used to generate modular arithmetic (as C code) given a curve description. The [generated C code](https://github.com/mirage/mirage-crypto/tree/main/ec/native) is highly portable, independent of platform (word size is taken as input) - it only requires a `<stdint.h>`, and compiles with all warnings enabled (once [a minor PR](https://github.com/mit-plv/fiat-crypto/pull/906) got merged). Supporting a new curve is simple: generate the arithmetic code using fiat-crypto with the new curve description. The downside is that group operations and protocol needs to implemented elsewhere (and is not part of the proven code) - gladly this is pretty straightforward to do, especially in high-level languages.

### Working with fiat-crypto

As mentioned, our initial [fiat-p256](https://github.com/mirage/fiat) binding provided ECDH for the NIST P-256 curve. Also, BoringSSL uses fiat-crypto for ECDH, and developed the code for group operations and cryptographic protocol on top of it.

The work needed was (a) ECDSA support and (b) supporting more curves (let's focus on NIST curves). For ECDSA, the algorithm requires modular arithmetics in the field of the group order (in addition to the prime). We generate these primitives with fiat-crypto (named `npYYY_AA`) - that required [a small fix in decoding hex](https://github.com/mit-plv/fiat-crypto/commit/e31a36d5f1b20134e67ccc5339d88f0ff3cb0f86). Fiat-crypto also provides inversion [since late October 2020](https://github.com/mit-plv/fiat-crypto/pull/670), [paper](https://eprint.iacr.org/2021/549) - which allowed to reduce our code base taken from BoringSSL. The ECDSA protocol was easy to implement in OCaml using the generated arithmetics.

Addressing the issue of more curves was also easy to achieve, the C code (group operations) are macros that are instantiated for each curve - the OCaml code are functors that are applied with each curve description.

Thanks to the test vectors (as structured data) from [wycheproof](https://github.com/google/wycheproof/) (and again thanks to Etienne, Nathan, and Clément for their OCaml code decodin them), I feel confident that our elliptic curve code works as desired.

What was left is X25519 and Ed25519 - dropping the hacl dependency entirely felt appealing (less C code to maintain from fewer projects). This turned out to require more C code, which we took from BoringSSL. It may be desirable to reduce the imported C code, or to wait until a project on top of fiat-crypto which provides proven cryptographic protocols is in a usable state.

To avoid performance degradation, I distilled some [X25519 benchmarks](https://github.com/mirage/mirage-crypto/pull/107#issuecomment-799701703), turns out the fiat-crypto and hacl performance is very similar.

### Achievements

The new opam package [mirage-crypto-ec](https://mirage.github.io/mirage-crypto/doc/mirage-crypto-ec/Mirage_crypto_ec/index.html) is released, which includes the C code generated by fiat-crypto (including [inversion](https://github.com/mit-plv/fiat-crypto/pull/670)), [point operations](https://github.com/mirage/mirage-crypto/blob/main/ec/native/point_operations.h) from BoringSSL, and some [OCaml code](https://github.com/mirage/mirage-crypto/blob/main/ec/mirage_crypto_ec.ml) for invoking these functions and doing bounds checks, and whether points are on the curve. The OCaml code are some functors that take the curve description (consisting of parameters, C function names, byte length of value) and provide Diffie-Hellman (Dh) and digital signature algorithm (Dsa) modules. The nonce for ECDSA is computed deterministically, as suggested by [RFC 6979](https://tools.ietf.org/html/rfc6979), to avoid private key leakage.

The code has been developed in [NIST curves](https://github.com/mirage/mirage-crypto/pull/101), [removing blinding](https://github.com/mirage/mirage-crypto/pull/106) (since we use operations that are verified to be constant-time), [added missing length checks](https://github.com/mirage/mirage-crypto/pull/108) (reported by [Greg](https://github.com/greg42)), [curve25519](https://github.com/mirage/mirage-crypto/pull/107), [a fix for signatures that do not span the entire byte size (discovered while adapting X.509)](https://github.com/mirage/mirage-crypto/pull/117), [fix X25519 when the input has offset <> 0](https://github.com/mirage/mirage-crypto/pull/118). It works on x86 and arm, both 32 and 64 bit (checked by CI). The development was partially sponsored by Nitrokey.

What is left to do, apart from further security reviews, is [performance improvements](https://github.com/mirage/mirage-crypto/issues/109), [Ed448/X448 support](https://github.com/mirage/mirage-crypto/issues/112), and [investigating deterministic k for P521](https://github.com/mirage/mirage-crypto/issues/105). Pull requests are welcome.

When you use the code, and encounter any issues, please [report them](https://github.com/mirage/mirage-crypto/issues).

## Layer up - X.509 now with ECDSA / EdDSA and PKCS 12 support, and a long-standing issue fixed

With the sign and verify primitives, the next step is to interoperate with other tools that generate and use these public and private keys. This consists of serialisation to and deserialisation from common data formats (ASN.1 DER and PEM encoding), and support for handling X.509 certificates with elliptic curve keys. Since X.509 0.12.0, it supports EC private and public keys, including certificate validation and issuance.

Releasing X.509 also included to go through the issue tracker and attempt to solve the existing issues. This time, the ["country name is encoded as UTF8String, while RFC demands PrintableString"](https://github.com/mirleft/ocaml-x509/issues/69) filed more than 5 years ago by [Reynir](https://github.com/reynir), re-reported by [Petter](https://github.com/paurkedal) in early 2017, and again by [Vadim](https://github.com/NightBlues) in late 2020, [was fixed by Vadim](https://github.com/mirleft/ocaml-x509/pull/140).

Another long-standing pull request was support for [PKCS 12](https://tools.ietf.org/html/rfc7292), the archive format for certificate and private key bundles. This has [been developed and merged](https://github.com/mirleft/ocaml-x509/pull/114). PKCS 12 is a widely used and old format (e.g. when importing / exporting cryptographic material in your browser, used by OpenVPN, ...). Its specification uses RC2 and 3DES (see [this nice article](https://unmitigatedrisk.com/?p=654)), which are the default algorithms used by `openssl pkcs12`.

## One more layer up - TLS

In TLS we are finally able to use ECDSA (and EdDSA) certificates and private keys, this resulted in slightly more complex configuration - the constraints between supported groups, signature algorithms, ciphersuite, and certificates are intricate:

The ciphersuite (in TLS before 1.3) specifies which key exchange mechanism to use, but also which signature algorithm to use (RSA/ECDSA). The supported groups client hello extension specifies which elliptic curves are supported by the client. The signature algorithm hello extension (TLS 1.2 and above) specifies the signature algorithm. In the end, at load time the TLS configuration is validated and groups, ciphersuites, and signature algorithms are condensed depending on configured server certificates. At session initiation time, once the client reports what it supports, these parameters are further cut down to eventually find some suitable cryptographic parameters for this session.

From the user perspective, earlier the certificate bundle and private key was a pair of `X509.Certificate.t list` and `Mirage_crypto_pk.Rsa.priv`, now the second part is a `X509.Private_key.t` - all provided constructors have been updates (notably `X509_lwt.private_of_pems` and `Tls_mirage.X509.certificate`).

## Finally, conduit and mirage

Thanks to [Romain](https://github.com/dinosaure), conduit* 4.0.0 was released which supports the modified API of X.509 and TLS. Romain also developed patches and released mirage 3.10.3 which supports the above mentioned work.

## Conclusion

Elliptic curve cryptography is now available in OCaml using verified cryptographic primitives from the fiat-crypto project - `opam install mirage-crypto-ec`. X.509 since 0.12.0 and TLS since 0.13.0 and MirageOS since 3.10.3 support this new development which gives rise to smaller EC keys. Our old bindings, fiat-p256 and hacl_x25519 have been archived and will no longer be maintained.

Thanks to everyone involved on this journey: reporting issues, sponsoring parts of the work, helping with integration, developing initial prototypes, and keep motivating me to continue this until the release is done.

In the future, it may be possible to remove zarith and gmp from the dependency chain, and provide EC-only TLS servers and clients for MirageOS. The benefit will be much less C code (libgmp-freestanding.a is 1.5MB in size) in our trusted code base.

Another potential project that is very close now is a certificate authority developed in MirageOS - now that EC keys, PKCS 12, revocation lists, ... are implemented.

## Footer

If you want to support our work on MirageOS unikernels, please [donate to robur](https://robur.coop/Donate). I'm interested in feedback, either via [twitter](https://twitter.com/h4nnes), [hannesm@mastodon.social](https://mastodon.social/@hannesm) or via eMail.