HACL Packages

The Cryspen HACL packages is a collection of cryptographic libraries developed by Cryspen on top of HACL*. In particular, it contains a portable C crypto library that selects optimized implementations for each platform, as well as Rust, OCaml, and JavaScript bindings for this library.

Getting Started

If you want to build from sources or run tests, get started on Github.

Depending on the language you are looking for there are different entry points.

• C
• Rust
• OCaml
• JavaScript

Contributing

The Cryspen HACL packages are free and open source. You can find the source code on GitHub and issues and feature requests can be posted on the GitHub issue tracker. If you'd like to contribute, please read the CONTRIBUTING guide and developer section and consider opening a pull request.

The HACL* repository is a collection of high-assurance cryptographic algorithms developed as part of Project Everest. It includes source code written in F*, generated code in C, verified assembly code from the Vale project, and an agile multiplexed cryptographic provider called EverCrypt. As such, the full HACL* repository contains many software artifacts.

Get in touch for more information or support.

Algorithms

The following tables gives an overview over the algorithms supported by the HACL packages.

For a detailed description fo the Support column, please see the Architectures section.

Platforms

The HACL Packages are supported based on the following tiers.

For a detailed description of the different supported architecture see the next section.

Tier 1

Tier 1 targets are guaranteed to work. These targets have automated testing to ensure that changes do not break them.

• x86_64 Linux (x86_64-unknown-linux-gnu)
• x86 Linux (i686-unknown-linux-gnu)
• x86_64 macOS (x86_64-apple-darwin)
• x86_64 Windows
  • x86_64-pc-windows-msvc
  • x86_64-pc-windows-clang
• x86 Windows (i686-pc-windows-msvc)

Tier 2

Tier 2 targets are guaranteed to build. These targets have automated builds to ensure that changes do not break the builds. However, not all of them are always tested.

• arm64 macOS (aarch64-apple-darwin)
• arm64 Linux (aarch64-unknown-linux-gnu)
• arm64 Android (aarch64-linux-android)
• arm64 iOS (aarch64-apple-ios)
• s390x z14 Linux (s390x-unknown-linux-gnu)

Tier 3

Tier 3 targets are supported by the code but there are no automated checks and there is no guarantee that they work.

• ARMv7 Android (aarch64arm-linux-androideabi)
• arm64 iOS Simulator (aarch64-apple-ios-sim)
• x86_64 iOS (x86_64-apple-ios)
• PowerPC
• IBM Z15
• FreeBSD / x64

Architectures

The HACL C library has different optimization for different platforms.

Development News

A short log of what is happening in the HACL world. This is not authoritative. Please see the CHANGELOG for released changes.

June 2023

Git changes

May 2023

Git changes

April 2023

Git changes

Releases

• OCaml 0.7.0

March 2023

Git changes

Added

• Rust low-level APIs
• OCaml v0.7.0

Fixed

• FreeBSD build

February 2023

Git changes

Changed

• SHA2 and SHA3 performance improvements
• Improved benchmarking for all primitives

Added

• Integration of JS bindings
• Rust low-level API

Fixed

• hacl-star <> hacl-packages integration

mach

The main entry point for all operations is the mach script.

Dependencies

Building HACL from sources requires a set of basic dependencies

• cmake > 3.17
• ninja
• python > 3.8
• clang or gcc (note that primarily clang is used)

Command line reference

usage: mach [-h] {benchmark,configure,doc,rust,test,update,install,build,clean} ...

positional arguments:
  {benchmark,configure,doc,rust,test,update,install,build,clean}

options:
  -h, --help            show this help message and exit

build

usage: mach build [-h] [-c] [--tests] [--test] [--benchmarks] [--benchmark] [--no-openssl]
                  [--libtomcrypt] [-r] [-a ALGORITHMS] [-p TARGET] [-d DISABLE] [-s SANITIZER]
                  [--ndk NDK] [--msvc] [-e EDITION] [-l LANGUAGE] [-v] [-m32] [--no-build]
                  [--coverage]

Main entry point for building HACL

    For convenience it is possible to run tests right after building using --test.

    Supported cross compilation targets:
        - x86_64-apple-darwin (macOS aarch64 only)
        - s390x-linux-gnu
        - aarch64-apple-ios (macOS only)
        - aarch64-apple-darwin (macOS x64 only)
        - aarch64-linux-android

    Features that can be disabled:
        - vec128 (avx/neon)
        - vec256 (avx2)
        - vale (x64 assembly)

    Supported sanitizers:
        - asan
        - ubsan

    Use an edition if you want a different build. Note that this build will
    use the MSVC version by default on Windows.
    Supported editions:
        - c89

    HACL can be built for another language than C.
    Note that bindings will always require the full C library such that the
    algorithm flag will be ignored.
        - rust
        - ocaml
        - wasm (TBD)

    ! Windows builds are limited. The following arguments are not supported:
        - algorithms
        - sanitizer
        - edition
        - disable
        - coverage
    

