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: Sun, 2 Feb 2020 12:44:18 -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-pl1-f172.google.com
  • Ironport-phdr: 9a23:0Mj0qhbl42cYSXij+/2SxPf/LSx+4OfEezUN459isYplN5qZr8i8bnLW6fgltlLVR4KTs6sC17OK9fy9EjVbvt7B6ClELMUXEUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/Jas90BTEr3tHd+hLy25lJ0+YkxLg6sut5pJu/Dlctvw7+8JcTan2erkzQKBFAjghL207/tDguwPZTQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctXSidPAJ6zb5EXAuUdMuhWr4byqUYAoxW9CwmjBv3hxDhTi3/qxK061vgtEQHa0AEiGd8FrXTarM/yNKcXSe270qjIzTDEb/NK2Tf86JXDfw47rvGWRrJwbdTeyU80FwjYiViQqIrlPy+S1uQTrWeb9eRgVeaoi28psAxxrT2vyd0tionNnI4a1lfE9SBgzYszONa2S1Z7bMa6HJdMsyyWLYh7T8M4T212pSo3xacKtYO5cSQU0Jgr2R/SZ+Cbf4WN/x7vSPqdITl9iX1+ZL6zmgi+/E28xeLiUsS7ylNHriRZndbQrH8A0hLe5daaRfZ45UitxTiC2gPW5+5aPU87iKXWJpg8ybAqjJUTq17MHirulUX2kqCWckIk9/Ct6+v9Y7XmooaQN5dwig3jK6gulNGzDOYmPgQUUGib/uO81LLn/ULnWrlFkvo2kqzBvJDbI8QUuLK5DhdL3oo/7xuzFTSr3dQCkXUZMV5IdwiLg5XrNl3QOPz4CO2wg1WokDdl3fDGObjhD43MLnjFjLfheqh95FBGyAo9ydBf4JxVB6oOIPL2QEDxtdjYAgUlPAyzxubrEM992Z8GWWKTHq+ZN7vfvkOP5uI2OuWDeIsVuCvmJPU+/P7vjXo5mUcHcqWz3JsXbmq4HvV8LEmDb3rsmIRJLWBftQ0nCefulVeqUDhJZn/0UbhvyCs8DdeaDILEWoC8yJeIxjynE5tNLjRHDEyLD3ryeYGDRN8DbSuTJolqlTlSBuvpcJMoyRz77Fyy8LFgNOeBonRF56Km78B84qjorT939TFwCJ7DgWSETmUxhmdRAjFvg/o5rkt6xVOOl6N/hq4ATI0B17ZySg4/cKXk4al/AtH2VBjGe47QGlmjS9SiRzo2S4BomoNcUwNGA9ynyyv78W+yGbZMzu6EAZU19uTX2H2jf8s=

Whatever memory corruption bugs remain in the ocaml ecosystem are just that -
bugs

But a design that’s intentionally just as dangerous (eg, filesystem
overwrites)? That’s a different conversation

Security isn’t a feature, it’s a set of concerns that are tightly coupled to
use case and threat exposure. “Threat modeling” is the primary process for
driving these discussions - but as a process, it requires first a sense of
what use cases Coq wants to support in the future.

If there is interest about setting up a good (read: productive, modern,
professional) process for discussing Coq’s security needs, I’d be happy to
facilitate pro bono. Any excuse to visit France :)

Sent from my iPhone

> On Feb 2, 2020, at 12:21 PM, Emilio Jesús Gallego Arias
> <e AT x80.org>
> wrote:
>
> Hi Théo,
>
> Théo Zimmermann
> <theo.zimmi AT gmail.com>
> writes:
>
>> Finally, Emilio, I don't understand what the issue would be with
>> providing a `-safe` mode that doesn't allow writing to files? Why do
>> you say a complete redesign and rewrite would be necessary? I seem to
>> have always heard people be optimistic on this matter (with projects
>> such as MetaCoq in particular). Your claim seems a bit at odds with
>> this.
>
> Maybe we don't agree on what I consider "adversarial"; indeed, to talk
> about "security" of Coq's type checking first we should establish what
> power does the adversary have.
>
> It is my impression that most security problems as of today are
> partially to blame on people doing too optimistic assumptions about the
> adversary.
>
> Can we for example guarantee that a .vo file is not going to be able to
> exploit a bug in the OCaml's GC / runtime as to have coqchk accept a
> file with a wrong proof?
>
> I'd advocate erring on the safe side here; my opinion is that Coq should
> not be used under general adversarial assumptions.
>
> E.
>



Archive powered by MHonArc 2.6.18.

Top of Page