The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Thank you for the link, it's an excellent talk! And extra-thank you for time-stamping it to the part about security :)

It sounds like my Q has been answered; thank you for all the replies. I'll need to mull over next steps.

Everything that follows is just IMHO:

I don't think gcc should be the model to emulate, and it would be nice if Coq could be used to certify code from untrusted sources.

If none of the maintained projects are using these exotic capabilities, they should to be removed given the impact it has on Coq's use cases. The sandboxing response is inviting trouble: perhaps Matt G is smart enough to get it right, perhaps a few other people are, but I assure you most engineers are not. Sandboxing should be used as a last-ditch "defense in depth," not as a front-line defense. It's hard to maintain for tons of reasons. For example, you need to re-evaluate your config every time you do a system update, since there's no computerized mechanism in place that guarantees that the update won't effect /etc or initd or any of a number of sandbox-relevant things.

For this reason, containers & VMs are awesome for sharing working environments, but are expensive and error-prone as a security boundary. Best practice yes, but only as a last line of defense.

But I also know that everyone's super busy and what I'm asking for is probably a hassle at this time - no worries and keep up the good work :)

On Sat, Feb 1, 2020 at 3:18 PM Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

On 2020-02-01 17:53, Tej Chajed wrote:
> For some idea of some of the issues, see this thread on a similar
> question for compiling C:
> https://security.stackexchange.com/questions/138881/is-it-dangerous-to-compile-arbitrary-c.
> In particular see Matt G's answer, since he runs a site that compiles
> arbitrary C. Essentially he runs the whole thing in a VM that doesn't
> have secrets, and then has extra mitigations to give nicer error
> messages when people try to exploit the compiler.

Matt has a talk in which he mentions the security of Compiler Explorer where he goes into a bit more details; see here: https://youtu.be/bSkpMdDe4g4?t=3193

Clément.