libcrux 0.0.1

Formally Verified Cryptography
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

# libcrux Architecture

libcrux contains [specifications in hacspec] as well as efficient implementations of cryptographic
primitives.

## HACL

[HACL*] is a collection of high-assurance cryptographic algorithms originally
developed as part of [Project Everest] and now maintained by the [HACL Community].
libcrux uses [HACL*] through the [Rust bindings] official [HACL packages] distribution.

![](architecture/hacl.excalidraw.svg)

## libjade

TBD

## AU Curves

The pipeline is described [here](https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust).

# Properties & Guarantees

Every implementation in libcrux is formally verified.
But it is important to be precise about proven properties and how the properties
proven translate to the code that's actually used.

## HACL

The HACL toolchain is depicted above.

1. The hacspec code is translated to F*, which is proven equivalent to the Low* implementation in HACL\*.
2. The Low\* code is extracted to C with [KaRaMel].
3. The C API is wrapped in a safe Rust API.
4. The Rust API is orchestrated depending on use case and available hardware.

### Properties

The equivalence proofs in 1. and the extraction in 2. ensure that the C code

- is correct with respect to the specification
- has secret independent performance
- is memory safe

Because the C API can not guarantee certain preconditions expected in the proofs
of the F* code (e.g. input sizes), these properties are ensured in the safe Rust
wrapper (3).

## libjade

TBD

## AU Curves

The AUCurves toolchain is depicted above.

0. The hacspec BLS spec contains [unit tests](https://github.com/hacspec/hacspec/blob/master/examples/bls12-381/src/bls12-381.rs#L809) and [property tests](https://github.com/hacspec/hacspec/blob/master/examples/bls12-381/src/bls12-381.rs#L530).
1. The hacspec code is translated to Coq, which is [proven equivalent](https://github.com/AU-COBRA/AUCurves/blob/main/src/Hacspec/Curve/BlsProof.v) to the specification of fiat-cryptography.
   This has been done for the group operations on both G1 and G2.
2. Fiat-cryptography can be use to generate efficient (C or rust) field operations for the fields underlying G1 and G2.
3. Bedrock2 can be used to generate the group operations in C, or Rust. 
   Printing to rust is done in Coq, but it is experimental and unverified.
   Alternatively, we can wrap the C code in a Rust API.

See the [specs] for a detailed list of proofs and properties.

[specifications in hacspec]: src/specs/Readme.md
[specs]: src/specs/Readme.md
[hacl*]: https://hacl-star.github.io
[project everest]: https://project-everest.github.io/
[hacl community]: https://github.com/hacl-star
[hacl packages]: https://github.com/cryspen/hacl-packages
[rust bindings]: https://github.com/cryspen/hacl-packages/tree/main/rust
[karamel]: https://github.com/FStarLang/karamel