Improving the implementation of cryptography in Tezos Octez

• 1. Our cryptography toolchain, and why it matters
• 2. The HACL* library
• 2.1 Quick, correct, and compatible: pick three
• 2.2 Three cryptographic primitives
  • 2.2.1 P-256
  • 2.2.2 SHA-3
  • 2.2.3 BLAKE2
• 3. EverCrypt: an API for HACL* (and more)
• 3.1 How EverCrypt enhances HACL*
• 3.2 Advantages of having a cryptographic provider
• 3.3 The OCaml API
• 4. A deep dive into the OCaml API
• 4.1 The low-level API hacl-star-raw
• 4.2 The high-level API hacl-star
• 4.3 Using the high-level API
• 5. Further reading
• Acknowledgements

1. Our cryptography toolchain, and why it matters

A safety-critical program is only as trustworthy as the libraries it relies on, so we at Nomadic Labs pay close attention to our tools and dependencies — i.e. to our toolchain.

Our toolchain is based on HACL*; a verified library of cryptographic primitives, which include the hash functions which are the backbone of blockchain technology (principally: Blake2), and the digital signatures which we use to assure transaction authenticity (Ed25519, P-256, and secp256k1 ²).

In this blog post, we’ll discuss recent improvements to our cryptography toolchain, and how we integrated them into practical OCaml programming of the Tezos Octez implementation. Namely:

• HACL* has been enriched and improved with new crypto primitives, and
• access to those primitives has been improved by introducing a sophisticated new cryptographic provider called EverCrypt.

In this blog post, we’ll survey

• what the HACL* crypographic library offers,
• how the cryptographic provider EverCrypt can enhance it, and
• the scaffolding we use to efficiently and reliably invoke these powerful tools from within the Tezos Octez implementation.

2. The HACL* library

2.1 Quick, correct, and compatible: pick three

HACL* is a cryptographic library¹ offering a comprehensive collection of cryptographic primitives (we give three examples below).

HACL* is complex, safety-critical code. Accordingly, it is written in and formally verified using the F* language, and then extracted (compiled) to correct and efficient C using KreMLin, a tool which translates a subset of F* to C. KreMLin also facilitates using the generated C code in OCaml projects — such as the Tezos Octez implementation — by automatically building the scaffolding that developers would otherwise write themselves.

The resulting code offers three formal safety guarantees:

1. Functional correctness: the code’s behaviour complies with its specification.
2. Memory safety: memory is managed correctly — so no buffer overflows, dereferencing null pointers, accessing memory after it has been freed, etc.
3. Secret independence: the C instructions executed, in what order, and any memory accesses, do not depend on any secret values. This protects against timing attacks that might slurp unintended information.

For more details see the original HACL* paper.

The point of this toolstack is that it gives us three important properties which it is far from trivial to reconcile:

1. Safety guarantees as described above, while
2. retaining the state-of-the-art performance required of a cryptographic library in a real-world system, and
3. safely interfacing with the code from within OCaml.

2.2 Three cryptographic primitives

The Tezos Octez implementation has been using HACL* since before its launch, and Nomadic Labs has been actively supporting the continued development of HACL*: via grants to the Prosecco team at Inria Paris; and through the work of engineers at Nomadic.

HACL* offers implementations for all but one² of the core crytographic primitives used by the Nomadic Labs Octez implementation of Tezos.

Let’s survey three examples, which are cryptographic primitives recently introduced into HACL* and relevant to the Tezos implementation:

2.2.1 P-256

P-256 (also called secp256r1) is an elliptic curve signature algorithm and one of the three signature schemes supported in Tezos: P-256; Ed25519; and secp256k1. P-256 is a NIST standard with wide industry support. It allows interoperability with HSMs (hardware security modules), including hardware wallets and Apple’s Secure Enclave.

Any Tezos address generated with P-256 starts with tz3.

A verified implementation of P-256 by the Prosecco team is now in HACL* and replaces our previous library.

2.2.2 SHA-3

Version 1 of the Tezos protocol environment introduced three hash functions based on the Keccak algorithm:

• SHA3-256 and SHA3-512 from the official NIST SHA-3 standard, and
• Keccak256, another variation of the Keccak algorithm, which is the hash function used in Ethereum.

Starting with the Edo protocol upgrade, these three hash functions are available as Michelson opcodes, alongside the previously-present hash functions BLAKE2 and SHA-256 and SHA-512 (which are two versions of SHA-2).

