Re: Provably Correct Crypto?

[fc@all.net (Dr. Frederick B. Cohen)]

> > I think that this issue can generally be addressed by a divide and
> > conquer strategy.  Prove that the called routines are correct and
> > confined under all possible parameters, do the same for the calling
> > routines, do the same for the interaction between them, and I think you
> > have it.  This is pretty easy for one or two routines, but when you take
> > the OS into account, the C compiler into account, the program itself
> > into account, and the external environment into account, you run into
> > some serious limitations.  For example, you may (in some cases) have to
> > show that under all possible sequences of interrupt timings and stack
> > conditions, the system operates correctly (which almost none currently
> > do).  Unless you design with this sort of thing in mind, it's very hard
> > to demonstrate these properties even for limited subproblems. 
> > 
> 
> After all your griping over PGP, you spout this?  Have you ever heard of 
> Godel's theorem?

I think so.  From my understanding, it basically says that, in the
general system, you can write a legitimate expression that expresses its
own illegitimacy, or in other words that the general system is
incomplete "...in the sense that it fails to provide a proof for every
formula which is true under the interpretation..." (quoted from
"Introduction to Metamathematics" by S.C.  Kleene 1952,...,1980)

But I think you misinterpret this.  This does not mean that no program
can be proven to meet any properties.  It means that, among other
things, there are an infinite number of infinite expressions that cannot
be proven, but it does not mean that a finite expression (e.g., a
typical modern program) cannot be proven to meet all sorts of
properties.

In particular, for certain classes of programs, proofs about the flow of
information are not exceedingly complex to establish.  In general (as
was proven in the early 1980s), tracking information flow in a program
is NP-complete, however, in a program designed to limit information flow
this can be very straight forward (in fact I think it may be linear time
and space).  By proving that information doesn't flow from place to
place, we can essentially prove that information in one place does not
affect information in another place (by information thoeory), and
therefore greatly reduce the complexity of demonstrating various things
of particular interest to information security - to wit - that item A
doesn't corrupt item B, and that information in item A is not leaked to
item B.

>  I have a phrase for people who peddle their mark of 
> approval that a given large program will work: "Snake oil salesman".

In the case of the http daemon, it is a relatively small program of less
than 80 lines designed to be secure in various ways.  In the case of PGP
it is a relatively larger program that it not designed to be secure.

>  In 
> the messages which you have scrawled between this and the last on my 
> system when I caught up this evening, you have demonstrated the 
> fraudulent nature of your business by first claiming that certain 
> propositions were "demonstrated", then stating that a graduate student 
> was working on "proving" them.

How is it fraudulent to accurately state the facts?

> I repeat: Snake Oil Salesman

-- 
-> See: Info-Sec Heaven at URL http://all.net
Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236