mit-plv / fiat-crypto

Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives =================================================================================== Building -------- [![Release][release-shield]][release-link] [![Zulip][zulip-shield]][zulip-link] [![Rust Crate][crate-shield]][crate-link] [![Go Reference][pkg.go-shield]][pkg.go-link] [release-shield]: https://img.shields.io/github/v/release/mit-plv/fiat-crypto.svg?logo=github&include_prereleases [release-link]: https://github.com/mit-plv/fiat-crypto/releases [zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-informational.svg [zulip-link]: https://coq.zulipchat.com/#narrow/stream/247791-fiat-crypto [crate-shield]: https://img.shields.io/crates/v/fiat-crypto.svg [crate-link]: https://crates.io/crates/fiat-crypto [pkg.go-shield]: https://pkg.go.dev/badge/github.com/mit-plv/fiat-crypto/fiat-go.svg [pkg.go-link]: https://pkg.go.dev/github.com/mit-plv/fiat-crypto/fiat-go 🌐 Try out synthesis on the web! (Supported by compilation.) This repository requires Coq 8.20 or later, including OCaml libraries. If you install Coq from Ubuntu aptitude packages, you need in addition to . Note that in some cases (such as installing Coq via homebrew on Mac), you may also need to install (for ). The extracted OCaml code for the standalone binaries requires OCaml 4.08 or later. We suggest downloading the latest version of Coq. Generation of JSON code via the Makefile also requires . Alternatively, choose your package-manager to install dependencies: Package Manager | Command Line Invocation | --|--| Aptitude (Ubuntu / Debian) | | Homebrew (OS X) | | Pacman (Archlinux) | | APK (Alpine) | | You can clone this repository with git clone --recursive https://github.com/mit-plv/fiat-crypto.git Git submodules are used for some dependencies. If you did not clone with , run git submodule update --init --recursive from inside the repository. Then run: make You can check out our CI to see how long the build should take; as of the last update to this line in the README, it takes about 1h10m to run on Coq 8.11.1. If you want to build only the command-line binaries used for generating code, you can save a bit of time by making only the target with make standalone-unified-ocaml Usage (Generating C Files) -------------------------- The Coq development builds binary compilers that generate code using some implementation strategy. The parameters (modulus, hardware multiplication input bitwidth, etc.) are specified on the command line of the compiler. The generated C code is written to standard output. A collection of C files for popular curves can be made with make c-files The C files will appear in . Just the compilers generating these C files can be made with make standalone-ocaml or for compiler binaries generated with Haskell, or for both the Haskell and OCaml compiler binaries. The binaries are located in and respectively. There is one compiler binary for all implementation strategies: • This binary takes arguments for the strategy: • - • - • - Passing no arguments, or passing or (or any other invalid arguments) will result in a usage message being printed. These binaries output C code on stdout. Here are some examples of ways to invoke the binaries (from the directories that they live in): # Generate code for 2^255-19 ./fiat_crypto unsaturated-solinas '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c # 1 ./fiat_crypto unsaturated-solinas '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c # 2 # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1) ./fiat_crypto word-by-word-montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c # 3 ./fiat_crypto word-by-word-montgomery 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c # 4 Try out the above on the web [🌐 1 ][web-1-link] [🌐 2 ][web-2-link] [🌐 3 ][web-3-link] [🌐 4 ][web-4-link]. You can find more examples in the . [web-1-link]: https://mit-plv.github.io/fiat-crypto/?argv=%5B%22unsaturated-solinas%22%2C%2225519%22%2C%2264%22%2C%225%22%2C%222%5E255-19%22%2C%22carry_mul%22%2C%22carry_square%22%2C%22carry_scmul121666%22%2C%22carry%22%2C%22add%22%2C%22sub%22%2C%22opp%22%2C%22selectznz%22%2C%22to_bytes%22%2C%22from_bytes%22%5D&interactive [web-2-link]: https://mit-plv.github.io/fiat-crypto/?argv=%5B%22unsaturated-solinas%22%2C%2225519%22%2C%2232%22%2C%2210%22%2C%222%5E255-19%22%2C%22carry_mul%22%2C%22carry_square%22%2C%22carry_scmul121666%22%2C%22carry%22%2C%22add%22%2C%22sub%22%2C%22opp%22%2C%22selectznz%22%2C%22to_bytes%22%2C%22from_bytes%22%5D&interactive [web-3-link]: https://mit-plv.github.io/fiat-crypto/?argv=%5B%22word-by-word-montgomery%22%2C%22p256%22%2C%2232%22%2C%222%5E256-2%5E224%2B2%5E192%2B2%5E96-1%22%5D&interactive [web-4-link]: https://mit-plv.github.io/fiat-crypto/?argv=%5B%22word-by-word-montgomery%22%2C%22p256%22%2C%2264%22%2C%222%5E256-2%5E224%2B2%5E192%2B2%5E96-1%22%5D&interactive Note that for large primes, you may need to increase the stack size to avoid stack overflows. For example: ulimit -S -s 1048576; ./fiat_crypto word-by-word-montgomery --static gost_512_paramSetB 32 '2^511 + 111' This sets the stack size to 1 GB (= 1024 MB = 1024 * 1024 KB = 1048576 KB) before running the command. As of the last edit of this line, this command takes about an hour to run, but does in fact complete successfully. Without a sufficiently large stack-size, it instead stack overflows. Usage (Generating Bedrock2 Files) --------------------------------- Output is supported to the research language bedrock2. The Coq development builds binary compilers that generate code using some implementation strategy. The parameters (modulus, hardware multiplication input bitwidth, etc.) are specified on the command line of the compiler. The generated bedro…