(... to be written)

Sources

[ZBPB17] explains HACL* in detail. The underlying F*/Low* to C translation (with KreMLin) is explained in [B17]. HACL* is available on GitHub[HACL*] as is KreMLin[KreMLin]. The main application and motivation driving the design and implementation of HACL* is implementing and proving the TLS 1.3 Record Layer[B16], but HACL* can, of course, be used everywhere: it has a NaCl/libsodium like API.

Some people, not being fluent in ML/OCaml, don't like writing cryptographic specifications in F*/Low*. Project hacspec[hacspec] aims to create a Python-like language for specs that translates to cryptol, Coq, F*, EasyCrypt. It is in a very early stage though. A paper[BKS18] and slides outline this effort.

This crypto bite is inspired by Karthikeyan Bhargavan's talk "Verified Cryptographic Libraries", starting at 21:02, at the 8th BIU Winter School on Cryptography, Secure Key Exchange, February 11-15 2018 (all videos).

and the followup talk "Verified Cryptographic Protocol Implementations":

A similar presentation on Low* is "Verified Low-Level Programming Embedded in F*" [B17]:

Literature

• [HACL*] HACL*: High-Assurance Crypto Library, on GitHub
• [KreMLin] KreMLin: An F*/Low* to C Extractor on GitHub
• [hacspec] Project hacspec on GitHub
• [ZBPB17] Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche: HACL*: A Verified Modern Cryptographic Library. (iacr.org 2017/536, full pdf)
• [B17] Karthikeyan Bhargavan et al.: Verified Low-Level Programming Embedded in F*. (full pdf, newer version)
• [B16] Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Karim Zinzindohoué: Implementing and Proving the TLS 1.3 Record Layer. (iacr.org 2016/1178, full pdf)
• [BKS18] Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub: hacspec, towards verifiable crypto standards. slides.