Stream: Coq devs & plugin devs

Topic: Verifying signatures of Coq release tarballs

Karl Palmskog (Jun 15 2020 at 08:10):

does an RM sign source tarballs? If not, why not?

Karl Palmskog (Jun 15 2020 at 10:12):

I think it makes sense (in adversarial settings) that one should be able to verify that the tarball checksum of a Coq release is endorsed by the RM, e.g., it could be that someone who is not the RM edits the GitHub release posthoc, submits updated package with updated checksum to OPAM, which we then all install. With proper signing, and under normal crypto assumptions, this could only happen if the RM GPG key was compromised.

Moreover, this is also an argument for better advertisement/visibility of RMs and their respective public keys.

Enrico Tassi (Jun 15 2020 at 11:43):

We do sign merge commits and tags as devs. I was expecting the tarballs to be just a git archive of a signed tag? Isn't it the case? Before git we were putting tarballs on a website and signing a asc file IIRC, but with git I don't see the point of it (the tarball is a reproducible artifact of a signed tag)

Karl Palmskog (Jun 15 2020 at 11:45):

for 8.11.2, the commit signature is different from the fingerprint given by Pierre-Marie above: 7922C01FD9BA3C7B

Karl Palmskog (Jun 15 2020 at 11:47):

where are we supposed to look to connect GitHub accounts with keyserver identities?

Karl Palmskog (Jun 15 2020 at 11:49):

to be honest, reproducing tarballs from a Git commit is a chore, has anyone verified that this works reliably? That is, bit-level equality can be obtained with the "official" tarball.

Enrico Tassi (Jun 15 2020 at 11:49):

Screenshot-from-2020-06-15-13-47-36.png

Karl Palmskog (Jun 15 2020 at 11:49):

yes, I am saying that the signature is different from what is given above here

Enrico Tassi (Jun 15 2020 at 11:50):

let me check...

Enrico Tassi (Jun 15 2020 at 11:52):

$ git verify-commit 1539a9a0d894ea9e24e3d0e163006d6477646ec6
gpg: Signature made jeu. 14 mai 2020 22:29:39 CEST
gpg:                using RSA key BA47A91F9104E72184D70F6D7922C01FD9BA3C7B

Karl Palmskog (Jun 15 2020 at 11:56):

so how do I reproduce the tarball from that locally?

Enrico Tassi (Jun 15 2020 at 11:56):

(but it is not in my keyring, I'll try to download later)

Enrico Tassi (Jun 15 2020 at 11:59):

Google says git archive --format=tar.gz -o /tmp/my-repo.tar.gz --prefix=my-repo/ master, I don't know if they use the exact same command. I've to go now

Enrico Tassi (Jun 15 2020 at 12:07):

gares@ollypat:~/COQ/master$ wget https://github.com/coq/coq/archive/V8.11.2.tar.gz
...
gares@ollypat:~/COQ/master$ sha256sum V8.11.2.tar.gz
98cb9e12ba2508a1ca59e0c638fce27bf95c37082b6f7ce355779b80b25e1bfd  V8.11.2.tar.gz
gares@ollypat:~/COQ/master$ git archive --format=tar.gz --prefix=coq-8.11.2/ -o /tmp/x.tar.gz V8.11.2
gares@ollypat:~/COQ/master$ sha256sum /tmp/x.tar.gz
98cb9e12ba2508a1ca59e0c638fce27bf95c37082b6f7ce355779b80b25e1bfd  /tmp/x.tar.gz

Enrico Tassi (Jun 15 2020 at 12:08):

everything looks in order to me, but I don't have a "proof" that the key belongs to PMP, I've never keysigned with him.

Enrico Tassi (Jun 15 2020 at 12:09):

Enrico Tassi said:

$ git verify-commit 1539a9a0d894ea9e24e3d0e163006d6477646ec6
gpg: Signature made jeu. 14 mai 2020 22:29:39 CEST
gpg:                using RSA key BA47A91F9104E72184D70F6D7922C01FD9BA3C7B

@Pierre-Marie Pédrot do you have a time machine ;-)

Enrico Tassi (Jun 15 2020 at 12:10):

It says 14 May ;-)

Karl Palmskog (Jun 15 2020 at 12:11):

I see, the main disconnection I see is then between BA47A91F9104E72184D70F6D7922C01FD9BA3C7B and 7922C01FD9BA3C7B. I guess there is some git command stuff for that?

Enrico Tassi (Jun 15 2020 at 12:12):

Key "ids" are the long thing, you got the last bytes there (this is usually the "short id" of a key)

Enrico Tassi (Jun 15 2020 at 12:13):

It works like git sha1, but IIRC you take the tail rather than the head ;-)

Karl Palmskog (Jun 15 2020 at 12:14):

OK thanks, if you don't mind I will post this to the Coq wiki (if something similar is not already there)

