coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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, 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?
- [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jay Kruer, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Andres Erbsen, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Tej Chajed, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Clément Pit-Claudel, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Marco Servetto, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jason Gross, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jason Gross, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Adam Chlipala, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Théo Zimmermann, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Emilio Jesús Gallego Arias, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Andres Erbsen, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jay Kruer, 02/01/2020
Archive powered by MHonArc 2.6.18.