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
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
Those are physical machines, so yes, giving access to anybody would be a big pb.
(if the setup is still the same as it used to be)
We can definitely restrict users in coqbot
However I feel like this is definitely not coqbots job to do
It has happened in the past that a check in coqbot has been implemented incorrectly
Currently coqbot is the user that will start the bench in the coqbot PR
I don't think it is possible for a users account to be used by coqbot to submit the bench request
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.
Too risky, as they'd still share the same user on the machine. So a malicious user can plant something for the next one.
Altough, I haven't looked at the setup in a long time
What to do then? Do you agree that restricting from coqbots side seems like hiding the problem?
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?
Here is a scenario that I am thinking about:
It seems to me that coqbot should not have permission to start the bench, otherwise we need to do security checks in coqbot
There is no getting away that we need to do security checks in coqbot anyway...
Isn't there a review process for coqbot PRs?
Ok, so coqbot should not start the bench then :)
Yes, there's a review process for coqbot PRs.
And yes, there's a risk of vulnerabilities in the code of the bot leading to security issues with the Coq project infrastructure.
Isn't that also true for merges?
Merges can be undone, damage to benches cannot
Well, for undoing you need to notice something is off
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.
As an attacker, I'd probably have more incentive sneaking in a malicious change in Coq than breaking the bench infrastructure
This leaves the question of my innocent looking PR letting coqbot start the bench
are you saying random PRs get deployed without review and before merging?
No they are not deployed without review
However I did not think about the security risks of my PR until today
And we can basically run whatever we like on bench as a result
It is not currently deployed
It was the right time to ask, then :)
Btw, another thing we could consider is to put some virtualization layer in this infra
I can submit a PR to coq/coq that will brick the bench, if my PR was deployed coqbot would have run it
But that's some work
Virtualization for a bench might be counterproductive however.
Isn't performance something we want here?
Virtualization has very low performance penalty these days
What is more tricky for the bench is stability of execution time
That would need to be measured
That's what we couldn't get on regular CI infra
So is it not possible to set a linux user to only be able to create files and run existing programs?
Or maybe I am scaring myself too much. Perhaps the best solution is for coqbot to check who sent the request
The user is already non-privileged
I think it is safer for coqbot to just check the user is in a list, like PMP said
Fair enough I will try to do that then
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?
Sounds reasonable to me. If we have logs with the user who triggered a call to the bench, even better.
Technically we have logs. "Are they easily accessible" is another question.
Ok, but at least in case of a pb, we can go and see what happened
As long as coqbot jobs lack permission to tamper with the logs.
Last updated: Dec 06 2023 at 14:01 UTC