options:
  -h, --help            show this help message and exit
  -c, --clean           Clean before building.
  --tests               Build tests.
  --test                Build and run tests.
  --benchmarks          Build benchmarks.
  --benchmark           Build and run benchmarks.
  --no-openssl          Don't build and run OpenSSL benchmarks.
  --libtomcrypt         Build and run LibTomCrypt benchmarks.
  -r, --release         Build in release mode.
  -a ALGORITHMS, --algorithms ALGORITHMS
                        A list of algorithms to enable. Defaults to all.
  -p TARGET, --target TARGET
                        Define compile target for cross compilation.
  -d DISABLE, --disable DISABLE
                        Disable (hardware) features even if available.
  -s SANITIZER, --sanitizer SANITIZER
                        Enable sanitizers.
  --ndk NDK             Path to the Android NDK.
  --msvc                Use MSVC on Windows (default is clang-cl).
  -e EDITION, --edition EDITION
                        Choose a different HACL* edition.
  -l LANGUAGE, --language LANGUAGE
                        Build language bindings for the given language.
  -v, --verbose         Make builds verbose.
  -m32                  Build for 32-bit (even when on 64-bit).
  --no-build            Don't actually build (don't run ninja).
  --coverage            Build with coverage instrumentation.

test

usage: mach test [-h] [-a ALGORITHMS] [-l LANGUAGE] [--coverage] [-v]

Test HACL*

options:
  -h, --help            show this help message and exit
  -a ALGORITHMS, --algorithms ALGORITHMS
                        The algorithms to test.
  -l LANGUAGE, --language LANGUAGE
                        Language bindings to test.
  --coverage            Test with coverage instrumentation.
  -v, --verbose         Make tests verbose.

The HACL C Package

The HACL C package is a modular, easy to use C library for low-level cryptographic primitives.

The (latest) documentation can be found here: HACL Packages API Reference (main) 📚

Releases of the C library can be found on Github 📦

CMake

You can include HACL Packages in your CMake project using FetchContent.

The CMakeLists.txt could look like this. To use a specific release change the GIT_TAG to the release tag.

cmake_minimum_required(VERSION 3.10)

include(FetchContent)
FetchContent_Declare(hacl
    DOWNLOAD_EXTRACT_TIMESTAMP TRUE
    GIT_REPOSITORY https://github.com/cryspen/hacl-packages/
    GIT_TAG main
)
FetchContent_MakeAvailable(hacl)

project(hacl-blake-example)

add_executable(example blake-example.cc)

# Add includes from HACL
target_include_directories(example PRIVATE
    ${hacl_SOURCE_DIR}/include
    ${hacl_SOURCE_DIR}/build
    ${hacl_SOURCE_DIR}/karamel/include
    ${hacl_SOURCE_DIR}/karamel/krmllib/dist/minimal
    ${hacl_SOURCE_DIR}/vale/include
)
# Link the HACL library
target_link_libraries(example PRIVATE hacl)

You can find the full example in examples/cmake.

Rust Package

The hacl-rust crate provides bindings to the HACL C package in Rust.

See the rust docs for more information and get the create from crates.io.

cargo add hacl

OCaml Package

For more information on the OCaml package please

• check out the latest documentation: HACL Packages API Reference (main) 📚
• the opam package 📦 (latest release)

Releases

See Changes.md for changes between the versions.

JavaScript Package

HACL* is compiled to WebAssembly via the WASM backend of Karamel (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 Karamel memory layout, calling convention, etc. This latter API is available as a Node.js package. Please note that the API is asynchronous and uses promises.

Example (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
  });

Documentation

Please check out the latest documentation 📚

Developer Guide

The following pages provide information when you want to contribute to HACL packages.

Contributing

See CONTRIBUTING.md

Repository Overview

The hacl-packages repository is a mono repository for all HACL packages and bindings. The top level holds the HACL C library that is based on the output of HACL*.

Source Code

The C source code lives in the src directory for most platforms.

The source code for MSVC can be found in src/msvc.

The includes can be found in the corresponding include directories (include and include/msvc).

Vale is considered an external dependency and therefore lives in its own directory vale --- sources in vale/src and headers in vale/include.

Tests

Tests are found in the tests folder and are written in modern C++ rather than C.

Karamel

The KaRaMeL dependency is found in karamel and holds only headers that are used by the HACL C source code.

CPU Features

A tool for basic CPU feature detection can be found in cpu-features. This is only used for tests and will probably be removed from this repository in future.

Tools

The build is driven by the mach script and the CMakeLists.txt. They rely on the contents of the tools folder (general tools for managing the repository and building in Python), as well as the config folder (platform detection and build configuration helper).

Docker

