AUCurves synthesizes formally verified implementations of pairing-friendly elliptic curves. Currently, it produces implementations of the groups G1 and G2 of the elliptic curve BLS12-381, as well as the quadratic field extension arithmetic underlying G2.
It expands the infrastructure provided by the Fiat-Crypto and Bedrock2 projects. We use the base field arithmetic synthesized by Fiat-Crypto as atomic building blocks in our implementations, and use Bedrock2's "ExprImp" as an intermediate language that allows us to proof correctness of our implementations, while abstracting over a number of parameters such as prime modulos, system bitwidth and curve-defining parameters.
More information on the pipeline can be found in the literature below.
Can be found here.
Briefly, the implementation is verified for:
- Memory Safety, since it produces rust
- Functional Correctness against a formal specification written in both Coq and hacspec
- Secret Independence, at least for the code produced by fiat-cryptography, as this is straight-line code.
AUCurves can produce both C and rust code.
The libcrux library currently uses the following verified implementations from AUCurves:
- BLS12-381 - rust
We pull code from the AUCurves and run the verification on the whole repository using the provided Makefile. The build process is explained there.
The syntesis of bedrock2 code is verified in Coq. We provide a small file for printing Bedrock2 to rust. This file has not yet been independently audited.
We provide a hacspec specification of the affine groups G1 and G2 of the BLS12-381 elliptic curve as well as the underlying fields. We prove the equivalence between the bedrock and hacspec implementations, by a chain of equivalence proofs. First, the bedrock implementation is proven equivalent to the gallina specification defined in the file MontgomeryCurveSpecs. This is then proven equivalent to the fiat-crypto specification of the projective Weierstrass curve. Fiat-crypto provides a proof that this is equivalent to the affine Weierstrass curve. Finally, this is proven equivalent to the hacspec implementation.
AUCurves and its associated proof methodologies have been published in the following abstract. A longer paper is in preparation:
- Workshop paper: Rasmus Holdsbjerg-Larsen, Bas Spitters, Mikkel Milo, A Verified Pipeline from a Specification Language to Optimized Safe Rust, CoqPL'22, 2022
- Diego Aranha, Rasmus Holdsbjerg-Larsen, Benjamin Salling Hvass, Bas Spitters, Synthesizing High-Assurance Implementations of Pairing Groups, In progress
As stated, AUCurves depends on: