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




Archive powered by MHonArc 2.6.18.

Top of Page