Docker tools for extracting the source code from HACL* are found in docker.

Docs

The docs folder contains this book you're reading right now.

Bindings

The language bindings are in sub folders.

Rust

The Rust bindings can be found in the rust folder. See the Rust chapter for more details on the build and structure.

OCaml

The OCaml bindings can be found in the ocaml folder. See the OCaml chapter for more details on the build and structure.

Build Process

The HACL C library is built with CMake and ninja and uses a Python driver script called mach. Due to the modular nature of the library the build is more complex than for many other libraries.

Selecting Algorithms

The algorithms compiled into the library can be selected using the -a|--algorithm argument on mach. By default all algorithms are selected. The files used in the build are selected by running a dependency analysis on the requested algorithm files (see configure.py). The resulting configuration is written into build/config.cmake, which is used as input into the main build process. This process is part of the mach script.

Platform Detection

Depending on the used toolchain a different set of algorithms can be used. In order to define the feature set available in the toolchain CMake runs a set of tests. Note that the toolchain feature must not be the same as the platform feature set the build is running on (due to cross compilation or extended features in the toolchain compared to the actual hardware). The library has runtime feature detection to ensure that hardware features are only used when they are actually available.

Release Builds

By default the builds use the debug mode. For release builds

./mach build --release

is used.

Rust

⚠️ The Rust bindings are work in progress.

OCaml

There are two different ways of building the OCaml bindings.

Standalone (Packaging)

For packaging the hacl-star opam package the bindings can be built standalone.

./opam.sh
cd opam

First we need to get the HACL C code, build it, and put it where the Makefile expects the result. The opam.sh script puts everything in the right place within the opam directory. In the directory we can now build/install the opam package(s) hacl-star (and hacl-star-raw).

opam install . --verbose --with-test --yes

Documentation can be built with

dune build @doc --only-packages=hacl-star

Mach (Dev Mode)

⚠️ The dev mode is not working right now

When working on the library mach offers a convenient way of building the C library and the ocaml bindings through mach using the -l|--language argument.

./mach build -l ocaml

This build the C library, copies the result into the ocaml directory, and then builds the OCaml bindings on top. Tests can be called through mach as well ./mach test -l ocaml.

JavaScript

Building, testing, and installing the hacl-wasm npm package

The package directory can be put together using a script:

./npm.sh
cd npm

Tests can be run with:

node api_test.js

The package can be installed with:

npm install

Publishing a new version of the hacl-wasm package to npm

Assuming all the steps above ran successfully, a new version of the package can be published on npm. First, update the version number in package.json and propagate it using npm install.

A tag js-vX.X.X should be created with the new version of the package.

The package can then be published with:

npm publish

This last step requires having logged in to npm and having the correct access rights.

Continuous Integration

The HACL Packages project uses GitHub Actions as its primary CI/CD system.

When a pull request (PR) or push is made to HACL Packages, the CI automatically runs a series of checks to ensure that all code compiles, all tests pass, and all changes are of a certain quality. To reduce the amount of computational work, the HACL Packages CI is configured to ignore commits that don't justify a CI run. For example, the CI will not run on changes of the README.md (and other *.md files in the root folder). If, for whatever reason, you think that a particular commit should not start the CI, consider including [skip ci] to your commit message. (See Skip pull request and push workflows.)

Workflows

The CI configuration files are located in the .github/workflows folder. Local actions reused across the HACL Packages CI are in the .github/actions folder.

There are multiple workflow files with the following tasks:

• build.yml builds and tests HACL Packages on many systems (see below).
• build_pull_request.yml builds and tests HACL Packages PRs on many systems (see below).
• sanitizer_builds.yml builds and tests HACL Packages on Linux (x86/x64) with UBSAN and ASAN
• gh-pages.yml builds and publishes new versions of this book.
• new_issue.yml adds newly created issues to the HACL Packages project board.
• ocaml.yml builds the OCaml bindings for HACL packages.
• rust.yml builds the Rust bindings for HACL packages.

What systems are tested?

GitHub Actions uses the concept of a "job matrix" to fan out a single job description to multiple separate jobs. This is useful to test a job on different systems, e.g., Linux, macOS, and Windows. In HACL Packages, and especially in the build workflow, we use matrices of the form ...

matrix:
  compiler: [ gcc, clang ]
  version: [ 7, 8, ..., 14 ]
  bits: [ 32, 64 ]
  edition: [ "" ]
  exclude:
    - compiler: gcc
      version: 12
    # ...
    # Not available
    - compiler: clang
      version: 14

... to cover the following targets:

Furthermore, on Linux, we test different "editions" of the C programming language, i.e., "msvc".

Documentation

The HACL Packages documentation consists of a high-level HACL Packages Book (that you are reading right now) and (multiple) technical references describing the provided programming language bindings.

