RE: Theoretical question about vulnerabilities

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

Nash wrote:

> >

On Wed, Apr 13, 2005 at 11:01:11AM -0400, der Mouse wrote:
> Take the code for the checker.  Wrap it in a small amount of code that
> makes a deliberate out-of-bounds access if the checker outputs `no
> problem'.  Then write another small bit of code which ignores its
> input and runs the wrapped checker on itself.
>
> Run the original checker on the result.
>
> This is basically the same diagonalization argument Turing used to
> demonstrate that the Halting Problem was unsolvable; that's the sense
> in which I call it the Halting Theorem rephrased.

First off, I think you're more or less correct. Sortof. There is no computable
predicate that will decide for any ARBITRARY PROGRAM whether ANY ARBITRARY
CONSTRAINT is satisfied. But, this is just the statement of the fact that there
are constraints that are, themselves, not computable.

But, this is highly naive. A useful checker would not be designed to try to meet
this objective. I think that's why he used the term "constrained environment."
<<

Exactly. I'm not interested in trying to write a program prover that will prove
that an arbitrary program is correct, if indeed it is. I am only interested in
proving that well-structured programs are correct. This does of course constrain
the software developer to write well-structured specifications and programs if
she wants them to be proven correct; but I see such a constraint as a positive
feature rather than a disadvantage, since it makes the resulting programs and
specifications easier to understand.

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