cryspen / hacl-packages Goto Github PK

The Cryspen HACL Distribution

Home Page: https://cryspen.com/hacl-packages

License: Other

Shell 0.06% CMake 0.63% Makefile 0.09% C 70.39% Dockerfile 0.08% Python 0.91% OCaml 5.43% Rust 3.86% C++ 4.96% Batchfile 0.01% Assembly 12.67% JavaScript 0.84% HTML 0.07%

cryptography formally-verified aead decryption encryption hkdf hmac signatures digest hashing

hacl-packages's Introduction

The Cryspen HACL Packages

This repository contains ready-to-use crypto packages 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.

Currently, we are in the process of adding more usable APIs, providing extensive documentation, and further optimizing the algorithms.

What is HACL* and why should you use HACL Packages?

HACL* is a collection of high-assurance cryptographic algorithms developed as part of Project Everest. It includes source code written in F*, generated C code, 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 and a complicated build system that can be intimidating to a crypto developer who simply wishes to use verified crypto.

Quickstart

Install build dependencies

We need the following dependencies ...

cmake (3.17 or newer)
ninja (1.10 or newer)
python (3.6 or newer)
clang (7 or newer) or gcc (7 or newer)

Depending on your system you can install them as follows (click to expand) ...

Arch Linux

$ sudo pacman -S cmake ninja python

# Either of ...
$ sudo pacman -S clang
$ sudo pacman -S gcc

Fedora

$ sudo dnf install cmake ninja-build python3

# Either of ...
$ sudo dnf install clang
$ sudo dnf install gcc

Ubuntu

$ sudo apt install cmake ninja-build python3

# Either of ...
$ sudo apt install clang
$ sudo apt install gcc

macOS

$ brew install cmake ninja python

# Either of ...
$ brew install llvm
$ brew install gcc

Build (and test) HACL Packages

You can run ...

$ ./mach build --test

... to build HACL Packages and run the tests. All actions are driven by mach. See ./mach --help for details.

Platform support

The HACL Packages are supported based on the following tiers.

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
FreeBSD / x64

Compiler support

A modern C compiler is expected.

Algorithms

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

Family	Algorithm	Support
AEAD	AES-GCM 128	AES-NI & CLMUL (x86 only)
AEAD	AES-GCM 256	AES-NI & CLMUL (x86 only)
AEAD	Chacha20-Poly1305	Portable \| vec128 \| vec256
ECDH	Curve25519	Portable \| BMI2 & ADX
ECDH	P-256	Portable
Signature	Ed25519	Portable
Signature	ECDSA P-256r1	Portable
Signature	ECDSA P-256k1	Portable
Signature	RSA-PSS	Portable
Hash	SHA2-224	Portable \| SHAEXT
Hash	SHA2-256	Portable \| SHAEXT
Hash	SHA2-384	Portable
Hash	SHA2-512	Portable
Hash	SHA3	Portable
Hash	Blake2	Portable \| vec128 \| vec256
Key Derivation	HKDF	Portable (depends on hash)
Symmetric Encryption	Chacha20	Portable \| vec128 \| vec256
Symmetric Encryption	AES 128	AES-NI & CLMUL (x86 only)
Symmetric Encryption	AES 256	AES-NI & CLMUL (x86 only)
MAC	HMAC	Portable (depends on hash)
MAC	Poly1305	Portable \| vec128 \| vec256 \| x64 ASM

Testing

Testing is done with gtest and requires a C++11 compiler (or C++20 MSVC).

Measure Test Coverage

Test coverage in HACL Packages can be measured with ...

./mach build --tests --coverage
./mach test --coverage
./tools/coverage.sh

Note that only clang is supported as a compiler and you may get an error ...

cc: error: unrecognized command-line option ‘-fprofile-instr-generate’; did you mean ‘-fprofile-generate’?

... when your default compiler is not clang. In this case, try to set the CC and CXX environment variables accordingly ...

export CC=clang
export CXX=clang++

Furthermore, additional tools are required to measure (and view) test coverage.

Make sure you have lcov and genhtml.

For Ubuntu these can be installed via ...

$ sudo apt install lcov

When everything went well you should be able to view the coverage reports with, e.g., ...

firefox build/Debug/coverage/full/html/index.html

Dependencies

Tests require the nlohmann_json package to read json test files. CMake takes care of pulling and building the package.

License

HACL packages are licensed under either of

at your option.

hacl-packages's People

Contributors

Stargazers

Watchers

Forkers

jpgoldberg addressxception bkmgit pnmadelaine duesee vertalo manasjayanth mamonet emillon ziqiaozhou ma-ilsi election-tech-initiative thb-sb rchyena s-zanella samuel-lee-msft

hacl-packages's Issues

Rust bindings

