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 17:35:58 -0800
  • Authentication-results: mail2-smtp-roc.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-pj1-f52.google.com
  • Ironport-phdr: 9a23:KF43OhPBQmwfaCW+eQAl6mtUPXoX/o7sNwtQ0KIMzox0LfT8rarrMEGX3/hxlliBBdydt6sYzbaI+Pu8ESxYuNDd6StEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQZjId4Jas8yxTFr3VHdu9LwW9kOU+fkwzz68ut8pNv6Thct+4k+8VdTaj0YqM0QKBCAj87KW41/srrtRfCTQuL+HQRV3gdnwRLDQbY8hz0R4/9vSTmuOVz3imaJtD2QqsvWTu+9adrSQTnhzkBOjUk7WzYkM1wjKZcoBK8uxxyxpPfbY+JOPZieK7WYNUXTndDUMlMTSxMGp+zYYQPAeUOIOhWoYrzp1UMohWgAgehH//vyiZNhnPq3a02z+YsHAfb1wIgBdIOt3HUoc3rOqcTVOC1y7XIzTXDbvhLxzry8pLIcgs9of6SW7JwatfaxE4uFwPDklWQrpLlMC2P1uQDt2ib6ORhWPmgi24isQ5xozyvyt0whYnOg4IY01bJ/jh6zoYtPdC0VlJ3bNq+HJZTtyyWLZV6Tt4jTm1yuCs21KUKtJy1cSQQ1Zgr2xrSZ+aZf4WG4R/vTvudLDR+iXl4YrywnQyy/lKlyuDkVsm7zlJKri1dn9nJrH8N1hjT5tGfSvt/40utwDiP2gDN5u1eLkA0kq3bK5ElwrEujJYcrUPDHirulEX3iq+ZaFkk9/C25+j7ZrjqvJyROo9uhg3gL6gjm9azDOQmPgQWWmiU4+W81Lnt/U3jR7VKi+U7kqjfsJDGIsQbuLC2AxVb0oYn7Ba+ASyr0NsdnXYdLVJFfAiLgJTuO1HLOPz4F+uwg0ywkDd3wPDLJqHuApLULnTajLjheat95FVHxQoozdFf4opUBasbLPLyXE/xrt3YAQUjPwy62ea0QOl6g4gZQCeEBrKTGKLUq16BoOw1cMeWY4pAhDf4LOQl9rbFhGUihVIbZuH93J0Lb261BPpiJFqxbn/lg9NHGmAP6FltBNf2gUGPBGYAL025WLgxs2liVNCWSLzbT4Xou4SvmT+hF8QPNG9DA1GIV3zvctfcAqpeWGepOsZk1wc8e/2hRosmj0z8sQb7z/9/LLOR9HBC853k09dx6qvYkhRgrWUlXfTY6HmESiRPpk1NQjY32K5lpkkkkwWM1KF5h7pTEtkBvv4=

Getting to a place where .vo is platform/version agnostic, and where we have
a decent library for checking/navigating .vo, would be FANTASTIC imho

Lots of benefits: checking untrusted code yes, but also integration into
other software that might want to support loading of certified plugins (just
for example)

Also would provide a clean way to combat bitrot by providing some forward
compatibility to Coq-based projects

I presume I’m just rediscovering some of the thinking that’s already been put
into this - thank you for your patience with me!

-t

Sent from my iPhone

> On Feb 2, 2020, at 2:44 PM, Emilio Jesús Gallego Arias
> <e AT x80.org>
> wrote:
>
> Adam Chlipala
> <adamc AT csail.mit.edu>
> writes:
>
>> I think this issue is actually relatively easy/cheap to sidestep.
>
>> Here's my solution, for an age when the world has converged enough on
>> a small set of proof assistants that are blessed for security-critical
>> verification.
>>
>> [...]
>
> Indeed, that sounds like a plan; of course work such as CoqInCoq
> etc... are also very welcome steps.
>
> What I was trying to answer is more "is the current Coq implementation
> adversarial-resistant"
>
> I think it not and it was not designed to be, getting a secure
> proof-checker will require new (and exciting) research and engineering work.
>
> There is a danger IMHO in sending the opposite message.
>
> Kind regards,
> E.



Archive powered by MHonArc 2.6.18.

Top of Page