Using the crypto library

Picking a distribution

Building the full hacl-star repository verifies the source F* and Vale code, then proceeds to extract it to C and assembly. However, users do not have to use this full build process: we provide the generated code in the dist/ directory, under version control to facilitate obtaining the source code.

Each subdirectory corresponds to a distribution, i.e. a particular set of options passed to KreMLin (the F*-to-C compiler) that influence how the generated C code looks like.

There is a total order on distributions: c89-compatible <= msvc-compatible <= gcc-compatible <= gcc64-only

  • The C89 distribution will work with the most C compilers; it relies on alloca; eliminates compound literals and enforces C89 scope to generate syntactically C89-compliant code; code still relies on inttypes.h and other headers that you may have to provide depending on your target. It does not include Merkle Trees and the code is incredibly verbose.
  • The MSVC distribution relies on alloca to avoid C11 VLA for the sake of MSVC; relies on KreMLin for tail-call optimizations. It also does not use GCC inline assembly for Curve25519 and uses external linkage instead.
  • The GCC distribution relies on C11 VLA and therefore does not work with MSVC.
  • The GCC64 distribution assumes a native unsigned __int128 type which can be manipulated via the standard arithmetic operators. This generates very compact code but only works on 64-bit GCC and Clang.

Other distributions are either for distinguished consumers of our code who need specific KreMLin compilation options (e.g. Mozilla, CCF) or for testing (e.g. portable-gcc-compatible, which compiles without -march=native, to ensure all our assumptions about CPU targets are explicit in our Makefile).

Compiling a full distribution

Each distribution comes with its own Makefile. It builds a static object (libevercrypt.a) and a dynamic object (libevercrypt.{so,dll}) along with the import library for Windows systems (libevercrypt.dll.a). On Windows, the Makefile has been tested in a Cygwin environment equipped with the MinGW cross-compilers. The dist/compact-msvc distribution works with the Microsoft compilers, but we provide no build support (i.e. no Visual Studio project, no NMake-compatible makefile).

Note

The gcc-compatible distribution also features OCaml bindings to our code. These require a valid OCaml setup, including packages ctypes, ctypes-foreign and bigstring, usually obtained via OPAM. You can easily disable building these bindings by removing the lib_gen directory in dist/gcc-compatible.

Integrating the code

To incoroporate our verified crypto code into a C software project, a developer has two choices.

  • Pick a full EverCrypt distribution, along with the dist/kremlin directory, thus giving a “wholesale” integration of the EverCrypt library, including all supported algorithms from HACL* and Vale.
  • For a more selective integration, cherry-pick the C or assembly files for specific versions of specific algorithms. Each header file contains the list of other headers (and implementations) it depends on so it’s easy to integrate, say, an individual algorithm from the HACL API without taking the full library.

The dist/kremlin directory contains all the required headers from KreMLin. In particular, these headers contain implementations of FStar.UInt128, the module for 128-bit arithmetic. The kremlin/include/kremlin/internal/types.h header will attempt to use C preprocessor macros to pick the right UInt128 implementation for your platform:

  • 64-bit environment with GCC/Clang: hand-written implementation using unsigned __int128 (unverified)
  • MSVC: hand-written implementation using intrinsics (also unverified)
  • every other case, or when KRML_VERIFIED_UINT128 is defined at compile-time: verified (slow) implementation extracted from FStar.UInt128

Bindings for Other Languages

HACL* and EverCrypt are designed to primarily be used either within verification-oriented projects in F* or as part of larger C developments. In addition to these use cases, the library developers and other HACL* users have also developed bindings for other programming languages:

OCaml

The KReMLin compiler auto-generates ocaml-ctypes bindings for HACL*. On top of these “raw” bindings, we add a high-level wrapper that uses functors, shares type signatures, performs run-time checks and offers a much more idiomatic API.

The former can be installed by running make install-hacl-star-raw in dist/gcc-compatible. The latter can be installed by running dune build && dune install in bindings/ocaml.

We expect these to be available in OPAM soon.

JavaScript

HACL* is compiled to WebAssembly via the WASM backend of KreMLin (see the Oakland’19 paper for details). We offer an idiomatic JavaScript API on top of HACL-WASM so that clients do not have to be aware of the KreMLin memory layout, calling convention, etc. This latter API is available as a Node.js package.

The jsdoc documentation of the package can be found online. Please note that the API is asynchronous (it uses promises).

Here is a small example of how to use the library (with Node.js) :

var hacl = require("hacl-wasm");
hacl.Curve25519.ecdh(new Uint8Array(32), new Uint8Array(32)).then(function (result) {
  // Here result contains an Uint8Array of size 32 with the DH exchange result
});

Rust

Various users have also published Rust crates for HACL*, but these have not been vetted by the HACL maintainers.