Re: "Perfect" or "Provable" security both crypto and non-crypto?

From: Bryan Olson (fakeaddress_at_nowhere.org)
Date: 09/14/04 

Date: Tue, 14 Sep 2004 07:56:21 GMT

Douglas A. Gwyn wrote:
> Paul Rubin wrote:
>
>> How do you know that?
>
> Well, of course I left out some details.
> The example was meant for a context in which
> the variable a was *declared* as an array.

Follow-ups can only respond to what you write, not necessarily
what you mean. Automated tools are also so limited. You
presented the code as a "template", and as such it is wrong. Not
that there isn't a point to correctness arguments, but this
strand does illustrate a major shortcoming of the method you
advocate: there are too many issues that you can simply miss and
thus get the proof wrong. Even in a trivial example of your own
choosing, Paul found a case that you missed.

There is a solution, that could well form the basis of future
efforts toward program correctness. Formal proofs should formal
to the extent that programs can verify their correctness. There
may be un-checkable assumptions, but the automated method should
at least explicitly state what they are. 

-- 
--Bryan