Re: Theoretical question about vulnerabilities

[Crispin Cowan <crispin () immunix com>]

David Crocker wrote:


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.


The Hermes programming language took this approach
http://www.research.ibm.com/people/d/dfb/hermes.html

Hermes proved a safety property called Type State Checking in the course
of compiling programs. Type State offers very nice safety properties for
correctness, including proving that no variable will be used before it
is initialized. But the Hermes Type State Checker was not formally
complete; there were valid programs that the checker could not *prove*
were correct, and so it would reject them. Here's an example of a case
it cannot prove:

if X then
   Y <- initial value
endif
...
if X then
   Z <- Y + 1
endif

The above code is "correct" in that Y's value is taken only when it has
been initialized. But to prove the code correct, an analyzer would have
to be "flow sensitive", which is hard to do.

Here's where it gets interesting. The authors of Type State went and
analyzed a big pile of existing code that was in production but that the
Type State checker failed to prove correct. In (nearly?) every case,
they found a *latent bug* associated with the code that failed to pass
the Checker. We can infer from that result that code that depends on
flow sensitivity for its correctness is hard for humans to reason about,
and therefore likely to be wrong.

Disclaimer: I worked on Hermes as an intern at the IBM Watson lab waay
back in 1991 and 1992. Hermes is my favorite type safe programming
language, but given the dearth of implementations, applications, and
programmers, that is of little practical interest :)

Crispin

--
Crispin Cowan, Ph.D.  http://immunix.com/~crispin/
CTO, Immunix          http://immunix.com