2.2.3 BLAKE2

BLAKE2 is the main hash function of the Tezos protocol. BLAKE2 hashes everything from individual keys and messages, to whole blocks.³

We now use BLAKE2 via its new HACL* implementation. This gives us the three formal safety guarantees above, and furthermore HACL* offers

• a portable C implementation of BLAKE2 which runs on any platform, and
• a faster vectorized implementation which assumes Intel’s Advanced Vector Extensions 2 (AVX2), which offer CPU instructions for SIMD (single instruction, multiple data) parallelism.

Modern cryptographic algorithms, including BLAKE2, are often designed from the ground up to allow implementors to make certain optimizations where possible, such as using hardware features like AVX2 or SIMD mentioned above where the hardware supports this. See a paper on how this fits into HACL*’s verification pipeline: for example, the SIMD implementation is around 30% faster than the non-SIMD one.⁴

3. EverCrypt: an API for HACL* (and more)

3.1 How EverCrypt enhances HACL*

Having a great library like HACL* is one thing. But how to package its features for developers to efficiently deploy in working code? This is where EverCrypt can help.

EverCrypt is a cryptographic provider that bundles the cryptographic primitives present in HACL* into a unified package. EverCrypt — which like HACL* is written in F* and extracted to correct and efficient C using KreMLin — does not replace HACL* so much as provide an additional interface to access the suite of cryptographic primitives offered by HACL*. EverCrypt also bundles routines written in highly-optimized assembly verified with a tool called Vale.⁵

We can sum this up as follows:

• HACL* is a cryptographic library.
• EverCrypt is a cryptographic provider.

3.2 Advantages of having a cryptographic provider

In practice, accessing cryptographic primitives through EverCrypt offers two advantages over accessing them directly (e.g. using HACL*): multiplexing and agile interfaces.

• EverCrypt provides multiplexing:

  Multiplexing means that EverCrypt automatically chooses the fastest available implementation of a given primitive, with no input required from the developer.

  HACL* may offer multiple implementations of some cryptographic algorithms. In the case of BLAKE2 there is a choice between

  • a C implementation that is portable and runs on all platforms, and
  • a faster but less portable vectorized implementation that only works on some platforms.

  For other primitives, there might be a choice between a portable C implementation, and one that uses verified assembly.

• EverCrypt provides agile interfaces:

  EverCrypt offers interfaces that group algorithms that perfom the same general function, e.g. hashing or HMAC. Users call a single function hash and pass the name of specific algorithm desired as a parameter. EverCrypt will then also multiplex to choose the specific implementation of that algorithm.⁶

See this paper for a much more in-depth look at how EverCrypt works and how it supports the development of verified applications.

3.3 The OCaml API

So now we have a cryptographic library (HACL*) and a cryptographic provider (EverCrypt).

There remains a technical issue: calling C functions (like those of HACL* and EveryCrypt) from an OCaml application (like Octez). How best to call a C function from OCaml?

It depends! One common mechanism is a foreign function interface (FFI). The OCaml FFI allows developers to call C functions; it’s up to the developer to write a binding that matches the signature of the C function, and to manage the relevant memory.

Interfacing with an external library using the OCaml FFI works, but it can be error-prone, time-consuming, and can duplicate effort for each project that uses the external library.

To ameliorate this and facilitate adoption in the OCaml ecosystem, EverCrypt and HACL* support an OCaml API primarily developed by Nomadic Labs. Released as the hacl-star package on opam, this provides an idiomatic, high-level interface to the EverCrypt and HACL* APIs. Starting with the recently-released version 0.4, the API is also fully documented.

As is often the case in programming, a more convenient interface is also a safer one, and hacl-star offers safety benefits compared to binding with the C code directly:

1. The lower-level bindings which interact directly with the C code are automatically generated as part of the compilation of F* code to C and are thus valid by construction with respect to the C code.
2. In the higher-level interface, all function calls check the preconditions that these functions have in F*. The formal guarantees of the verified code only hold if the arguments satisfy these preconditions (such as buffers being a certain length or not passing the same buffer as multiple arguments). This prevents developers from using the API incorrectly, and is therefore safer.

The rest of this blog post dives into a description of how the tools above actually get invoked in the Octez codebase. We are proud of our code and would love you to read this — but you are also welcome to skip to the further reading!

