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) : .. code-block:: javascript 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.