Today, we announce the first release of the HACL Packages libraries. 🎉

This release of HACL packages includes the first release of the HACL C library and a new release of the hacl-star OCaml bindings.

Together with this first release of the C library, we publish a first, work in progress, version of the documentation for the library. The HACL Packages documentation is the main entry point for all information about the HACL Packages.

Please file an issue or open a discussion if you have trouble with anything in this tutorial.

If you use cryptography anywhere, we’d be happy if you used HACL and told us if it’s working for you or (why) not. And get in touch if you have any questions about high assurance cryptography in general or the HACL library in particular.

Note that while this release can be used in production, there are a number of breaking changes coming up before the first stable 1.0 release.

Getting started

To start using HACL Packages, we first need to set up a new project and make HACL Packages a dependency. Let’s start by creating a hacl-packages-example folder by executing …

mkdir hacl-packages-example

We will place our main.c file into this folder later. Now, clone the HACL Packages repository …

git clone https://github.com/cryspen/hacl-packages.git

… and change into it …

cd hacl-packages

The HACL Packages README already tells you how to build and test the package. However, in this blog post, we want to show how to use the library in your project. Note that we choose only to use a single algorithm and not build the entire library. To keep this post short, let’s assume we want to use BLAKE2B.

We need to set up some build dependencies first. Specifically, we need cmake, ninja, python, and a compiler (gcc or clang). Please see the Install build dependencies section in the HACL Packages README for instructions.

After we have installed the build dependencies, we can build the BLAKE2B HACL Packages part with …

./mach build -a blake2 --release

The -a flag lets us choose the algorithms we want to use. We also want to build in --release mode and not in --debug to get the best performance.

Now, to use HACL Packages in another project, we need the HACL Packages library and header files. You can copy everything yourself, but it is easier to use …

./mach install -p ../hacl-packages-example

… to let our “mach build system” do this for you. This command creates a lib and include folder in the example folder containing everything you need to work with HACL Packages. All changes are limited to the folder you specify with -p (or --prefix). However, you could also use a different prefix to globally install HACL Packages on your system.

We don’t need to come back to hacl-packages anymore. So, let’s switch to our example folder for the rest of this introduction …

cd ../hacl-packages-example

Now, “all you need to do” is to write code 😊 Let’s open the HACL Packages Documentation and navigate to the C API Reference of BLAKE2B.

The C API Reference for the HACL API documents different implementations of each algorithm. We tried to make this more accessible, but there is certainly work to be done. For now, you need to know that we are interested in the “32” variant of BLAKE2B. This implementation should run on any CPU and is thus suitable for an introduction. If you want to use HACL Packages in production, you should consider using the other implementations or use the EverCrypt provider that chooses the best implementation for you.

So, here is the code …

#include "Hacl_Hash_Blake2.h"

void print_hex_ln(size_t bytes_len, uint8_t *bytes);

int main() {
  // Reserve memory for a 64 byte digest, i.e.,
  // for a BLAKE2B run with full 512-bit output.
  uint32_t output_len = 64;
  uint8_t output[64];

  // The message we want to hash.
  const char *message = "Hello, HACL Packages!";
  uint32_t message_len = strlen(message);

  // BLAKE2B can be used as an HMAC, i.e., with a key.
  // We don't want to use a key here and thus provide a zero-sized key.
  uint32_t key_len = 0;
  uint8_t *key = 0;

  Hacl_Blake2b_32_blake2b(
    output_len,
    output,
    message_len,
    (uint8_t *)message,
    key_len, key
  );

  print_hex_ln(output_len, output);
}

void print_hex_ln(size_t bytes_len, uint8_t *bytes) {
  for (int i = 0; i < bytes_len; ++i) {
    printf("%02x", bytes[i]);
  }

  printf("\n");
}

Create a main.c file with the code above and run …

clang main.c -Iinclude -Iinclude/hacl lib/libhacl_static.a -o main

… to create a statically-linked executable called main.

In this case, the example hashes the byte sequence “Hello, HACL Packages!” into a BLAKE2B digest with 64 bytes. Thus, running …

./main

… should output …

f99574aa3ba6cf78ad48e1f22a77e7aef1d7433c1cb3d424d14ae5ec51af8c6dc8bf41cb0a10383274f256df0f7d0f145a043b7a77f4c17e47e535f72a4e1f43

Wait a second. How do we know this high-performance and formally verified implementation gives us the correct output? Let’s check against OpenSSL …

echo -n 'Hello, HACL Packages!' | openssl blake2b512

OCaml

The OCaml package has been around for a while but we want to show how to use it again here if you are new to HACL.

Before getting started the hacl-star package needs to be installed.

opam install hacl-star

Now we can use the same BLAKE2B hash function in OCaml.

open Hacl_star

let main =
  let msg = Bytes.of_string "Hello, HACL Packages!" in
  let digest = Hacl.Blake2b_32.hash msg 64 in
  Printf.printf "%s\n" (Hex.show (Hex.of_bytes digest));

We assume this was put into a file called blake2b_example.ml. We can build this file now as follows.

ocamlfind ocamlopt -o blake2b_ocaml -linkpkg -package hacl-star,Hex blake2b_example.ml

And run it as follows:

./blake2b_ocaml

The output should be the same as above.