4. A deep dive into the OCaml API

The OCaml API is split into

• a low-level part called hacl-star-raw (this contains the actual cryptography) and
• a high-level idiomatic interface hacl-star (this makes the low-level part much easier to use).

Let’s look in more detail at how hacl-star-raw replaces manually-written bindings with automatically generated ones, and how hacl-star builds on top of this to offer a convenient, safer API.

4.1 The low-level API hacl-star-raw

Consider the example of the SHA-256 function from HACL*. Its C signature is:

void Hacl_Hash_SHA2_hash_256(uint8_t *input, uint32_t input_len, uint8_t *dst);

To call it from OCaml we can write a C stub file and match the C types with compatible OCaml FFI types:

#include <caml/mlvalues.h>
#include <caml/bigarray.h>
#include "Hacl_Hash.h"

CAMLprim value ml_Hacl_Hash_SHA2_hash_256(value input, value input_len, value dst) {
    Hacl_Hash_SHA2_hash_256(String_val(input),
                            Int_val(input_len)
                            String_val(dst));
    return Val_unit;
}

Then we can bind this external function to an OCaml function which we can call in the rest of the code as we would any OCaml function:

external sha2_256_hash : Bytes.t -> int -> Bytes.t -> unit =
    "ml_Hacl_Hash_SHA2_hash_256" [@@noalloc]

However, there’s a simpler way to write bindings.

Using the Ctypes library, we can just write OCaml declarations for the C functions that we want to bind, and the library takes care of the rest. A Ctypes declaration for the SHA-256 example above would look like this:

open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
  struct
    open F

    let hacl_Hash_SHA2_hash_256 =
      foreign "Hacl_Hash_SHA2_hash_256"
        (ocaml_bytes @-> uint32_t @-> ocaml_bytes @-> returning void)

end

This is cleaner than before, but we’ve only bound a single function – the SHA-256 hash. We would need to write one such binding for every function from the C library that we want to use in OCaml.

We now take this a step further by having the KreMLin tool automatically generate these Ctypes declarations, at the same time as the C code. This automation saves time and effort and furthermore it ensures that the signatures are correct with respect to the original F* code and the extracted C code, and that they remain in sync when the F* code changes.

This functionality in KreMLin can be fine-tuned,

• allowing users to specify which of the resulting C modules will come with Ctypes bindings, and
• correctly inferring which dependencies also need to be bound.

The output is a collection of bindings that resemble the snippet above, along with the required Ctypes boilerplate and a .depend file listing dependencies between the generated bindings to be used as part of the build.

Thus, we generate bindings for the entirety of the EverCrypt/HACL* code every time a new snapshot is produced. This is then all packaged as the hacl-star-raw opam package.

4.2 The high-level API hacl-star

hacl-star-raw is better than writing C bindings by hand, but it still offers a low-level, C style interface to the library.

To complement this we developed a handwritten idiomatic OCaml API. This further improves convenience and safety; primarily because the preconditions of the original F* functions (which are lost when compiling the F* code to C) can be enforced at runtime.

To illustrate, let’s look at the original F* signature (permalink) of the SHA-256 function above:

module B = LowStar.Buffer

let hash_st (a: hash_alg) =
  input:B.buffer uint8 ->
  input_len:size_t { B.length input = v input_len } ->
  dst:hash_t a->
  ST.Stack unit
    (requires (fun h ->
      B.live h input /\
      B.live h dst /\
      B.disjoint input dst /\
      B.length input <= max_input_length a))
    (ensures (fun h0 _ h1 ->
      B.(modifies (loc_buffer dst) h0 h1) /\
      Seq.equal (B.as_seq h1 dst) (Spec.Agile.Hash.hash a (B.as_seq h0 input))))

[...]

val hash_256: hash_st SHA2_256

Let’s break hash_st down:

1. We can see that hash_256 is an instantiation of a generic SHA-2 function sha_st, parameterized by the specific algorithm. This is a pervasive pattern throughout the library.

2. Just as we specified in the OCaml binding above, it takes three arguments:

   1. input, which is a uint8_t buffer,
   2. input_len, with a refinement specifying that the size of input must be equal to input_len, and
   3. dst of type hash_t a, which is also a uint8_t buffer of the correct digest size for algorithm a.

Glossing over some of the details, we see in the requires clause above that the function hash_st (and therefore hash_256 too) has certain liveness, disjointness, and other preconditions. In particular:

