Serial backends w/formally-verified field arithmetic for 32 & 64 bits #342
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This uses https://github.com/calibra/rust-curve25519-fiat/ to implement a new 64bit serial backend for dalek. Co-authored-by: Zoe Parakevopoulou <zoopar@fb.com>
Renames fiat backend directory to fiat_u64 and does the additional plumbing required to make fiat_{u32, u64}_backend equal alternatives.
Adds a few comments.
huitseeker
force-pushed
the
fiat4_with_u32
branch
from
82f207f
to
35ece27
Compare
huitseeker
force-pushed
the
fiat4_with_u32
branch
from
35ece27
to
d1ed427
Compare
isislovecruft
approved these changes
Apr 13, 2021
There was a problem hiding this comment.
Thanks @huitseeker! I'm pleasantly surprised by how small the LOC footprint is to add Fiat support. Hopefully I'll get more time at some point to dig into their output Rust code again and see if there's other optimisations to be made, but ~15% slow down is pretty impressive.
huitseeker
added a commit
to huitseeker/ed25519-dalek
that referenced
this pull request
May 3, 2021
This allows the fiat backends introduced in [curve25519-dalek/#342](dalek-cryptography/curve25519-dalek#342) to be used from an ed25519 import without cumbersome overrides.
huitseeker
added a commit
to huitseeker/x25519-dalek
that referenced
this pull request
May 3, 2021
This allows the fiat backends introduced in [curve25519-dalek/#342](dalek-cryptography/curve25519-dalek#342) to be used from an x25519 import without cumbersome overrides.
|
@isislovecruft @huitseeker This paper speeds up curve25519: https://cs.adelaide.edu.au/~yval/pdfs/KuepperEGSWCCGWY23.pdf They say it's the fastest implementation on Intel i9 12G. |
mkj
pushed a commit
to mkj/ed25519-dalek
that referenced
this pull request
Mar 29, 2023
This allows the fiat backends introduced in [curve25519-dalek/#342](dalek-cryptography/curve25519-dalek#342) to be used from an ed25519 import without cumbersome overrides.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Contribution
This sets up two non-default serial backends,
fiat_u32_backendandfiat_u64_backend. Those backends use field arithmetic generated in Rust from proofs of functional correctness checked by the Coq theorem prover, as part of the fiat-crypto project. More details can be found in the fiat-crypto paper.This Rust code is located in the fiat-crypto crate maintained by fiat-crypto team, and the present PR simply provides the plumbing necessary to integrate with curve25519-dalek's backend architecture.
Motivation
This contribution could offer to curve25519-dalek an opt-in backend providing a "gold standard" of correctness, and already used for this reason in Wireguard, Go, BoringSSL, etc. Dalek developers could also use these backends as a fuzzing target, in order to check the correctness upcoming optimizations of the serial code.
Performance
The performance is lower, but within a single digit of the existing basic operations, and only rises to a ~15% slowdown on composite operations.
https://gist.github.com/huitseeker/d3c7a30fa90fdb43d2815eb4b63a7205
Maintenability
The backends collectively comprise less than 600 SLoC. They reuse the scalar and constant definitions to offer a minimal code increment.
The fiat-crypto project already runs the curve25519-dalek unit tests on the fiat_u64 backend as part of its CI. Hence the probability that it would break this backend is very low. I would be happy to contribute the few lines of adjustments necessary there to make it run on the fiat_u32 backend as well, should the present PR be merged.