Cryptographic signing of platform releases

[palmskog]

To increase the trustworthiness of the platform and allow users to certify that they are installing what they expect, I suggested in a Coq Zulip topic that platform releases should be cryptographically signed by the release manager.

There is a wide spectrum of possible ways to sign releases, going from signing of the GitHub commit for the platform repo associated with a release, to full signing of a special platform opam repository. Fortunately, the latter (arguably more fundamental) approach has been explored at length by @hannesm in his Conex project.

Conex is a utility for verify and attest release integrity and authenticity of community repositories through the use of cryptographic signatures

The ideas behind Conex have been described in blog posts and papers (in reverse chronological order):

• https://hannes.nqsb.io/Posts/Conex
• https://github.com/hannesm/conex-paper/raw/master/paper.pdf
• https://opam.ocaml.org/blog/Signing-the-opam-repository/

According to Hannes, Conex is as of September 2021 not yet ready for deployment at the scale of the Coq platform, but is expected to improve later this year, which could make it viable to use here.

Hannes summarizes the design of Conex as an adaptation of the Update framework for opam:

the signing metadata is part of the opam repository --> an update of the opam repository can be verified (and this is the only place where verification needs to happen)

conex has few dependencies, and will likely be integrated into opam at some point in time

opam has (since 2.0) a so called validation hook https://opam.ocaml.org/doc/Manual.html#configfield-repository-validation -> command which is executed after repository update (but before installing the update of the repository) with the old repo (on disk) and the patch to be applied --> here conex can verify the new repository to be properly signed

[MSoegtropIMC]

@palmskog : do you think singing the github commits (annotated tags) would be sufficient for the time being?

[palmskog]

@MSoegtropIMC annotated tags sound good, but for this to be meaningful I think signing should be done with a personal GPG key that can be independently checked to belong to one's web of trust. For example, I documented how one could recreate/check a Coq release tarball on the Coq Wiki.

[MSoegtropIMC]

Wouldn't simply be signing the tag with a GPG key that is registered with Github sufficient?

[palmskog]

My personal view is that the signing GPG key should have some meaning outside of GitHub for the signing process to be meaningful (i.e., provide some additional trustworthiness over what is already there). For example, the Coq release managers seem to have all signed each other's GPG keys, so if you trust one of the RMs, you can trust all of their signatures.

Maybe we can ask @gares to sign the signing key, or to sign the commit directly? Then you at least have the connection between Coq release signing and Platform signing.

[MSoegtropIMC]

Yes, I can do this key signing with @gares or ask the respective Coq release manager to sign of the Coq Platform tag.

[gares]

Didn't we sign our GPG keys already? I do have a BAC3DD18 in my keyring associated to your email

[gares]

Maybe we can ask @gares to sign the signing key, or to sign the commit directly? Then you at least have the connection between Coq release signing and Platform signing.

I think all devs should cross sign their keys, then git tag -s should just be enough. My key is decently connected (Debian past).

[MSoegtropIMC]

@gares: we did exchange the keys but I don't think that either of use signed the signing keys of the others.

[MSoegtropIMC]

Triage note: all future tags will be signed with the personal GPG key of the support engineer of Coq Platform at INRIA - currently @rtetley. @palmskog : if this is agreeable, please close this issue.

[MSoegtropIMC]

(Or close after it actually happened for the next release)

[palmskog]

@MSoegtropIMC signing the tag is one big step forward, but as per earlier discussion in this issue I don't think it solves verifiability by Platform users of the package collection, which something like conex would solve.

[MSoegtropIMC]

In this case I think the Coq team needs to state what kind of credibility authority or mechanism INRIA wants to use.

@Zimmi48 : can you please comment?

[palmskog]

Since @Zimmi48 is not an Inria employee, I think it's hard for him to comment on Inria issues in general. But arguably, there needs to be some kind of authority backing up all signing related to Coq and the Platform. Ideally, there is a trace of cryptographic signings going from the Platform maintainer to a Coq core team coordinator (and possibly further into Inria-based authority). I don't see how we can have formal trust otherwise. There are already examples of open source projects being "taken over" and used as attack vectors.

[MSoegtropIMC]

Looking at how difficult it is to get the installers signed, I have little hope that we get anywhere any time soon with deriving something from INRIA owned keys.