The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Ron wrote:

> I am new to this list and interested in using a theorem prover to
> semi-automatically prove that a certain executable containing binary
> code(thus a dissassembly needs to be generated first) on e.g. Linux
> contains no possibility for e.g. a buffer-overflow.
Are you familiar with the large existing body of work on Foundational 
Proof-Carrying Code?  In this area, we prove theorems about machine code 
programs using no axioms but those of the machine architecture we run 
on.  The most well-studied and -implemented theorems here are memory 
safety theorems, which I think subsume buffer-overflow checking, given 
the right definitions.

I'm aware of these FPCC projects that already use Coq:

- Those in the FLINT group at Yale: 
http://flint.cs.yale.edu/flint/publications/
- My co-authors' and my work on building scalable FPCC systems using 
proof-generating or proved-sound program verifiers: see the 1st and 3rd 
entries on http://www.cs.berkeley.edu/~adamc/papers/

There is also work in the area using Twelf in place of Coq:

- The original FPCC project at Princeton: 
http://www.cs.princeton.edu/sip/projects/pcc/
- The ConCert project at CMU: see the 1st entry in each of the 1st two 
categories of http://www.cs.cmu.edu/~crary/papers/

> Coq seems to be a
> well developed theorem prover, however, I read in Chapter 1 of Coq'Art
> that Coq can't prove theorems about all computable functions(in
> particular those that not terminate). So, it seems I can't use Coq for
> my purposes, since I need to prove things over programs that are
> possibly interactive, and hence don't need to terminate. Could anyone
> provide some pointers, in case, it is possible to still use Coq?
>  
I think you have confused the "meta language," or language of Coq itself 
(which is a programming language in its own right); with potential 
"object languages," or programming languages that you prove theorems 
about.  There is no limitation against formalizing an object language 
that supports non-termination, and in fact all of the FPCC work I 
mentioned is in such a setting.

> More in general, it seems everyone ignores I/O (I have only seen the
> proof of the correctness of simple functions like max, sum, average,
> etc in some high-level language in the papers I skimmed). Is there
> some "trick" which makes I/O a non-issue? (I have seen dependent types
> approaches, but those seem to be still at the theoretical level).
>  
If you are only interested in buffer overflows, then you shouldn't need 
to model these exactly.  In any case, the first link I gave above 
probably has the most relevant work on proving general correctness 
properties of machine code.