Enrico Tassi (Jun 15 2020 at 12:15):

The only missing bit, on my PC, is that I've never keysigned with @Pierre-Marie Pédrot so he never told me in person that that fingerprint is indeed his. He did in this chat, but he was not even trolling a bit, so I can't be 100% sure he was himself ;-)

Enrico Tassi (Jun 15 2020 at 12:15):

You are welcome to do that.

Karl Palmskog (Jun 15 2020 at 12:16):

you seem to have cross-signed with him? https://pgp.cs.uu.nl/stats/7922c01fd9ba3c7b.html

Enrico Tassi (Jun 15 2020 at 12:17):

oops, then my local db is not up to date, let me fetch

Enrico Tassi (Jun 15 2020 at 12:18):

Oh yes. Then the tarball is definitely his work!
```gares@ollypat:~/COQ/document-manager$ gpg --receive-keys BA47A91F9104E72184D70F6D7922C01FD9BA3C7B
gpg: key 7922C01FD9BA3C7B: 4 signatures not checked due to missing keys
gpg: key 7922C01FD9BA3C7B: public key "Pierre-Marie Pédrot (pierre-marie.pedrot@irif.fr) <pierre-marie.pedrot@irif.fr>" imported
gpg: marginals needed: 3 completes needed: 1 trust model: classic
gpg: depth: 0 valid: 5 signed: 31 trust: 0-, 0q, 0n, 0m, 0f, 5u
gpg: depth: 1 valid: 31 signed: 26 trust: 29-, 0q, 0n, 0m, 2f, 0u
gpg: depth: 2 valid: 7 signed: 14 trust: 6-, 0q, 0n, 0m, 1f, 0u
gpg: next trustdb check due at 2020-08-04
gpg: Total number processed: 1
gpg: imported: 1
gares@ollypat:~/COQ/document-manager$ git verify-commit 1539a9a0d894ea9e24e3d0e163006d6477646ec6
gpg: Signature made jeu. 14 mai 2020 22:29:39 CEST
gpg: using RSA key BA47A91F9104E72184D70F6D7922C01FD9BA3C7B
gpg: Good signature from "Pierre-Marie Pédrot (pierre-marie.pedrot@irif.fr) <pierre-marie.pedrot@irif.fr>" [unknown]
gpg: aka "Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>" [full]

Karl Palmskog (Jun 15 2020 at 12:18):

of course, nobody has verified that PMP is the RM of 8.11. Arguably this would/should be done by Matthieu? Also, if there are two RMs, shouldn't they both sign the tag/commit? (Yes, pushing this way too far, but for sake of argument)

Théo Zimmermann (Jun 15 2020 at 12:45):

Karl Palmskog said:

of course, nobody has verified that PMP is the RM of 8.11. Arguably this would/should be done by Matthieu? Also, if there are two RMs, shouldn't they both sign the tag/commit? (Yes, pushing this way too far, but for sake of argument)

Aren't you going a bit far? The RM is written down in the changelog in the manual (which is in the sources (where all PRs are integrated through signed merge commits)).

Karl Palmskog (Jun 15 2020 at 12:46):

ah, but do those changelogs specify the signatures/keys of the RMs?

Théo Zimmermann (Jun 15 2020 at 12:47):

Ah no, they don't.

Théo Zimmermann (Jun 15 2020 at 12:47):

Since we are signing merge commits, I think we should organize key signing parties next time we meet physically.

Enrico Tassi (Jun 15 2020 at 12:50):

I don't see the problem is with the scenario "trusted dev X makes a release without being (officially) appointed RM".

Karl Palmskog (Jun 15 2020 at 12:50):

extremely paranoid people like myself would consider it suspicious

Karl Palmskog (Jun 15 2020 at 12:51):

https://github.com/coq/coq/wiki/VerifyingReleases

Enrico Tassi (Jun 15 2020 at 12:52):

Thanks for the write up, +1 for key signing parties.

Karl Palmskog (Jun 15 2020 at 12:53):

btw, isn't this kind of stuff something that would be required for Common Criteria certification and similar?

Karl Palmskog (Jun 15 2020 at 12:59):

OK, so the process for PM certification would be something like the following:

• We trust RM #0. This person signs the "initial" release commit, which contains release notes with the name+signature of RM #1.
• RM #1 signs the next release commit, which contains release notes with the name+signature of RM #2

Karl Palmskog (Jun 15 2020 at 13:06):

this would all break down if RM #n got ill or similar, which is why it makes sense to have two RMs per release.

Pierre-Marie Pédrot (Jun 15 2020 at 13:13):

extremely paranoid people like myself would consider it suspicious

You should consider all my kernel patches to be extremely suspicious then...

Karl Palmskog (Jun 15 2020 at 13:16):

there is no protection here against RMs going rogue (or failing to prevent other contributors from going rogue), but at least one can trace a chain of successors, so it will go down in flames like Aurelius passing the Roman Empire to Commodus, rather than by barbarian invasion

Pierre-Marie Pédrot (Jun 15 2020 at 13:19):

first time I see summoning Roman history to explain trust in software development...

Karl Palmskog (Jun 15 2020 at 13:47):

ah, glad I had the opportunity before it becomes a Watson'ing offense...

Cyril Cohen (Jun 15 2020 at 14:49):

Karl Palmskog said:

so how do I reproduce the tarball from that locally?

In mathcomp I reproduce the tarballs locally in etc/utils/packager, I reverse engineered the following:

ARCHIVE=$(mktemp)
PREFIX=$(echo math-comp-$TAG | sed "s/\+/-/")
git archive --format=tgz --output=$ARCHIVE \
    --prefix=$PREFIX/ $TAG # reproduce github archive
SUM=$(sha256sum $ARCHIVE | cut -d " " -f 1)

(given ARCHIVEURL="https://github.com/math-comp/math-comp/archive/$TAG.tar.gz" )

Karl Palmskog (Jun 15 2020 at 14:53):

@Cyril Cohen so do you also have a "rolling RM" system for MathComp now?

Cyril Cohen (Jun 15 2020 at 14:54):

Karl Palmskog said:

Cyril Cohen so do you also have a "rolling RM" system for MathComp now?

We do.

Karl Palmskog (Jun 15 2020 at 14:57):

ah, then I will have to be (equally?) paranoid there as well. I hope a few MC devs get included in any future keysigning party.

Cyril Cohen (Jun 15 2020 at 14:58):

Karl Palmskog said:

ah, then I will have to be (equally?) paranoid there as well. I hope a few MC devs get included in any future keysigning party.

We do not sign the releases anyway :oops: but we should start asap

Enrico Tassi (Jun 15 2020 at 15:00):

We should sign the tags!

Enrico Tassi (Jun 15 2020 at 15:01):

Note that GH does a "soft signature" of tags you create from the web UI IIRC

Enrico Tassi (Jun 15 2020 at 15:02):

(I don't know what it does exactly, but you a get a non-gpg verified label somewhere. I belieev it means verifies w.r.t. GH authentication, which you may not trust, but is better than an anonymous push)

Karl Palmskog (Jun 15 2020 at 15:03):

Cyril Cohen said:

We do not sign the releases anyway :oops: but we should start asap

I hope you can also pinpoint future RMs (and ideally their keys) in your CHANGELOG.md

Enrico Tassi (Jun 15 2020 at 15:06):

My "problem" with this signature is that I'd like MC release process to be OK for non geeks to. Here https://github.com/math-comp/math-comp/wiki/Howto-Release#release I suggested to do the tag via GH (which does the soft signing) since GPG has a masochistic UI and I would not inflict it on anyone. I believe my motivation/opinion on this is not unanimous, but at least explain how things are in MC.

Théo Zimmermann (Jun 15 2020 at 15:08):

I care very much for accessibility of the contributing process too.

Théo Zimmermann (Jun 15 2020 at 15:08):

And our requirement of signing merge commits is a barrier of entry, which I hoped to lift by making it possible for members of the pushers team to merge by calling the bot to the rescue.

Enrico Tassi (Jun 15 2020 at 15:08):

Similarly I'm not happy switching MC to a script-based merge process as we do in Coq, or push the process towards the tons of rebases we do in Coq, but I never had to push too much for this.

Enrico Tassi (Jun 15 2020 at 15:10):

Asking a non-geek "hey, please rebase since there is a trivial conflict in the changes files" seems like shooting yourself in the foot to me.

Enrico Tassi (Jun 15 2020 at 15:10):

We do this a lot in Coq (but not for the changes...)

Enrico Tassi (Jun 15 2020 at 15:11):

I'm not saying it is wrong in the context of Coq, but I believe MC users and potential contributors are less acquainted to git or gpg gimmicks.

Karl Palmskog (Jun 15 2020 at 15:12):

simple rebase is one thing and is at least in the realm of being teachable, but I think the limit may be at: "please refactor your commits into 5 units with the following granularity and commit message format"

Enrico Tassi (Jun 15 2020 at 15:15):

Believe me when I say that even convincing some users to fire up gitk to actually see the status of thie branch is not obvious ;-) (with the objective of then explaining the command line gimmicks in terms of actions on the DAG). I would rule out rebase completely.

Enrico Tassi (Jun 15 2020 at 15:16):

The PR assignee can do it of course, but asking the contributors... it really depends if you know the contributor IMO.

Théo Zimmermann (Jun 15 2020 at 15:23):

Yep, when you don't know the contributor, it might be a good idea for the PR assignee to take care of trivial rebases, especially when this is the last thing blocking a merge.

Last updated: May 31 2023 at 16:01 UTC