The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 05/05/2011 11:07 AM, Andreas Bogk wrote:
> Excerpts from guninski's message of Mi Mai 04 13:50:13 +0200 2011:
> >    Proof.
> >      external "/bin/sh" "ESCAPE_SEQ; write_vo_proof; nicely_kill_coq ;" True.
> >      (* this invokes /bin/sh. suited for formal software verification *)
> >    Qed.
>
> FWIW, I think that this "external" feature, as well as the loading of 
> arbitrary
> plugins, are indeed a problem.

external is supposed to return either a proof term or a tactic to be 
applied on the goal. You can disrupt the execution flow as Georgi did 
and forge object files, but the checker (and an inspection of the object 
file) will detect that.

> Coq is more and more being used for software
> engineering for critical systems.

Yes, been there, done that...

> There's a huge benefit in being able to
> specify desired behaviour of subsystems formally, and have the author of the
> subsystem prove that his implementation fulfills the specification.  The 
> ability
> to break proof checking by the tricks demonstrated mean we're back at having 
> to
> read every single line of code of the subsystem, instead of being able to just
> read the specification and leave the details to the proof checking engine.

I think you are slightly rigorist here (please don't take that 
personally nor negatively). Having well-behaved subcomponents is clearly 
a good practice but (1) it may prevent you from using incomplete though 
effective proof techniques, and (2) it doesn't give the highest levels 
of confidence on its own.

Look at Chris Casinghino's and Brian Aydemir's proof of Fermat's theorem 
(Stéphane gave a link). You could formalise the syntax thoroughly and 
being convinced you understand every single detail of the syntax, and 
still fall in their trap. Whatever the syntax, you'll always find an 
illusionist to trick you.

The best defense against illusion is to have several viewpoints. That's 
what we intend to provide with the checker and the missing tool: a .vo 
file explorer.

> My suggestion would be:
>
>   * Remove the "external" feature, or make it optional, with "turned off" 
> being
>     the default
>   * Split load paths for .vo files and coq plugins, make plugin load path
>     default to system directories only, inhibit manipulation of plugin
>     load path from within .v files.

This is somehow a packaging policy that you may want to follow in a 
skeptical mode, but it seems dangerous to me to rely only on such 
techniques because it's hard to guarantee that there is no similar 
trapdoor in the toplevel.

--
Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14