degenerate Makefile so that running `make` defers to `./mach.py build`

Pick a benchmarking system

Clean Rust API

remove deprecated items
remove unused APIs
consistent naming of APIs (all hacl?)
consistent API design (naming, parameter order, ...)
documentation

64-bit Windows (x86_64-pc-windows-msvc) T1

[mach] test

Improving mach's test capabilities.

Benchmarks

Tracking implementations of benchmarks.

Implement benchmarks for all primitives

HACL

EverCrypt

Variants

Discuss if we also want to provide examples for variants, i.e., 32/256/512.

allow setting gtest filters

Streamline ./mach update

Only copy upstream files that we want https://github.com/cryspen/hacl/blob/f7851963ef02e227ffd4a617f91d8d13580d2971/tools/vcs.py#L44
Copy ml files
Copy karamel
add info.txt
#299

ARM64 Android (aarch64-linux-android) T2

Add CodeQL to CI

To catch issues like: hacl-star/hacl-star#550

We should make sure this applies to the Windows and C89 flavors of our code;

Feature parity with upstream dist

Tracking build feature parity with the upstream hacl* dist directory.

ARM64 iOS (aarch64-apple-ios) T2

set up documentation automation

[mach] Bindings

Handle bindings with mach

32-bit Linux (i686-unknown-linux-gnu) T1

GCC-latest, clang-latest, ~~gcc-minimum~~

OCaml bindings

implement documentation system

Check if everything we want is done.

Copy tests from upstream

https://github.com/cryspen/hacl/blob/f5fe166470347c14ca089cba3acc88269722452c/tools/vcs.py#L45

ARM64 macOS (aarch64-apple-darwin) T2

32-bit Windows (i686-pc-windows-msvc) T1

Mach usability

#8
#9
without cmake mach fails with an unhelpful backtrace FileNotFoundError: [Errno 2] No such file or directory: 'cmake'
running ./mach.py test on my M1 gives: FileNotFoundError: [Errno 2] No such file or directory: './blake2b'

Document CI (book)

[docs] Documentation System

Document system and process

pick documentation tooling

[mach] Snapshots (dist)

Tracking generation of snapshots (other dists)

copy headers
allow setting feature restrictions
write out config.h

JS bindings

Move https://github.com/hacl-star/hacl-star/tree/main/bindings/js to this repo and delete there.

copy bindings into js
update mach update to copy wasm as well
add JS build/test to mach
add bindings to CI node api_test.js && node test2.js && node test3.js
publish new release
- test packaging on CI
publish documentation

Feature parity with C library

Ensure that Rust exposes all APIs we have (advertise) in the C API.

[mach] Build

Tracking progress on mach for building

allow disabling features
selectively run tests
~~connect to F*/kremlin config~~
support GCC and clang

Build static and dynamic libraries

https://github.com/cryspen/hacl/blob/92293fdc43c6db96021ee725ddeb1a4c8493e1cb/CMakeLists.txt#L172

re-usable CI configuration

https://github.blog/2022-02-10-using-reusable-workflows-github-actions/

64-bit Linux (x86_64-unknown-linux-gnu) T1

GCC-latest, clang-latest, ~~gcc-minimum~~

maybe have a little bit of setup check in mach that ensures ninja, cmake, etc. are found in the path? (there was a similar unfortunate error for the absence of ninja)

Build & test with minimum GCC and clang versions

~~- [ ] GCC 4.8~~
The c89 compatible code is broken. We are skipping this for now.

Clang 7

make util.binary_path dependent on config

https://github.com/cryspen/hacl/blob/4aa8d08b450f61c1e9b7e1ff9a89e4a8f1c439a1/tools/utils.py#L14

set upstream repository or directory

./mach update should take an argument where to find the hacl-star distribution.
This can be

a directory
a git repository

If the upstream is a git repository

set revision to pull

ARM64 Linux (aarch64-unknown-linux-gnu) T2

build if test not present instead of aborting

./mach test
 [mach] Running tests ...
 [mach] ! Nothing is built! Please build first. Aborting!

hacl-star-raw

The basic hacl-star-raw source is in https://github.com/cryspen/hacl-packages/tree/main/ocaml.
This issue should make sure that the raw package is working as expected.

Allow algorithm selection for agile APIs

Building with ./mach build -a blake2 (or any other algorithm) disables evercrypt (the agile APIs).
While this is intentional, it's not great. It would be best to add a new well-designed, flexible API on top of HACL that would allow this.

set up public documentation endpoint

remove unnecessary CI jobs

[meta] CI

Tier 1 Targets

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

Tier 2 Targets

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.

Document supported SHA3 and blake2 versions

Documentation only says SHA3 and blake2 but doesn't mention which versions are supported.

Ensure Toolchain and Platform Checks are correct