• the input buffer must be smaller than the maximum allowed size for the specific algorithm (B.length input <= max_input_length a), and
• hash_256 is guaranteed to modify only dst, and dst will contain the result of the hash as defined in the spec.

In the original F* these preconditions are statically checked when compiling code that calls hash_256. But in OCaml we only get to work with the extracted C code, in which this information has been erased (as seen in the C signature of the function). Users of the C library must make sure that the arguments they pass respect the original preconditions of these functions.

In the OCaml API, we do check all of these preconditions at runtime. For example, this is what the functor used internally for hash functions roughly looks like:

module Make_HashFunction (C: Buffer)
    (Impl : sig
       val hash_alg : alg
       val hash : C.buf -> uint32 -> C.buf -> unit
     end)
= struct
    let hash ~msg ~digest =
      check_max_input_len Impl.hash_alg (C.size msg);
      assert (C.size digest = digest_len Impl.hash_alg);
      assert (C.disjoint msg digest);
      Impl.hash (C.ctypes_buf msg) (C.size_uint32 msg) (C.ctypes_buf digest)
end

Make_HashFunction is parameterized both by

• C, which is the data type we want to use to represent C buffers (we currently use Bytes, but Bigstring is also possible), and
• Impl, the specific hash function implementation.

Before calling the bound C function, the buffers are checked to have the correct size and to be disjoint (which for Bytes simply means checking for inequality).

4.3 Using the high-level API

We’ve seen how the OCaml library comes together, from the HACL* C code, to the low-level Ctypes bindings, to the idiomatic OCaml API. Now let’s look at how it can be used.

Most cryptographic algorithms exposed through this OCaml API can be called in more than one way, to suit different use cases. Our SHA-256 example above will conveniently illustrate them.

The API is split in two interfaces:

• Hacl, which directly exposes the portable C implementations
• EverCrypt, which exposes the agile and/or multiplexing interfaces

In Hacl, SHA-256 can be used in two styles:

1. Hacl.SHA2_256.hash which takes a buffer representing the message and returns the digest
2. Hacl.SHA2_256.Noalloc.hash which, more in keeping with the C style, takes as inputs both the message buffer and the output buffer into which the digest will be written

The first style is usually more convenient, but the second style can be useful in cases where an output buffer has already been allocated and we don’t want to allocate a new one. The choice is the programmer’s to make: most modules in Hacl and EverCrypt offer both styles above.

EverCrypt offers three further options:

1. EverCrypt.SHA2_256 is an identical interface to Hacl.SHA2_256, but with a different underlying implementation: Hacl.SHA2_256 uses the portable C implementation of SHA-256; whereas EverCrypt.SHA2_256 uses the multiplexing EverCrypt interface which automatically uses code relying on Intel SHA extensions if the architecture supports it.

2. EverCrypt.Hash.hash is an agile and multiplexing interface to all hashing functions supported in EverCrypt and it is parameterized by the hashing algorithm:

   
       let digest = EverCrypt.Hash.hash ~alg:SHA2_256 ~msg
       

3. The EverCrypt.Hash incremental hashing interface can be used when we need to update the internal state repeatedly before generating a digest:

   
       let st = EverCrypt.Hash.init ~alg:SHA2_256 in
       EverCrypt.Hash.update ~st ~msg; (* can be called multiple times *)
       let digest = EverCrypt.Hash.finish ~st
       

5. Further reading

Taken together, these changes constitute a significant investment in improving our codebase, which has brought us up-to-date with the best technology available and allowed us to increase reliability and flexibility, without compromising on performance.

You can read further in:

• The OCaml API documentation.
• For web development, an official JavaScript API is available, exposing the version of HACL* extracted to WebAssembly.
• For more examples using other algorithms, see the unit tests.
• EverCrypt is free and open-source, for you to use.
• See this paper for a more in-depth look at how EverCrypt works and how it supports the development of verified applications.

We hope this survey has been informative and may inspire you to use EverCrypt in your own OCaml projects too!

Acknowledgements

Thanks to Karthikeyan Bhargavan, Natalia Kulatova, and Marina Polubelova of the Prosecco team at INRIA, and to Jonathan Protzenko of Microsoft Research, for their help, support, and collaboration. At Nomadic Labs, the work reported on in this article was carried out principally by Victor Dumitrescu.