The book aims to give a high-level overview of the HACL Packages project. It describes the build process, the infrastructure (CI/CD), and how we want to work with each other. Notably, we also need to document the documentation system itself, which is what the next section is about.

Documentation Infrastructure (C)

Building the documentation

The HACL Packages can be built with mach ...

./mach doc

... and the tool will tell you what to install and how to view the documentation.

Contributing to the documentation

The documentation system uses Doxygen, Sphinx, and Breathe to document the HACL* C API.

The build process is roughly as follows: First, mach runs Doxygen to generate an XML representation of the HACL* library. Then, Sphinx uses the Breathe plugin to extract and create reference documentation in all places in the markdown files that reference HACL* C functions or types.

A directive to a C function in the HACL* library may look like this:

```{doxygenfunction} Hacl_Hash_SHA2_hash_256
```

Here, we used the doxygenfunction directive to instruct Sphinx to generate a documentation block for the Hacl_Hash_SHA2_hash_256 function. This will always create a stub of the function and, possibly, documentation if available.

Referencing functions (and types) on a fine-grained basis allows us to "cluster" API entry points and makes the documentation easier to understand. Thus, we also use tabs and sections to improve readability. Note that you can wrap code blocks by using more backticks:

`````{tabs} A tab environment
````{tab} First tab
```{doxygenfunction} Hacl_Hash_SHA2_hash_256
```
````
````{tab} Second tab
```{doxygenfunction} Hacl_Hash_SHA2_hash_512
```
````

Adding missing documentation

Generally, the reference documentation, i.e., the description of a specific type or function, should leverage as much existing documentation as possible from the HACL* project. Suppose a particular function (or type) lacks documentation. In that case, we can proceed as follows: Either we provide ad-hoc documentation by opening a PR on HACL Packages and writing it just below the referenced stub, or we provide documentation by opening a PR in the HACL* project updating HACL Packages afterward.

Generally, we do want to upstream as much documentation as possible. Still, the first variant can be a stepping stone toward variant two. Furthermore, it could make sense to provide information in HACL Packages that don't fit in HACL*.

OCaml Docs

The OCaml documentation system (odoc) doesn't support documenting multiple versions. The [ocaml-docs] workflow can be used to generate documentation for all ocaml- tags (releases).

Creating a new release

When creating a new release an ocaml- tag with the new version number is created. (1) After creating the tag the gh-pages job must be triggered to create the new, tagged ocaml documentation. (2) After creating the docs, a link to them must be added to the table in hacl-ocaml/readme.md.

Benchmarks

HACL Packages provides a set of benchmarks that serves two purposes: To detect regressions, and to see how HACL Packages compares to other cryptographic libraries. Although the benchmarks give us an idea about HACL Package's performance, they should not be overly relied on.

All benchmarks are in the benchmarks folder and are registered through config/config.json in mach. To build the benchmarks, run ...

./mach build --benchmarks --release

Then, to run the benchmarks, execute ...

./mach benchmark

Note that it is also possible to compare two benchmark runs, e.g., to test for regressions. For this, you need to have a separate hacl-packages checkout, and execute ...

./mach benchmark --compare <path_to_other_hacl_packages_checkout>

Note that you need to build the benchmarks in the other checkout, too. But mach will remind you about that.

OpenSSL comparison

The benchmarks in HACL are compared with OpenSSL. If OpenSSL 3 is not in the PATH, the OPENSSL_HOME environment variable can be set. To disable OpenSSL benchmarks, use --no-openssl when building benchmarks.

Contributing to the benchmarks

We use the Google Benchmark framework to define and run all benchmarks and it is generally useful to consult the User Guide while working on the benchmarks. Although Google Benchmark helps a lot, writing benchmarks remains a delicate task. Thus, we collected some rules of thumb to apply during benchmarking:

• Benchmark against a specific usecase, i.e., "Alice obtains a serialized message, and public key, and needs to verify it.". This way, it is clear with what input the benchmarks start. If you provide a comparison, e.g., against OpenSSL, make sure that both libraries "do the same thing", i.e., that we don't measure setup/cleanup routines in one library but skip in the other.
• Use fixed inputs. During benchmarking, it is okay to always use the same message, same key material, etc. If you feel that we need to randomize this, do it deterministic, e.g., by precomputing random values.
• Do not use assert. Asserts are stripped in release builds and may even lead to broken benchmarks because the code you intended to run is optimized out.
• Do not test. Benchmarks are benchmarks. Tests are tests. If you feel that a benchmark would benefit from a sanity check, you can use state.SkipWithError(). Note, however, that you probably want to avoid this in the benchmark loop. Also, in comparisons, when you check the value of one library, make sure to also check in the other library.
• Don't repeat yourself. It is tempting to copy&paste benchmark code. We've been there and it doesn't turn out great. Try to make good use of Google Benchmark features to deduplicate code.