coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Sun, 02 Feb 2020 23:43:59 +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:DNUblxL1YJ8z3OQfO9mcpTZWNBhigK39O0sv0rFitYgRI/XxwZ3uMQTl6Ol3ixeRBMOHsq4C17ed6v66ESxYuNDd6StEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQZjId4Jas8yhTFrmZJduhI2GhkIU6fkwvm6sq/4ZJu/T5ct+49+8JFTK73Y7k2QbtEATo8Lms7/tfrtR7NTQuO4nsTTGAbmQdWDgbG8R/3QI7/vjP1ueRh1iaaO9b2Ta0vVjS586hrUh7ohzwZODM/7Wral9Z/jKNfoBKmuhx/34vZa5ybOfZiYq/Qe84RSHFfVchNSSNOHoK8b5MOD+UfO+ZYs5L9rEYKoRenGAWgGP/jxjpOi3Tr36M1zv4hHBnG0gI+AtwOt3rUotv3O6kRX++6w7XHwzrYYvNKwDfw8pTEfgw7rPyOW797bMrfyVMoFwPAllieponlPzKR1uQMtGiU9+5uWvy0i3Y9sAF+ujmhyd0oionNmI0VxVfE+j1lzYYvJN23UlV7asOjHZROrCybOIh7Tt84T2FvoiY6xaQLtJimdyYJ0JQq3wPTZv+EfoSS/B7vSuecLS1liH9nZb6znQu+/Ea+xuHkVMS50kxGojRZntTDrHwByRPe58mdRvdg8Uqs2DCC3B3J5O5eO0A7j6/bJoYhwrEukpoTtlzOHyD1lUnqlqOWcV8k+uew5+TmZLXpuIOcOpdphgz9MakigNKzDfo5PwQUQmSW+/mw2Kf+8UD3XrlGlvg2nbPYsJDeK8QbvKm5AwpN34k98Bu+ADSr3MgCkXkANlJFdwqLj5L1NFHWPPD4EfC/jkywnzds3vDKJ6HuApHQLnfYi7rhZrZ860tEyAUp19xf5pRUCqsAIP3pQEPxusbYXVcFNFmdz+/iQP590oIGUGaGSvuQPKrXuneD/esuJ6+JZZNTtTrgfasL/fnr2FI8mFscep6L0ICFc0eXF/BiLkqeVlP2g94aWTMHlhpuFKrtklLUAm0bXGq7Q69pvmJzM4mhF4qWA9n12OXcjhf+JYVfYyV9Mn7JEXrscNTWS6dULiWILZ04y2BWZf2aU4YkkCqWmkri0bM2fPqEomsfr52xjIEktd2Wrgk78HlPN+rY1miMS29umWZZFS9mhOZ4u0Mvk1o=
Organization: X80 Heavy Industries

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.

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 ?, Emilio Jesús Gallego Arias, 02/02/2020