RE: Theoretical question about vulnerabilities

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

Crispin wrote:

> > 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.
<<

The whole science of program proving is based on exactly this sort of flow
analysis. The analyser will postulate that Y is initialised at the assignment to
Z, given the deduced program state at that point. This is called a "verification
condition" or "proof obligation". It can then attempt to prove the hypothesis;
for this example, the proof is trivial. I guess it would have been more
difficult 20 years ago when Hermes was written.

The alternative solution to the problem of uninitialised variables is for the
language or static checker to enforce Java's "definite initialisation" rule or
something similar. This at least guarantees predictable behaviour.

An issue arises when a tool like Perfect Developer is generating Java code,
because even though PD can prove that Y is initialised before use in the above
example, the generated Java code would be violate the "definite initialisation"
rule. We have to generate dummy initialisations in such cases.

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