The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Ok I think I understand now.

I think Jason's suggestion of coqchk is as close as Coq provides to
that, but maybe the following idea would be closer.  I once used an
antequated proof system (pvs) that had a tactic language but also had
the ability to "macro-expand" the tactics into atomic proof steps and
record the resulting fully expanded proofs in a file. Having that
eliminates the need to run the tactic language later to verify the
proof, and thus the possibility that someone can exploit the tactic
language.

Ideally, or as close to it as one could hope, one would have the
ability to "macro-expand" Coq proofs into something that contains no
Ltac or vernacular (and is probably very large as a result), and is
completely checkable by the Coq kernel alone, which has been closely
scrutinized to be clean of exploitable behavior.  It wouldn't even read
in other files - every such fully-expanded proof would be self
contained - so that the Coq kernel could run so as to say
Yeah or Nay without any other IO.

On Sat, 1 Feb 2020 20:30:36 -0800
Timothy Carstens 
<intoverflow AT gmail.com>
 wrote:

> Sorry for my part in any confusion <3
> 
> Consider the following workflow:
> 1. User goes to website and downloads .tgz
> 2. User extracts .tgz, finds a bunch of .v files
> 3. README.md says "The safety guarantee is expressed in foo.v"
> 4. Independent expert in computer science reads foo.v, reads
> basic_definitions.v, and says "yep: the safety guarantee means what
> you think it means. if it typechecks, then you're good to go."
> 5. User runs coqc foo.v
> 
> My question was: is this safe for the user to do, or is it possible
> that coqc foo.v might hack their computer?
> 
> The interesting question is whether Coq intentionally has features
> that can facilitate this: things like the ability to run shell
> commands, write to files at arbitrary paths, explore the file system
> in any way, open sockets, run arbitrary ocaml, etc.
> 
> [ Ignore memory safety for a moment; I'll assume no one knows if coqc
> is memory safe for the same reasons no one knows if any program is
> memory safe (no formal methods - yet!) ]
> 
> If so, then (5) is inherently an unsafe thing to do, and in that case
> I don't see how Coq could be used to certify untrusted code. You'd
> need to first do a code review of the ltac and everything else to
> convince yourself that it was safe to compile. IMHO this should
> change in the future, simply on the appeal of the use case described
> above. One of Coq's best application domains is the verification of
> real world computing artifacts, after all.
> 
> 
> Again, I don't want people to think I'm raising giant alarm bells
> here - Coq is undergoing a lot of changes right now as a platform,
> and I respect the autonomy of the Coq maintainers to decide what
> problems to tackle and in what order. In my opinion they have shown
> excellent judgement thus far and I do not seek to interfere in their
> plans.
> 
> 
> On Sat, Feb 1, 2020 at 7:48 PM 
> jonikelee AT gmail.com
> <jonikelee AT gmail.com>
>  wrote:
> 
> > There's some confusion here, perhaps all mine, about the distinction
> > between Coq as a system for verifying code (which it can do) vs. Coq
> > and the environment it runs in as a verified system (which it
> > isn't). It seems to me that these questions have been mixing those
> > two very different concepts.
> >
> > Coq, merely by virtue of it being a system for verifying code, does
> > not enhance trust of itself and the environment it is run in being
> > safe to use to check that some other code can be verified.  One
> > level of trust does not eliminate the need for trusting the other
> > level.
> >
> > If you run Coq in a way such that something malicious can substitute
> > 'echo "Qed!"' for your Coq prover without you knowing it is
> > doing so, then there is nothing Coq nor its developers can do to
> > save you.  Yet I am sure this must be obvious to all, so it must be
> > me that is still confused about your questions.
> >
> >
> >
> > On Sun, 2 Feb 2020 15:50:27 +1300
> > Marco Servetto 
> > <marco.servetto AT gmail.com>
> >  wrote:
> >  
> > > > Also: "put it in a container" doesn't address the other use
> > > > case I mentioned above: namely, telling people that they can
> > > > use Coq to certify the safety/correctness of untrusted code.  
> > >
> > > To make this more explicit:
> > > if there was an online service that gives you "proven correct and
> > > safe code1" and the corresponding coq proof code2; would running
> > > such proof be a valid certification that such code1 is
> > > correct and safe? or, is it possible that during the execution of
> > > code2 arbitrary behavior makes a "yes" result even if the proof in
> > > itself if bogus?
> > > Note how running coq in a container or not does not really change
> > > the issue here.  
> >
> >