The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Real world isn't binary. Whether or not a container is the *only* line of defense very much changes the expense and complexity.

Just because everything runs in a VM or container does *not* mean everything is secured to a level where random Internet people could be given shell accounts and no harm could come of it. I don't think there's any debate about that in InfoSec. Happy to talk specifics/debate if it's hard to see why that's the case.

But even at a high level, I think most working engineers would agree: it's unreasonable to suggest that the following two services should have the exact same security posture:

* A website that typechecks a pure, total, functional language

* A shell server that gives away accounts to anyone who asks

If compiling .v can interact with the environment in unconstrained ways, then basically the advice I'm getting is "give everyone a shell on your server, just make sure your server is locked down." I think that's nuts.

Also: "put it in a container" doesn't address the other use case I mentioned above: namely, telling people that they can use Coq to certify the safety/correctness of untrusted code.

-t

On Sat, Feb 1, 2020 at 5:50 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Sat, 1 Feb 2020 15:35:53 -0800
Timothy Carstens <intoverflow AT gmail.com> wrote:

> ...
> 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.

Containers & VMs are a line of defense one should always have, whether
it is first line or last line doesn't change the expense and complexity.

Sure I'd prefer the Coq environment to have a small attack surface and
well defined requirements.  But I'm still going to use a container
regardless. So the expense and complexity of the container is always
felt.

Are you suggesting instead that you'd prefer the Coq environment be
made so that containers are unnecessary?