Request: add my SSH public keys to the set of authorized keys on the INRIA server

[ahelwer]

For CI development we want to:

• Upload TLAPM builds to the INRIA server
• Deploy latest documentation to the INRIA server for the TLAPM tutorial website

For CI development iteration speed I need access to the INRIA server so I can see directory layouts and try out commands before putting them in a CI script. Could @lemmy @damiendoligez or @muenchnerkindl please add the following keys to the /home/github/.ssh/authorized_keys file on the INRIA server so I have access to the github user account on there?

[email protected] AAAAGnNrLXNzaC1lZDI1NTE5QG9wZW5zc2guY29tAAAAICQDDvPsnAIWneg4zy3v5Gtwj6Mm1XfYx4Fr/kZZ6B+AAAAABHNzaDo= [email protected]
[email protected] AAAAGnNrLXNzaC1lZDI1NTE5QG9wZW5zc2guY29tAAAAIKs9wb3HMZewa1DapZ8/nLRww5hJJC1v5CoW4THeuc7JAAAABHNzaDo= ahelwer@node-workstation-2022-11-15
[email protected] AAAAGnNrLXNzaC1lZDI1NTE5QG9wZW5zc2guY29tAAAAIA5Kc9kKTEyNnsDcNHi0ZkyNV9Wno3ywnt8z5nx1h9lwAAAABHNzaDo= ahelwer@node-2023-04-06-yubikey-c-bio

The private key counterparts reside in hardware U2F tokens so there is no risk of them being exposed (unless somebody robs my house).

Ref #125 (comment)

[lemmy]

I suggest creating a dedicated user account for ahelwer to keep the upload account separate in case there is a compromise of either account. I can add the github private key as a repository secret here.

[damiendoligez]

@ahelwer: do you mean adding these keys for a limited time while you debug the CI scripts ? Otherwise I agree it's better to create a separate account for you.

[lemmy]

I can add the github private key as a repository secret here.

INRIA_SSH_PRIVKEY

[ahelwer]

@ahelwer: do you mean adding these keys for a limited time while you debug the CI scripts ? Otherwise I agree it's better to create a separate account for you.

Yes this would only be necessary while I write/debug the CI scripts.

I guess I'm not entirely sure whether my own user account would be sufficient because I want to (1) replicate the method of distribution for the tla2tools.jar but with TLAPM and (2) update the TLAPM Inria docs automatically (https://tla.msr-inria.inria.fr/tlaps/content/Home.html) so whether my own account would be sufficient to learn/modify the current setup is dependent on what the current setup even is, which I do not know. Perhaps a user account where I at least have read access to all other users' home directories would be sufficient. Then I can clone the setup to some test server I setup on Azure or something.

[lemmy]

kuppe@tla:~$ ls -lah /home/github/
total 56K
drwxr-xr-x 9 github github 4.0K Apr  2  2020 .
drwxr-xr-x 9 root   root   4.0K Apr  1  2020 ..
-rw------- 1 github github  416 Apr  2  2020 .bash_history
-rw-r--r-- 1 github github  220 Apr  1  2020 .bash_logout
-rw-r--r-- 1 github github 3.5K Apr  1  2020 .bashrc
drwxr-xr-x 2 github github 4.0K Apr  1  2020 bin
drwx------ 3 github github 4.0K Apr  1  2020 .cache
drwx------ 4 github github 4.0K Jun 22  2022 .config
drwx------ 3 github github 4.0K Apr  1  2020 .gnupg
drwx------ 3 github github 4.0K Apr  1  2020 .local
-rw-r--r-- 1 github github  807 Apr  1  2020 .profile
drwx------ 2 github github 4.0K Apr  1  2020 .ssh
drwxr-xr-x 6 github github 4.0K Sep 17  2020 upload
-rw------- 1 github github  786 Apr  1  2020 .viminfo
kuppe@tla:~$ ls -lah /home/github/upload/
total 24K
drwxr-xr-x  6 github github 4.0K Sep 17  2020 .
drwxr-xr-x  9 github github 4.0K Apr  2  2020 ..
drwxr-xr-x  3 github github 4.0K Apr 28 00:54 dist
drwxr-xr-x 14 github github 4.0K Apr 28 00:40 doc
drwxr-xr-x  2 github github 4.0K Apr 28 01:30 products
drwxr-xr-x  5 github github 4.0K Apr 28 00:54 repository

upload is served by Apache at https://nightly.tlapl.us.

[ahelwer]

Can you create a user account then please? This is entirely about making iteration time as small as possible.

[lemmy]

You should be able to log in the machine.

By the way, the TLAPS documentation could also be uploaded to Github pages, hosted at tlapm.tlapl.us.

[ahelwer]

@lemmy that might be an easier route to go for the docs actually. IIRC all you'd need to do is activate github pages in the repo settings, set it to serve from doc/web/index.html on the main branch, then set up the A record on the subdomain and all the usual stuff to get letsencrypt SSL working.

[lemmy]

Apparently, there is already https://proofs.tlapl.us/

[lemmy]

@ahelwer I will deactivate your account to minimize the attack surface if you no longer need SSH access to the Inria machine.

[ahelwer]

Still needed for uploading binaries. Could you switch it to serve from main?

[lemmy]

Are binaries also uploaded to Github? Why don't you use the github account for that?

[lemmy]

Could you switch it to serve from main?

Switched

[ahelwer]

Are binaries also uploaded to Github? Why don't you use the github account for that?

I will, but would still like access until that feature is complete.