Cryptographic Primitive Code Generation by Fiat
Coq C Shell Python Assembly Makefile Other
Clone or download
Permalink
Failed to load latest commit information.
bbv @ 8eb02b5 git submodule update May 31, 2018
coqprime @ be32c40 Bump coqprime Jul 10, 2018
etc Add git diff for better debugging of C-file issues Jul 21, 2018
liblow Fix liblow.h for cmovznz64 Jan 15, 2018
measurements pick best implementation, not first Dec 1, 2017
src Montgomery reduction in new pipeline Jul 21, 2018
third_party Pass -mbmi2 to gcc Jan 19, 2018
.dir-locals.el coqprime in COQPATH (closes #269) Feb 24, 2018
.gitignore Montgomery reduction in new pipeline Jul 21, 2018
.gitmodules relocate and prove an admit Apr 9, 2018
.mailmap Update .mailmap Apr 3, 2018
.travis.yml Add some primes to be synthesized Jul 21, 2018
AUTHORS update licensing information Jun 25, 2016
CONTRIBUTORS Prove montladder correct in the zero case. Jan 8, 2018
LICENSE Strip trailing whitespace Jun 2, 2017
Makefile Add some primes to be synthesized Jul 21, 2018
README.md Update README.md Nov 15, 2017
_CoqProject Montgomery reduction in new pipeline Jul 21, 2018
capture.sh capture.sh require constant TSC Jul 5, 2017
crypto-defects.md Update crypto-defects.md Nov 16, 2017
curve25519_32.c Montgomery reduction in new pipeline Jul 21, 2018
curve25519_64.c Montgomery reduction in new pipeline Jul 21, 2018
expansion.md Strip trailing whitespace Jun 2, 2017
extract-function-header.sh Add femul,fesqure for C32 Sep 21, 2017
extract-function.sh Add femul,fesqure for C32 Sep 21, 2017
failures.txt triage synthesis failures Nov 7, 2017
folkwisdom.md Work around bad design in Coq Jul 20, 2016
generate_parameters.py Pass -mbmi2 to gcc Jan 19, 2018
measure.c Don't inline measure_helper Sep 16, 2017
optimizations.md Strip trailing whitespace Jun 2, 2017
p224_32.c Add some primes to be synthesized Jul 21, 2018
p224_64.c Add some primes to be synthesized Jul 21, 2018
p256_32.c Add some primes to be synthesized Jul 21, 2018
p256_64.c Add some primes to be synthesized Jul 21, 2018
p384_32.c Add some primes to be synthesized Jul 21, 2018
p384_64.c Add some primes to be synthesized Jul 21, 2018
p521_32.c Add some primes to be synthesized Jul 21, 2018
p521_64.c Add some primes to be synthesized Jul 21, 2018
primes.txt primes.txt: remove a curve25519 alias, add 64-bit secp256 Nov 6, 2017
regenerate-curves.sh Add a regenerate-curves target Nov 17, 2017
register-allocate.py Use imul (not sure if it's better...) Sep 13, 2017
secp256k1_32.c Add some primes to be synthesized Jul 21, 2018
secp256k1_64.c Add some primes to be synthesized Jul 21, 2018
synthesis-parameters.txt rename-everything Apr 7, 2017

README.md

Build Status

Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives

Build Requirements

This repository requires:

  • To build the proofs and almost-C-like outputs: Coq 8.7 (tested with 8.7.0)

To build (if your COQPATH variable is empty):

make

To build:

export COQPATH="$(pwd)/coqprime${COQPATH:+:}$COQPATH"
make

To build a representative subset, instead of make, run

    make selected-specific-display non-specific

The core library (target nonautogenerated-specific-display non-specific) is expected to build within about one hour (in serial, on a particularly fast machine), within about 3.5--4 GB of RAM, plus an additional 1-5 minutes to run coqdep on all of our files. Of the additional curves, 90% finish within 5 minutes per file, and 99% finish within 15 minutes per file (though some take upwards of 50 GB of RAM). These 99% of curves together take about 60 hours.

  • To build the C outputs: Python (2 or 3)

To build:

    make c

or, for a representative subset,

    make selected-c
  • To build and run the binaries, gcc (7.1.2; or 7.1.1 with -fno-peephole2) or clang of a new enough version to support the appropriate compiler intrinsics.

To build and run:

    make test bench

or, for a representative subset,

    make selected-test selected-bench

Exploring the code

Push-button synthesis

To add a new prime, add a new line to primes.txt with your prime. Then run

    ./generate_parameters.py; ./src/Specific/remake_curves.sh

You will see a bunch of lines starting with git add; any .v files that show up in these lines must be added to _CoqProject. (If you are working in the git repository, you may simply run the git add lines, and then run make update-_CoqProject.) Note that the directory structure involves a textual representation of your prime, call it ${REPRESENTATION_OF_YOUR_PRIME}. To build, you can run

    make src/Specific/{montgomery,solinas}{32,64}_${REPRESENTATION_OF_YOUR_PRIME}/fibe

This will build all the necessary .vo and .c files, as well as the fibe binary, which is automatically run when you make bench or make test.

Curve Correctness Theorems

Specifications live in src/Spec, e.g., src/Spec/Ed25519.v. Some selected cuve-level proofs live in

Arithmetic Core

Generic mathematical optimization strategies live in src/Arithmetic. Good examples include

Demo of Synthesis

The idea of the synthesis process is demoed in src/Demo.v.

Actual Synthesis

The curve-specific synthesis framework lives in src/Specific/Framework.

Example Output

The c output lives in the various subfolders of src/Specific. For example, C-like code for X25519 multiplication on 64-bit machines lives in src/Specific/X25519/C64/femulDisplay.log, which is generated from src/Specific/X25519/C64/femulDisplay.v, which in turn uses synthesis run in src/Specific/X25519/C64/femul.v. The c target turns this into src/Specific/X25519/C64/femul.c.

Footnotes

¹ This magic comes in the form of calls to transparent_abstract, packaged up in some tactics in src/Util/Tactics/CacheTerm.v.