RE: Theoretical question about vulnerabilities

["David Crocker" <dcrocker () eschertech com>]

Crispin wrote:

> >
Proving that all array accesses are within bounds would seem to be
Turing undecidable. Either you are not proving what you way you are
proving, or your programs are not full Turing machines.

Proof: <insert diagonalization argument here :>

Issue: Some people may regard diagonalized programs are a contrivance,
and are only interested in correctness proofs for real programs (for
some value of "real").
<<

The diagonalization argument shows quite nicely they you cannot write a program
that, for any arbitrary input program, can say whether or not it has any array
bounds problem. Which is why we haven't wasted our time trying to write such a
program. Instead, we have produced a tool-supported method that lets us produce
programs (including programs that solve complex problems) that are proven -
subject to correctness of tool chain and processor - not to have array bounds
problems (or many other sorts of problem), for arbitrary inputs.

> >
Crispin's rebuttal: Suppose I want to prove that your program checker
does not have any illegal array references ...
<<

I don't see what you are getting at here. Our proof engine is large and complex;
but because of the way we have built it, the proofs that array indices are in
bounds are not particularly difficult. Of course, you would need to use a
different proof engine - or at least an independent proof checker - to produce
reasonable "proof" of the correctness of the prover itself. Despite this,
running the tool on itself does provide a lot of value, because proof failures
have shown up a number of problems with the tool. Some of these problems would
be very hard to detect by testing. The input space for a program of this type is
so large so that testing can only exercise a small fraction of that space
(actually, an infinitesimal fraction).

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com