If someone hacked GitHub they'd just get the _public_ keys, same as the ones listed in the link. You can't login on a server with the public key.

What he has done is that by adding github ids, he gets the public keys of all the users and adds them to his servers. Now all the users' public keys are already in the system. Now they can login with their private keys and this private key remains _only_ on their own system. Not on GitHub or server.

If someone hacked github, they could substitute their own evil key for one of the developers' keys and the automation would add that key to appropriate places, giving access to whomever has the evil private key.

On the other hand, OP probably trusts the contents of source repositories stored on github (few people use commit and tag signing); if so he already trusts github with everything.

It really depends upon if the git repo is gpg signed. We really don't know enough about the automation to make any assumptions.

Were I to do it I would require gpg signed commits and setup the trust chain a bit differently. But you're right its likely just a list of git repos that aren't signed.

Signing of the repo contents (commits/tags) doesn't help anyhow with user ssh keys. If the automation gets the keys from github it effectively trusts github completely, irrespective of the situation with repos.

Not necessarily. It could do key pinning for example, which at least protects already-established users.

Additionally, if you use gpg to build your ssh keys and have a trust/sign chain you could then pull this stuff with impunity as long as you keep the trust chain issues sorted.