From 847d8f36f22dc1cc2e40bb85d25f05d7601e8347 Mon Sep 17 00:00:00 2001 From: Hannes Mehnert Date: Mon, 19 Jul 2021 14:55:51 +0200 Subject: [PATCH] fiat-crypto is really fiat-crypto, not fiat --- Posts/EC | 20 ++++++++++---------- Posts/NGI | 2 +- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Posts/EC b/Posts/EC index 56fa70d..68aef62 100644 --- a/Posts/EC +++ b/Posts/EC @@ -7,7 +7,7 @@ abstract: Elliptic curves (ECDSA/ECDH) are supported in a maintainable and secur ## 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](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. +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 @@ -21,7 +21,7 @@ Elliptic curve cryptoraphy is [vulnerable](https://eprint.iacr.org/2020/615) [to 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](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. +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. @@ -31,25 +31,25 @@ Revisiting our cryptography stack with the elliptic curve perspective had severa 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*](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 ``, 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 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. +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 ``, 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 +### 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 for ECDH, and developed the code for group operations and cryptographic protocol on top of it. +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 (named `npYYY_AA`) - that required [a small fix in decoding hex](https://github.com/mit-plv/fiat-crypto/commit/e31a36d5f1b20134e67ccc5339d88f0ff3cb0f86). Fiat 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. +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 which provides proven cryptographic protocols is in a usable state. +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 and hacl performance is very similar. +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 (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 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. @@ -79,7 +79,7 @@ Thanks to [Romain](https://github.com/dinosaure), conduit* 4.0.0 was released wh ## Conclusion -Elliptic curve cryptography is now available in OCaml using verified cryptographic primitives from the fiat 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. +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. diff --git a/Posts/NGI b/Posts/NGI index 6e7ec3b..b38e3ec 100644 --- a/Posts/NGI +++ b/Posts/NGI @@ -25,7 +25,7 @@ Here is a very subjective random collection of accomplishments in 2020, where I ### TLS 1.3 -Dating back to 2016, at the [TRON](https://www.ndss-symposium.org/ndss2016/tron-workshop-programme/) (TLS 1.3 Ready or NOt), we developed a first draft of a 1.3 implementation of [OCaml-TLS](https://github.com/mirleft/ocaml-tls). Finally in May 2020 we got our act together, including ECC (ECDH P256 from [fiat](https://github.com/mit-plv/fiat-crypto/), X25519 from [hacl](https://project-everest.github.io/)) and testing with [tlsfuzzer](https://github.com/tlsfuzzer/tlsfuzzer), and release tls 0.12.0 with TLS 1.3 support. Later we added [ECC ciphersuites to TLS version 1.2](https://github.com/mirleft/ocaml-tls/pull/414), implemented [ChaCha20/Poly1305](https://github.com/mirleft/ocaml-tls/pull/414), and fixed an [interoperability issue with Go's implementation](https://github.com/mirleft/ocaml-tls/pull/424). +Dating back to 2016, at the [TRON](https://www.ndss-symposium.org/ndss2016/tron-workshop-programme/) (TLS 1.3 Ready or NOt), we developed a first draft of a 1.3 implementation of [OCaml-TLS](https://github.com/mirleft/ocaml-tls). Finally in May 2020 we got our act together, including ECC (ECDH P256 from [fiat-crypto](https://github.com/mit-plv/fiat-crypto/), X25519 from [hacl](https://project-everest.github.io/)) and testing with [tlsfuzzer](https://github.com/tlsfuzzer/tlsfuzzer), and release tls 0.12.0 with TLS 1.3 support. Later we added [ECC ciphersuites to TLS version 1.2](https://github.com/mirleft/ocaml-tls/pull/414), implemented [ChaCha20/Poly1305](https://github.com/mirleft/ocaml-tls/pull/414), and fixed an [interoperability issue with Go's implementation](https://github.com/mirleft/ocaml-tls/pull/424). [Mirage-crypto](https://github.com/mirage/mirage-crypto) provides the underlying cryptographic primitives, initially released in March 2020 as a fork of [nocrypto](https://github.com/mirleft/ocaml-nocrypto) -- huge thanks to [pqwy](https://github.com/pqwy) for his great work. Mirage-crypto detects [CPU features at runtime](https://github.com/mirage/mirage-crypto/pull/53) (thanks to [Julow](https://github.com/Julow)) ([bugfix for bswap](https://github.com/mirage/mirage-crypto/pull/96)), using constant time modular exponentation (powm_sec) and hardens against Lenstra's CRT attack, supports [compilation on Windows](https://github.com/mirage/mirage-crypto/pull/39) (thanks to [avsm](https://github.com/avsm)), [async entropy harvesting](https://github.com/mirage/mirage-crypto/pull/90) (thanks to [seliopou](https://github.com/seliopou)), [32 bit support](https://github.com/mirage/mirage-crypto/pull/65), [chacha20/poly1305](https://github.com/mirage/mirage-crypto/pull/72) (thanks to [abeaumont](https://github.com/abeaumont)), [cross-compilation](https://github.com/mirage/mirage-crypto/pull/84) (thanks to [EduardoRFS](https://github.com/EduardoRFS)) and [various](https://github.com/mirage/mirage-crypto/pull/78) [bug](https://github.com/mirage/mirage-crypto/pull/81) [fixes](https://github.com/mirage/mirage-crypto/pull/83), even [memory leak](https://github.com/mirage/mirage-crypto/pull/95) (thanks to [talex5](https://github.com/talex5) for reporting several of these issues), and [RSA](https://github.com/mirage/mirage-crypto/pull/99) [interoperability](https://github.com/mirage/mirage-crypto/pull/100) (thanks to [psafont](https://github.com/psafont) for investigation and [mattjbray](https://github.com/mattjbray) for reporting). This library feels very mature now - being used by multiple stakeholders, and lots of issues have been fixed in 2020.