Karl Palmskog (Sep 08 2021 at 13:15): Karl Palmskog (Sep 08 2021 at 13:15):sorry for the slightly off-topic comment, but are platform releases (commits in coq/platform repo) signed?
Michael Soegtrop (Sep 08 2021 at 13:16):The installers are signed (typically ...)
Michael Soegtrop (Sep 08 2021 at 13:16):(With INRIA keys).
Karl Palmskog (Sep 08 2021 at 13:17):but wouldn't it make sense to sign the commits by the Platform manager like what RMs do with Coq?
Michael Soegtrop (Sep 08 2021 at 13:17):The commits in coq/platform are typically not signed - I could change that although as mentioned before Coq Platform is mostly opam.
Michael Soegtrop (Sep 08 2021 at 13:17):It has little meaning without say checking hashes of opam packages or the like.
Karl Palmskog (Sep 08 2021 at 13:18):OK, so there's no traceability to archives right now.
Michael Soegtrop (Sep 08 2021 at 13:19):Not sure what you mean by that ... do you mean a verified connection to specific git repos or others sources?
Karl Palmskog (Sep 08 2021 at 13:21):I mean, one might want to check that the archives I used to build the platform locally are the ones blessed by the Platform release manager. So there would be message/commit/something with all the archive SHAs that the RM has signed, and I can check this if I know the RM's public key.
Enrico Tassi (Sep 08 2021 at 13:22):I guess he means if you did git tag -S or just git tag
Michael Soegtrop (Sep 08 2021 at 13:23):Yes, but wouldn't this require support by opam? As I said, the Coq Platform code inherits its meaning to 99% from opam repositories.
Enrico Tassi (Sep 08 2021 at 13:23):The former makes a "heavy" tag where you sign the sha of that commit. If you create the commit via github, the tag is "light"
Enrico Tassi (Sep 08 2021 at 13:24):I agree with that
Michael Soegtrop (Sep 08 2021 at 13:24):I usually create the tag via Github as part of making a release. As I said, I can change this, but I don't see how one could get a tight solid chain to source code from that.
Karl Palmskog (Sep 08 2021 at 13:25):I think this is similar to doing an overlay of arXiv. Yes, everything comes from arXiv, but people are interested in whether a Turing awardee gave his blessing to this collection of papers or not
Michael Soegtrop (Sep 08 2021 at 13:26):Hmm, yeah, maybe. I didn't see the advantage, but if you say there is one, I can change it.
Karl Palmskog (Sep 08 2021 at 13:27):well, no requirement from me, I'm just paranoid about software collections being manipulated, and would be interesting if I could trace that I have the actual packages in a certain platform release.
Michael Soegtrop (Sep 08 2021 at 13:28):Hmm yes, but I guess it would only have meaning if I would tie it to a specific hash of the opam repos - which I don't want for flexibility.
Karl Palmskog (Sep 08 2021 at 13:29):but one could list the SHAs for actual tarballs for packages explicitly included in a release, no?
Karl Palmskog (Sep 08 2021 at 13:30):actually, it would be enough to list the commit SHAs for the GitHub repos for the package projects, since the tarballs can be recreated from those
Karl Palmskog (Sep 08 2021 at 13:33):this is also related I guess: https://reproducible-builds.org/
Michael Soegtrop (Sep 08 2021 at 13:34):I could also check the checksums in opam's download folders ...
Michael Soegtrop (Sep 08 2021 at 13:36):But again, I think this should first place be discussed with the opam team - how can I be sure that opam install xy.z installs version z of xy. If opam has this, we can discuss how Coq Platform can build on top of this.
One can also build something around it - like asking opam for all sources and all opam packages and comparing hashes, but it would be a bit of a hack.
Karl Palmskog (Sep 09 2021 at 11:26):this appears to be the state of the art of heavyweight opam repo signing (I was imagining much more lightweight stuff): https://github.com/hannesm/conex
Some documentation on the ideas behind the approach, in reverse chronological order:
We could summon the author to comment (he is on the Zulip).
Michael Soegtrop (Sep 09 2021 at 12:22):@Karl Palmskog : thanks for sharing - interesting! It doesn't seem feasible for 2021.09, but I could imagine to have this in the next release. Yes please invite the author for a discussion here.
Karl Palmskog (Sep 09 2021 at 12:29):@Hannes Mehnert we would like to increase trustworthiness of the Coq platform of packages, which is essentially an overlay of the main opam repository and the Coq opam repository. Could you comment on the feasibility of starting to use Conex to sign releases of the platform?
Karl Palmskog (Sep 09 2021 at 12:34):I think the "closure" of the platform is currently something like 30-40 packages? So scale is hopefully not an issue.
Théo Zimmermann (Sep 09 2021 at 12:54):Michael Soegtrop said:
Karl Palmskog : thanks for sharing - interesting! It doesn't seem feasible for 2021.09, but I could imagine to have this in the next release. Yes please invite the author for a discussion here.
I would prioritize adding more packages to the platform first though. Some people (like Iris) have been waiting for a long time now.
Michael Soegtrop (Sep 09 2021 at 12:57):@Théo Zimmermann : this is planned for 2021.09 :-)
Théo Zimmermann (Sep 09 2021 at 12:57):Great to hear!
Karl Palmskog (Sep 09 2021 at 12:58):No time requirements from my side. I can write up a GitHub issue about signing once we know a bit more.
Hannes Mehnert (Sep 13 2021 at 21:36):(conex designer and author here) conex is at the moment not ready (I have some experimental deployment) -- but I'll work on improving it (and would be happy if the coq community would like to use it) later this year! :) Furthermore, if people are interested in contributing, please say so. for 2021.09 I'd recommend to use good old PGP :)
also, if you open an issue on GitHub, feel free to mention me so I can track that. I've quite some projects on my plate at the moment.
Hannes Mehnert (Sep 14 2021 at 09:54):To be a bit more wordy. The design of conex is adapting the update framework https://theupdateframework.io/ to OPAM:
Current TUF installations have some issues, and usually have a single key that is able to delegate to someone. Lack of self-revocation and teams that adminstrate themselves (shrink / grow) has been discussed with Justin Cappos and specified in https://github.com/theupdateframework/taps/blob/master/tap8.md (I fail to remember whether conex implements that version or not).
For actual deployment, and public key infrastructure maintenance, it'd be good to integrate sigstore (sigstore.dev) via https://github.com/theupdateframework/taps/pull/141 -- or to specify and develop clearly the workflows of new developers / rolling over their keys / etc.
Funding-wise the OCaml software foundation is interested in funding work on conex this year, person-wise it is on my plate atm (and as explained, I have some other projects on my plate as well). I'm sure I'll achieve some work on conex in 2021 -- though the first step would be an online service (snapshot/timestamp) that holds a private key and signs an opam repository at timestamp X (so that clients can verify to have a recent repository).
Karl Palmskog (Sep 14 2021 at 09:59):thanks for the overview, I will try to summarize this in an issue on GitHub where I tag interested parties. It sounds like we will wait for there being a first successful deployment before we experiment with conex for the Coq platform
Karl Palmskog (Sep 15 2021 at 08:52):to close the circle, here is the issue link: https://github.com/coq/platform/issues/132
Last updated: Jun 03 2023 at 03:01 UTC