Stream: Coq devs & plugin devs

Topic: Security of bench


view this post on Zulip Ali Caglayan (Mar 21 2022 at 13:40):

Since I am adding the @coqbot bench command which will allow any user to bench, is security a concern? I don't know how much damage you can do in a bench script on the machines for instance? cc @Gaëtan Gilbert @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (Mar 21 2022 at 13:41):

probably. Can't you check that the use who requested the bench is a member of some reasonable dev set? e.g. any maintainer team

view this post on Zulip Maxime Dénès (Mar 21 2022 at 13:45):

Those are physical machines, so yes, giving access to anybody would be a big pb.

view this post on Zulip Maxime Dénès (Mar 21 2022 at 13:45):

(if the setup is still the same as it used to be)

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:11):

We can definitely restrict users in coqbot

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:11):

However I feel like this is definitely not coqbots job to do

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:11):

It has happened in the past that a check in coqbot has been implemented incorrectly

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:12):

Currently coqbot is the user that will start the bench in the coqbot PR

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:13):

I don't think it is possible for a users account to be used by coqbot to submit the bench request

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:14):

Can we not run the bench scripts as a user with restricted permissions on the machines? That way we won't have sudo powers and whatnot.

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:15):

Too risky, as they'd still share the same user on the machine. So a malicious user can plant something for the next one.

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:17):

Altough, I haven't looked at the setup in a long time

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:17):

What to do then? Do you agree that restricting from coqbots side seems like hiding the problem?

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:18):

Not sure it is hiding. If we trust coqbot from the point of view of this infrastructure, then we need to restrict access to coqbot, right?

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:20):

Here is a scenario that I am thinking about:

  1. Somebody submits an innocent looking PR to coqbot which allows anybody to start the bench (it literally only requires sending a request to gitlab)
  2. Somebody then submits a PR to coq/coq and runs a malicious bench script
  3. Bench machines have been broken as a result

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:22):

It seems to me that coqbot should not have permission to start the bench, otherwise we need to do security checks in coqbot

view this post on Zulip Théo Zimmermann (Mar 21 2022 at 14:23):

There is no getting away that we need to do security checks in coqbot anyway...

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:23):

Isn't there a review process for coqbot PRs?

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:23):

Ok, so coqbot should not start the bench then :)

view this post on Zulip Théo Zimmermann (Mar 21 2022 at 14:23):

Yes, there's a review process for coqbot PRs.

view this post on Zulip Théo Zimmermann (Mar 21 2022 at 14:24):

And yes, there's a risk of vulnerabilities in the code of the bot leading to security issues with the Coq project infrastructure.

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:25):

Isn't that also true for merges?

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:25):

Merges can be undone, damage to benches cannot

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:25):

Well, for undoing you need to notice something is off

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:26):

My point is we should not be too scared. Having to sneak in a coqbot PR takes more effort than if we just open the infrastructure to arbitrary code execution.

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:27):

As an attacker, I'd probably have more incentive sneaking in a malicious change in Coq than breaking the bench infrastructure

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:27):

This leaves the question of my innocent looking PR letting coqbot start the bench

view this post on Zulip Gaëtan Gilbert (Mar 21 2022 at 14:27):

are you saying random PRs get deployed without review and before merging?

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:28):

No they are not deployed without review

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:28):

However I did not think about the security risks of my PR until today

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:28):

And we can basically run whatever we like on bench as a result

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:29):

It is not currently deployed

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:29):

It was the right time to ask, then :)

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:30):

Btw, another thing we could consider is to put some virtualization layer in this infra

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:30):

I can submit a PR to coq/coq that will brick the bench, if my PR was deployed coqbot would have run it

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:30):

But that's some work

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:31):

Virtualization for a bench might be counterproductive however.

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:31):

Isn't performance something we want here?

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:31):

Virtualization has very low performance penalty these days

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:31):

What is more tricky for the bench is stability of execution time

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:32):

That would need to be measured

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:32):

That's what we couldn't get on regular CI infra

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:33):

So is it not possible to set a linux user to only be able to create files and run existing programs?

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:35):

Or maybe I am scaring myself too much. Perhaps the best solution is for coqbot to check who sent the request

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:35):

The user is already non-privileged

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:35):

I think it is safer for coqbot to just check the user is in a list, like PMP said

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:36):

Fair enough I will try to do that then

view this post on Zulip Théo Zimmermann (Mar 21 2022 at 14:37):

Regarding which list to use, my suggestion was to use the "@coq/contributors" team. It is a pretty large team, but we are liberal in how we add people to the GitLab organization anyway, so it matches OK with this process. Is that OK with everyone?

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:40):

Sounds reasonable to me. If we have logs with the user who triggered a call to the bench, even better.

view this post on Zulip Ali Caglayan (Mar 21 2022 at 14:42):

Technically we have logs. "Are they easily accessible" is another question.

view this post on Zulip Maxime Dénès (Mar 21 2022 at 14:52):

Ok, but at least in case of a pb, we can go and see what happened

view this post on Zulip Paolo Giarrusso (Mar 22 2022 at 06:48):

As long as coqbot jobs lack permission to tamper with the logs.


Last updated: Dec 06 2023 at 14:01 UTC