Tracking uses of fiat-crypto

[JasonGross]

Maybe we should create a wiki page tracking uses of fiat-crypto?

The ones I'm aware of:

• BoringSSL / https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/fiat/ / https://boringssl.googlesource.com/boringssl/+/47b1e39042bc3208771a8d947f1a1ed2fe5f3d8b/third_party/fiat/ / https://web.archive.org/web/20201218200341/https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/fiat/
• Chrome via BoringSSL
• Facebook LibreCoin? (Rust)
• Go language (crypto: import fiat-crypto implementations golang/go#40171)
• ECCKiila (https://gitlab.com/nisec/ecckiila)
• WireGuard (https://www.wireguard.com/formal-verification/)
• Firefox? (32-bit only?) (link?)
• others?

[huitseeker]

Diem via https://github.com/novifinancial/curve25519-dalek/tree/fiat3

[vincenthz]

my modest addition : eccoxide

[chjj]

libtorsion

[huitseeker]

Re: Firefox 32-bits,
https://blog.mozilla.org/security/2020/07/06/performance-improvements-via-formally-verified-cryptography-in-firefox/

[bbbrumley]

• NSS for P-384 and P-521, both 32 and 64 bit builds.
• Firefox via NSS
• GOST engine for eight standardized curves

Yes these are ECCKiila deployments but IMO you def should track them for your own visibility.

[hannesm]

In MirageOS (OCaml) we use fiat (the exported C source code, bound and wrapped https://github.com/mirage/fiat) for ECDH on P256. This is packaged in opam as fiat-p256 and used by OCaml-TLS - a TLS implementation in pure OCaml).

Upcoming is ECDSA support (to be integrated into X.509, once I find time to figure #885) and "more curves" (P384, P521, secp256k1, Ed448). From the list of "things that would be nice" there's for sure "try the OCaml code extraction and measure speed differences between C and OCaml", and also "provide a build rule to run the extraction on local machine").

[jvz]

I've imported the curve25519 code into https://github.com/o1c-dev/o1c recently. I tried using the Java sources originally, but I couldn't get its output to match the C code, so I'm not sure if that works properly. I did get the C code working after referring to the BoringSSL notes page.

[JasonGross]

It's cool to see how many projects are using fiat-crypto!

I tried using the Java sources originally, but I couldn't get its output to match the C code, so I'm not sure if that works properly

I believe the Java code is only synthesizing 32-bit operations (see #681), so that might be the discrepancy you're hitting. If it's not, please do open an issue, or comment on #707 with an example discrepancy, since we are lacking tests for the Java output (and may have gotten casting wrong).

I did get the C code working after referring to the BoringSSL notes page.

If you think the code could use more comments on how to use it, or if you think the README could benefit from more instructions, please feel free to open an issue or PR.

[jvz]

I tried using curve25519_32.c for comparison with the Java variant. One of the confusing aspects is that the field elements are unpacked from int arrays rather than byte arrays as the other APIs work, though even converting a byte array to that form or manually constructing one gives different results as demoed in https://gist.github.com/jvz/0bd0ff04b47524da8b8aedc16e79a4eb which I've commented in #707.

[jvz]

I just noticed that OpenBSD is using fiat-crypto, though it's somewhat transitive since it's related to WireGuard code.

[dfaranha]

Touting my own horn, but RELIC also supports Fiat-Crypto as a field arithmetic backend.

[huitseeker]

Available directly as a backend in dalek-crypto, as of version 3.1.

[JasonGross]

@huitseeker Nice! 9cb5fdd066d6caea2056f5bb591b2b8390a40224 is not a commit of mit-plv/fiat-crypto, though, and doesn't seem to be in https://github.com/dalek-cryptography/curve25519-dalek nor https://github.com/novifinancial/curve25519-dalek-fiat...

Btw, should we update the CI test of

fiat-crypto/etc/ci/test-fiat-rust-curve25519-dalek.sh

Lines 5 to 17 in a204ed3

	################################################################################
	# Tests for calibra/curve25519-dalek
	################################################################################
	git clone https://github.com/calibra/curve25519-dalek.git --branch=fiat2 curve25519-dalek || exit $?
	pushd curve25519-dalek >/dev/null || exit $?
	cat >> Cargo.toml <<EOF
	[patch.crates-io]
	fiat-crypto = { path = "../fiat-rust" }
	EOF
	cargo test --features="std fiat_u64_backend" --no-default-features || exit $?

?

[jedisct1]

A small addition, that's been using it since day one: ed25519-compact (rust)

It is also planned to be used in the standard library of the Zig programming language, as well as the reference implementation of the standard cryptography interface for WebAssembly using the Zig code.

[hannesm]

coming back here, we in MirageOS (+OCaml) finally have the stack released and in use (for ECDH and ECDSA / Ed25519)-- I published a post about that https://hannes.robur.coop/Posts/EC -- once again thanks for fiat :)

code https://github.com/mirage/mirage-crypto/tree/main/ec (extraction infrastructure https://github.com/mirage/mirage-crypto/tree/main/ec/native)

[armfazh]

Soon-ish CIRCL Go cryptography library.
See cloudflare/circl#252

[brycx]

FWIW, Orion uses fiat-crypto for X25519 in the upcoming release.

Edit: Poly1305 using fiat-crypto is included in the next release.

[apetcher-amazon]

AWS libcrypto incorporates the P-384 code in addition to the curves that are provided by BoringSSL. Addition of P-521 is currently under review.

[andres-erbsen]

https://github.com/Yawning/secp256k1-voi #1444 (comment)

[0x0ece]

Firedancer: https://github.com/firedancer-io/firedancer
(first added here: firedancer-io/firedancer#1311)