HACL* (High-Assurance Cryptographic Library) is a formally verified cryptographic library in F*, developed by the Prosecco team at INRIA Paris in collaboration with Microsoft Research, as part of Project Everest. HACL* was inspired by discussions at the HACS workshop and aims at developing a set of reference implementations in C for common cryptographic primitives.

This is the first post in a series describing formal verification in NSS as an approach to improve confidence in highly complex, highly security critical code. In this first post I describe the most important ideas and concepts of HACL*, the basis of most formally verified code in NSS. If you want to have all the juicy details about HACL*, I recommend reading the CCS’17 paper.

HACL*

HACL*, though written in F*, can be compiled to C code with guaranteed memory safety, secret independent computation, and functional correctness with respect to some mathematical specification. Let’s first have a look at the high-level idea of HACL* on the example of Curve25519.

The first step is to take the specification (RFC 7748 in this case) and translate it into a high level F* specification. This specification is easy to read and can be checked for correctness against the RFC easily. All correctness guarantees HACL* gives for the generated C code are based on this specification, i.e. the C code is proven to be functionally equivalent to the the high level specification. Here the definition of the Montgomery ladder, an excerpt from the Curve25519 specification. (Apologies for the highlighting, no F* support.)

 1let rec montgomery_ladder_ (init:elem) x xp1 (k:scalar) (ctr:nat{ctr<=256})
 2  : Tot proj_point (decreases ctr) =
 3  if ctr = 0 then x
 4  else (
 5    let ctr' = ctr - 1 in
 6    let (x', xp1') =
 7      if uint_to_nat (ith_bit k ctr') = 1 then (
 8        let nqp2, nqp1 = add_and_double init xp1 x in
 9        nqp1, nqp2
10      ) else add_and_double init x xp1 in
11    montgomery_ladder_ init x' xp1' k ctr'
12)

Running the reference implementation is possible but obviously slow (it is executed in OCaml). However a subset of F* (called Low*) can be translated to C using Kremlin. While the specification might be valid Low* code it is not optimised and thus won’t yield fast C code. In order to generate fast C code more efficient Low* code has to be written first. Looking at state of the art C code for the given algorithm (Curve25519 Donna for example) Low* code can be written that resembles the fast C code and can be extracted via Kremlin to similarly looking C code.

At this point the main benefit of the HACL* approach comes to light. The optimised Low* code (as well as the extracted C code) are hard to get right and even harder to review for correctness, memory safety, and secret independent execution. Using an SMT solver (Z3 is used in HACL*) and F*’s strong type system, functional equivalence is proven between the high-level F* specification and the optimised Low* code. The Low* code usually has to be enhanced with additional information to help prove the equivalence. This additional code however is ignored by Kremlin and doesn’t get translated to C.

The following graphic gives an overview of the HACL* process.

An Example - Conditional Swap

HACL* is a pretty complex library and it might be hard to understand what’s going on. Therefore I’ll give a small example of the basic concepts behind HACL* focusing on functional correctness.

Conditional swaps are used for example in Curve25519 implementations to swap two variables a and b if a certain condition is given, c = 0 here. In F* this can be written as follows.

1val cswap: x:uint32 -> y:uint32 -> c:uint32 ->
2  Tot (uint32 * uint32)
3let cswap x y c =
4  if c = 0ul then
5    (x, y)
6  else
7    (y, x)

This code can be easily inspected for correctness and is used as specification. However, this is not the code we want to have as it branches on potentially secret data in c. Instead of checking c for 0 we should use masking and logical operations to achieve the variable swapping. Note that we require c to be either all 1 or all 0 now. This can be easily computed from the single bit c we had in the previous example. This looks as follows in pseudo-C-code.

1void cswap_constant_time(uint32_t *a, uint32_t *b, uint32_t c) {
2    uint32_t mask = (*a ^ *b) & c;
3    *a = *a ^ mask;
4    *b = *b ^ mask;
5}

The same code in F* (with slightly different input/output behaviour) looks as follows.

1val cswap_constant_time: x:uint32 -> y:uint32 -> c:uint32{c = 0xFFFFFFFFul \/ c = 0ul} ->
2  Tot (uint32 * uint32)
3let cswap_constant_time x y c =
4  let mask = (x ^^ y) &^ c in
5  let a = x ^^ mask in
6  let b = y ^^ mask in
7  (a, b)

This code is not trivially correct anymore and requires considerable thought by both author and reviewer. But instead of staring at the code to understand it or writing incomplete tests we can use F* now to prove that cswap_constant_time is equivalent to our spec, i.e. cswap. To this end we write a lemma to ensures that.

1let a, b = cswap_constant_time x y c in
2let c, d = cswap x y c in
3a = c /\ b = d

While this can’t be proven immediately it is relatively easy to write some helper lemmata that help F* and Z3 to understand the correctness of this statement. The C code extracted by Kremlin from the F* code above then looks as follows.

1typedef struct {
2  uint32_t fst;
3  uint32_t snd;
4}
5K___uint32_t_uint32_t;
6
7K___uint32_t_uint32_t Impl_CSwap_cswap_constant_time(uint32_t x, uint32_t y, uint32_t c) {
8  return ((K___uint32_t_uint32_t){ .fst = x ^ ((x ^ y) & c), .snd = y ^ ((x ^ y) & c) });
9}

Check out the repository for the full source code of the example.

Memory safety can be proven easily as well by specifying liveliness conditions of buffers. In this example we don’t have buffers so no need for verifying memory safety. We skip proving secret-independent execution here as it requires additional support from HACL*.

Code Generation vs Code Verification

The HACL* approach as described above is a great way of generating fast C code that’s proven to be correct, memory safe, and have secret-independent runtime. For NSS we decided to use code generation and integrate code from HACL* into the code base. However, instead of generating code it would also be possible to verify existing C code with other tools such as Cryptol/SAW to prove similar properties of the code.

The main advantage of code generation is that the mathematical specifications can be easily used to build more complex algorithms and protocols on top and allow for re-use of specification code. The trusted code base written in F* is therefore very small.

The main drawback of generating code is a relatively large third-party code base that has to be trusted in order to generate the code. The weakest link in the case of HACL* is probably Kremlin, which has a hand written proof but is a relatively young piece of code that probably contains bugs.

There is no optimal solution to this problem that works for everyone but the HACL* approach as described in this post is a great way to get better confidence in correctness and security of complex C code using formal verification.

In the next post I’ll talk about challenges we faced when integrating code from HACL* into NSS and how we solved them.