Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Safe to download and compile .v from evil source ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?


Chronological Thread 
  • From: Timothy Carstens <intoverflow AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
  • Date: Sat, 1 Feb 2020 18:19:32 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=intoverflow AT gmail.com; spf=Pass smtp.mailfrom=intoverflow AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f50.google.com
  • Ironport-phdr: 9a23:NvEMmBxn3FKtnqXXCy+O+j09IxM/srCxBDY+r6Qd1O8TIJqq85mqBkHD//Il1AaPAdyHra4fwLaN++C4ACpcuM3H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMjoZvJKk9xxTHr3BVf+ha2X5kKUickhrh6Mq85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyNOAo2+YIUPAeQPPvtWoZfhqFYVtxSyGROhCfnzxjNUhHL727Ax3eQ7EQHB2QwtB8wAsHXRrNXyKKcSUeC0x7TWwDrZdfNWwiv955bOchA6vPqBWrNwcczNyUkoCQPKkE+QqYLhPzOS2OUAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4Ebykjc+Cln3Io4Ice0RU17bNK+DZddtiOXO5F2T88+RWxjpTw0xaccuZGheSgH0JQnyADba/yAa4WI5wjsVOeVITthgHJldq+ziw+88UWg1uHwTMa00FFNripKltnDqGoB2ADU6siCUvd9/0Gh1iiT1w3L9O1IPUQ5mbDYJpMh2LI8i5sevEbZEiL2hEn6lKqWeV8l+uis5eTneLLmppqEOo91jAH+LqMumtKhDuQiPAgOW2+b+Oqn2b3s+E32WrRKjvksnqbFt5DaINwXprSlDA9NzoYj9xG/Ai+639QfhHkLNU5KeBaaj4fyIFzOO/D5DfKng1u2ijtrxvbGPqfgAprXNHTDnq3hLv5B7BtXzxN2xtRC7bpVDKsAKbT9QBzfrtvdWyM4Nguow/evI9xnzZ8TX3nHVq6fLKTMvEWG4uUwC+aJbY4R/j36Lq52tLbVkXYllApFLuGS1pwNZSXgR6g0EwCieXPpx+w5PyISpANnFb7ljVSDVXhYYHPgB/thtAF+M5qvCML4fq7ogLGF233mTJhfZ2QDDl7VVHm1L8OLXPADbC/UKchkwGRdBOqRDrQ53BTrjzfUjr9uL+7a4Cod7Mux29185umVnhY3p2V5

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?



Archive powered by MHonArc 2.6.18.

Top of Page