Stream: Coq Platform devs & users

Topic: Certifying releases of the platform


view this post on Zulip Karl Palmskog (Aug 25 2020 at 19:47):

Another long-term issue for the platform: make all platform package maintainers cryptographically sign their releases that become part of a platform release. I documented here how one can check that a Coq tarball was actually signed by a Coq release manager, and similar practices should apply to the platform: https://github.com/coq/coq/wiki/VerifyingReleases

view this post on Zulip Karl Palmskog (Aug 25 2020 at 19:50):

unfortunately, a "Coq platform key signing party" to increase trust may be some time off in the future, and not only due to the time it takes to get the platform established...

view this post on Zulip Théo Zimmermann (Aug 26 2020 at 07:54):

Why does this page explain how to verify the signature of the commit instead of the signature of the tag itself?

view this post on Zulip Karl Palmskog (Aug 26 2020 at 07:57):

@Théo Zimmermann as far as I can tell, there is no dedicated git command for verifying a tag, git verify-commit is all there is (or maybe it was added recently)

view this post on Zulip Karl Palmskog (Aug 26 2020 at 08:17):

also, it seems the V8.11.0, V8.11.1 and V8.11.2 tags were never signed :shrug:

view this post on Zulip Théo Zimmermann (Aug 26 2020 at 09:48):

Sigh! This is despite the release documentation giving exactly the commands to use to prepare the tags.

view this post on Zulip Karl Palmskog (Aug 26 2020 at 10:14):

I guess I can update for 8.12 and add a note about instructions (for verifying release locally) not working for 8.11. It's not really feasible to describe both workflows at the same time (verifying a tag vs. verifying a commit)

view this post on Zulip Théo Zimmermann (Aug 26 2020 at 10:55):

We could also ask @Pierre-Marie Pédrot (not subscribed to this stream) to recreate the tags for 8.11.

view this post on Zulip Karl Palmskog (Aug 26 2020 at 11:23):

but wouldn't that change the tarballs/checksums and lead to a lot of work in opam, etc.?

view this post on Zulip Théo Zimmermann (Aug 26 2020 at 12:24):

I don't think so. The tarballs only depend on the content in there, not the tag meta-data AFAIK.

view this post on Zulip Michael Soegtrop (Aug 26 2020 at 14:10):

I think it would make sense to have a meta field in opam to specify how sure one can be about the authorship and check this. Btw.: interestingly opam does not fail when the given hashes are wrong. It spits an an error, but continues happily.

view this post on Zulip Karl Palmskog (Aug 26 2020 at 14:16):

@Théo Zimmermann so should I open a Coq issue about the missing tags? it may become a problem in the future if we integrate authorship verification in some pipeline

view this post on Zulip Théo Zimmermann (Aug 26 2020 at 14:17):

Sure!


Last updated: Jan 30 2023 at 10:03 UTC