mathlib container setup script SSH fingerprints

Stream: general

[(deleted)]

mathlib's container setup script currently does an SSH to GitHub once to suppress the unknown key warning. Given that GitHub has an endpoint to download SSH fingerprints, shouldn't we download the actual fingerprints instead? https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/githubs-ssh-key-fingerprints

[Michael Gehlke]

Are you referring to:

# ssh to github once to bypass the unknown fingerprint warning
RUN ssh -o StrictHostKeyChecking=no github.com || true

in the Dockerfiles?

Eg,

• https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile#L39
• https://github.com/leanprover-community/mathlib4/blob/master/.docker/lean/Dockerfile#L35

If so, yes -- switching over to using the metadata API would ground the trust, rather than blindly checking whatever is at the DNS entry.

[(deleted)]

Once there's more support I plan to make a pull request

[Michael Gehlke]

I'm new so I'm not sure what the development standards are, but since it's used in at least two places and has security implications -- is this somewhere we should have a script like get_github_ssh_signatures.sh (or .py or .lean or...) that is used by both builds?