This fork was a failed attempt to make updates so that NOISE* can work with the latest version of HACL*. I'm archiving it in case someone else can make use of it.
The verifier is getting stuck on mk_device_p_create_from_secret_has_s in Impl.Noise.API.Device.fst and nothing I have tried has helped. And even if I eventually get it to work it seems likely I will run into additional issues that I don't understand.
Maybe someone with more F* can get it to work.
This repository contains formally verified implementations of all 59 protocols in the Noise family, in C. Each implementation manages a state machine, a peer list, and offers a high-level defensive API that prevents user errors. See our paper for more details. We rely on verified cryptographic primitives provided by the HACL* project, although it should not be hard to edit the C code to call the library of your choice.
The generated implementations are in /noise-all.
This directory contains a subdirectory for each protocol of the Noise family,
itself divided into further subdirectories for the various choices of cipher suites.
For instance, the implementation of protocol IKpsk2, instantiated with Curve25519, ChaChaPoly and
SHA256, is in /noise-all/api-IKpsk2/IKpsk2_25519_ChaChaPoly_SHA256.
Clone and build HACL*.
git checkout https://github.com/project-everest/hacl-star
cd hacl-star
export HACL_HOME=$(pwd)
cd dist/gcc-compatible
make -jThen, navigate to one of the directories you are interested in:
cd api-IKpsk2/IKpsk2_25519_ChaChaPoly_SHA256
make -jIn order to link a final executable, remember to pass
-L$HACL-HOME/dist/gcc-compatible -levercrypt to the linker (after
-lnoiseapi).
See examples for an example of usuage of the API.
Building and running the example simply requires executing make in the subdirectory,
after HACL* and Noise* have been properly built.
The example uses IKpsk2, with Curve25519, ChaChaPoly and SHA256 (non-optimized implementations).
The generic implementation formally verified with F*
is in src/.
There are a lot of cipher suites, and most of the cryptographic primitives have several (optimized) implementations. Because there are too many of them, we only generate implementations for a limited choice of cryptographic primitive implementations. If you desire a specific choice of implementations made available by the Hacl* library, feel free to contact the authors.
The results of this work have been published at S&P 2022. The paper (long version) is available here.