gebner / noise-star

Verified implementations for the Noise family of protocols

Noise*

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.

Generated Verified Implementations

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.

Build Instructions

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 -j

Then, navigate to one of the directories you are interested in:

cd api-IKpsk2/IKpsk2_25519_ChaChaPoly_SHA256
make -j

In order to link a final executable, remember to pass -L$HACL-HOME/dist/gcc-compatible -levercrypt to the linker (after -lnoiseapi).

Examples

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).

Verified Implementation

The generic implementation formally verified with F* is in src/.

Specific Choices of Cryptographic Implementations

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.

Paper

The results of this work have been published at S&P 2022. The paper (long version) is available here.