The build currently replicates what the upstream configure script. But that's not always correct or complete (see for example hacl-star/hacl-star#519 (comment)).

See https://github.com/cryspen/hacl/blob/main/cpu-features.md for full CPU feature matrix.

Check for AES instructions
- Lib_IntVector_Intrinsics_ni_aes_enc, Lib_IntVector_Intrinsics_ni_aes_enc_last, Lib_IntVector_Intrinsics_ni_aes_keygen_assist
- x86: AES
Check for clmul instructions
- Lib_IntVector_Intrinsics_ni_clmul
- x86: PCLMULQDQ
Check for SSE2
- Lib_IntVector_Intrinsics_vec128_xor, Lib_IntVector_Intrinsics_vec128_eq32, Lib_IntVector_Intrinsics_vec128_gt32, Lib_IntVector_Intrinsics_vec128_or, Lib_IntVector_Intrinsics_vec128_and, Lib_IntVector_Intrinsics_vec128_lognot, Lib_IntVector_Intrinsics_vec128_shift_left, Lib_IntVector_Intrinsics_vec128_shift_right, Lib_IntVector_Intrinsics_vec128_shift_left64, Lib_IntVector_Intrinsics_vec128_shift_right64, Lib_IntVector_Intrinsics_vec128_shift_left32, Lib_IntVector_Intrinsics_vec128_shift_right32, Lib_IntVector_Intrinsics_vec128_shuffle32, Lib_IntVector_Intrinsics_vec128_shuffle64, Lib_IntVector_Intrinsics_vec128_rotate_right_lanes32, Lib_IntVector_Intrinsics_vec128_rotate_right_lanes64, Lib_IntVector_Intrinsics_vec128_load32_le, Lib_IntVector_Intrinsics_vec128_load64_le, Lib_IntVector_Intrinsics_vec128_store32_le, Lib_IntVector_Intrinsics_vec128_store64_le, Lib_IntVector_Intrinsics_vec128_zero, Lib_IntVector_Intrinsics_vec128_add64, Lib_IntVector_Intrinsics_vec128_sub64, Lib_IntVector_Intrinsics_vec128_mul64, Lib_IntVector_Intrinsics_vec128_smul64, Lib_IntVector_Intrinsics_vec128_add32, Lib_IntVector_Intrinsics_vec128_sub32, Lib_IntVector_Intrinsics_vec128_load64, Lib_IntVector_Intrinsics_vec128_load64s, Lib_IntVector_Intrinsics_vec128_load32, Lib_IntVector_Intrinsics_vec128_load32s, Lib_IntVector_Intrinsics_vec128_interleave_low32, Lib_IntVector_Intrinsics_vec128_interleave_high32, Lib_IntVector_Intrinsics_vec128_interleave_low64, Lib_IntVector_Intrinsics_vec128_interleave_high64
Check for SSE3
- Lib_IntVector_Intrinsics_vec128_rotate_left32_8, Lib_IntVector_Intrinsics_vec128_rotate_left32_16, Lib_IntVector_Intrinsics_vec128_rotate_left32_24, Lib_IntVector_Intrinsics_vec128_rotate_left32, Lib_IntVector_Intrinsics_vec128_rotate_right32, Lib_IntVector_Intrinsics_vec128_load_be, Lib_IntVector_Intrinsics_vec128_load32_be, Lib_IntVector_Intrinsics_vec128_load64_be, Lib_IntVector_Intrinsics_vec128_store_be, Lib_IntVector_Intrinsics_vec128_store32_be, Lib_IntVector_Intrinsics_vec128_store64_be (all also SSE2)
Check for SSE4.1
- Lib_IntVector_Intrinsics_vec128_eq64, Lib_IntVector_Intrinsics_vec128_insert8, Lib_IntVector_Intrinsics_vec128_insert32, Lib_IntVector_Intrinsics_vec128_insert64, Lib_IntVector_Intrinsics_vec128_extract8, Lib_IntVector_Intrinsics_vec128_extract32, Lib_IntVector_Intrinsics_vec128_extract64, Lib_IntVector_Intrinsics_vec128_mul32, Lib_IntVector_Intrinsics_vec128_smul32 (also sse2)
Check for SSE4.2
- Lib_IntVector_Intrinsics_vec128_gt64,

hacl-star

The hacl-star source code is in https://github.com/cryspen/hacl-packages/tree/main/ocaml/hacl-star.
This issue should make sure that the opam packaging works as expected and it is easy to publish new packages.

build opam package
publish opam package

[cmake] Build

Tracking the cmake build

[mach] Update

Tracking the update sub-command

#76
copy all needed files (msvc, c89)
#12
write out revision of all dependencies
make snapshot of all dependencies in a docker image
only copy what's really needed (using dependency analysis)