Bug 2213270

Summary: Review Request: rust-fiat-crypto - Correct-by-Construction Code for Cryptographic Primitives
Product: [Fedora] Fedora Reporter: Fabio Valentini <decathorpe>
Component: Package ReviewAssignee: Aleksei Bavshin <alebastr89>
Status: CLOSED RAWHIDE QA Contact: Fedora Extras Quality Assurance <extras-qa>
Severity: unspecified Docs Contact:
Priority: unspecified    
Version: rawhideCC: alebastr89, eclipseo, package-review
Target Milestone: ---Flags: alebastr89: fedora-review+
Target Release: ---   
Hardware: Unspecified   
OS: Unspecified   
Whiteboard:
Fixed In Version: Doc Type: If docs needed, set a value
Doc Text:
Story Points: ---
Clone Of: Environment:
Last Closed: 2023-06-15 13:21:42 UTC Type: ---
Regression: --- Mount Type: ---
Documentation: --- CRM:
Verified Versions: Category: ---
oVirt Team: --- RHEL 7.3 requirements from Atomic Host:
Cloudforms Team: --- Target Upstream Version:
Embargoed:
Bug Depends On:    
Bug Blocks: 2210897    

Description Fabio Valentini 2023-06-07 16:59:07 UTC
Spec URL: https://decathorpe.fedorapeople.org/rust-fiat-crypto.spec
SRPM URL: https://decathorpe.fedorapeople.org/rust-fiat-crypto-0.1.20-1.fc38.src.rpm

Description:
Correct-by-Construction Code for Cryptographic Primitives.

Fedora Account System Username: decathorpe

Comment 1 Fabio Valentini 2023-06-07 17:12:03 UTC
*** Bug 2005536 has been marked as a duplicate of this bug. ***

Comment 2 Fabio Valentini 2023-06-07 17:15:31 UTC
Note: According to discussion in the original bug (RHBZ#2005536) and the Legal mailing list, this package is built from sources from which all code related to the p434 elliptic curve has been removed, since it has not yet been approved as permissible in Fedora.

Comment 3 Aleksei Bavshin 2023-06-13 06:13:45 UTC
> git apply ../0001-remove-references-to-code-related-to-the-p434-curve.patch

The patch is missing from the srpm, making the clean archive generation not reproducible.

Not sure if we should follow the policy for pregenerated code[1] here. The situation fits, but it would make the packaging insanely cumbersome even without regenerating the code :(

[1]: https://docs.fedoraproject.org/en-US/packaging-guidelines/what-can-be-packaged/#pregenerated-code

Comment 4 Fabio Valentini 2023-06-13 08:45:36 UTC
Good catch, I will include the patch as a Source file.

===

The generated code guidelines don't really apply here, as far as I understand. The code is not generated from other sources, but from ... well, prime numbers and a few parameters, and these are documented at the top of each source file.

Additionally, packaging the whole fiat crypto framework (which includes support for a dozen languages, not just Rust). It's also written in OCaml (but already packaged for Fedora): https://src.fedoraproject.org/rpms/coq

So I'd say the relevant parts of the pregenerated sources are fulfilled:

- generated by free software that is available in Fedora
- process would be reproducible since input parameters are documented (but I'm not interested in packaging the tooling itself, because that looks like a whole different beast)

Comment 5 Aleksei Bavshin 2023-06-15 05:15:25 UTC
fiat-crypto is an interesting thing. It's, of course, way over my head (I think we need someone like jjames to translate things to a regular English), but I've got a surface grasp of the papers referenced

The team behind fiat-crypto implemented several things:
 1. a formally verified implementation of a set of operations on mathematical primitives used in ECC (Montgomery curves, Solinas primes, etc...) in Coq (a functional language with formal proof capabilities, which is commonly used to implement said formally verified algorithms)
 2. a tooling to rewrite the algorithm of choice in a selected language, specialized for a given set of constants.
 3. a proof that the operation in 2 preserves the properties of an already verified algorithm.
    I'd say they did that by implementing things in Coq, again, but my language comprehension skills struggle with an intermediate level Haskell so I can't read their sources.

Well, if we twist a point of view a bit, we can consider 1 a part of the tooling and not a source code that gets transformed into Rust. With that interpretation I'm going to agree and approve this.

(I'm finding the part with regenerating the archive with `cargo package` curious, but I guess that creates some metadata required by cargo).

---

Please, ensure that the clean archive can be regenerated from the dist-git or srpm before import.

Comment 6 Fabio Valentini 2023-06-15 12:39:50 UTC
Thanks for the review! Yeah, I agree, this is an interesting (but a bit unusual) project. But I think the way it's done now is the best that can be done with reasonable effort. The part about re-packaging the ".crate" file only ensures that the correct files are included in the tarball (.crate files are just .tar.gz) and that the crate metadata / Cargo.toml remains valid. I will ensure that the "cleaned" .crate file can be produced from dist-git contents before I import and build things.

Comment 7 Fedora Admin user for bugzilla script actions 2023-06-15 12:40:15 UTC
The Pagure repository was created at https://src.fedoraproject.org/rpms/rust-fiat-crypto

Comment 8 Fabio Valentini 2023-06-15 13:21:42 UTC
Imported and built:
https://bodhi.fedoraproject.org/updates/FEDORA-2023-7bf086d1d2