coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Emilio Jesús Gallego Arias <e AT x80.org>
- To: Théo Zimmermann <theo.zimmi AT gmail.com>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
- Date: Sun, 02 Feb 2020 21:20:35 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
- Ironport-phdr: 9a23:g8zNyh+wnVWFqv9uRHKM819IXTAuvvDOBiVQ1KB42u4cTK2v8tzYMVDF4r011RmVBNmdt68P0rGN++C4ACpcuM3H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMjoZvKqk9xgbHr3ZGZu9awX9kKU+Jkxvz+8u98oRv/zhMt/4k6sVNTbj0c6MkQLJCET8oKXo15MrltRnCSQuA+H4RWXgInxRLHgbI8gj0Uo/+vSXmuOV93jKaPdDtQrAvRTui9aZrRwT2hyoBKjU07XvYis10jKJcvRKhuxlyyJPabY2JKPZzeL7WcMgETmRdQMleSy1BApu9b4QRCeoBIf1YpJT5q1cXsBeyGRWgCObpxzRVhHH5wLc63vwhHw/YwQIgGNwOvnrWo9v2OqgdXvy6wqbTwDXfdvNbwyvx5JTSfx0jp/yHQLJ+cdDWyUkqDw7LgVCQqY3hPzOU0eQCq2yV4PR7Vfq1kG4oswB/rSKrxscolIbJiYUVxUjY+CVjwYY6P8a4Q1N8bNG6C5ZRuCKXO5dsTsMlWWFotz83x7sbspC4ZCgH0Ikryh3cZvCdbYSE/BPuWPyMLTp6mX5pYq+zihis/US4yeDxV9O43VdIoyZfltTArHAA2wLV58OaUPVy5F2h1iyK1w3L6uFLP0Q0la3DJp8uwbM8ioAfsUPZHi/5gEn2jamWeVs4+uWw9ujqYbbrqoWCO4NqiwzyKLkil86iDegiLwQDUXaX9fy51LL5/E35RLtKjucxkqncqJ3VO98Wp6G6DgNJyIoj7Ay/Dzi+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmZk9ws5TqDxo8PhaxyuDhQIFh1o4ZH3COB6qYGKzXuF6MoOkoJr/fSpUSvWPQLvkh5vnZr3IiC0QqUqCt2ZYYb0eRBPVvOA3NbFL80o9HFn0F6FltBNf2gUGPBGYAL025WLgxs3RiUNr/UNXzA7u1ibnE5x+VW51bYmcXWEDcSTHvbYrWAq5QOhLXGddol3k/bZbkU5UohEO+5Fe8zKBofLKNq38o8Kn73d0w3NX90BQ79Dh6FcOYgjOdHzkymXkHFWY7
- Organization: X80 Heavy Industries
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.
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, (continued)
- 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 ?, Adam Chlipala, 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 ?, Timothy Carstens, 02/03/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Emilio Jesús Gallego Arias, 02/03/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 ?, Adam Chlipala, 02/02/2020
Archive powered by MHonArc 2.6.18.