Re: Provably Correct Crypto?

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

...
> Frederick can you please tell me why I should belive thttpd is secure.
> I don't accept the ability to compile it myself as evidence and I
> don't accept a summary of that source written in english prose on the
> basis that it has no hard link what so ever to the source.  It was
> also written by the authors of thttpd.

The reason to believe that thttpd fulfills the claims it makes is
provided in some detail in the white paper on our server (see what's new
under http://all.net).  A slightly more detailed version has been
submitted for a journal article, and hopefully will appear in a year or
two.

Certainly compiling it yourself would not in any way help you assert its
security, however it would help you assure that the compiled version (which
we don't provide on-line) is not an altered executable.

I would detail the full set of claims here, but this is not the proper
forum for general security issues.  Of course if there is popular
support, I would be glad to... Instead, I will briefly outline it here:

The basic reason that thttpd can be verified to fulfill the claimed
security properties relate to some well thought-of and mathemtically
proven theories about information flow.  Specifically:

	we have shown that information coming from the client cannot
	flow to the server except in its effects of sending the requested
	file (if it exists, is properly owned, and is properly protected
	for access by remote users) and logging the request in the log
	file generated by the program.  If no information can flow from
	the client to the server data, the client cannot cause
	corruption of the server (subject to various details not
	included here).

	we have shown that the server is a limited function program (i.e.,
	does not have Turing capability), and that therefore no general
	purpose operations can be performed as a result of any external input.

	we have shown that the variables and structures are confined so
	as to have no unspecified side effects, and that therefore there
	are no effects other than those stated in the description of the
	program.

	we have also shown some other stuf you might be interested in.

The next logical question is why those are worthwhile things to show,
and I won't get into these details here without further prompting.

> You should find this argument hauntingly familiar.

I welcome your questions about "why" as I always do.  I think that
this is a very important question and one worth following up.

> You state that crypto should be poved correct and suggest a technique
> otherwise known as formal specification.  I agree, pgp should have
> been written in Z-specs.  If you take a course in formal specification
> you will soon see the intractability of the technique wrt large
> systems.

I didn't say that.  Perhaps you should review what I said before
characterizing it.

> I'm sorry, the english prose your team writes holds no extra formal
> credibility over trust.  It demonstrates more study - but has not
> proven security.

I have shown (not yet proven) certain things.  A graduate student is now
working on trying to prove the various properties I believe to be of
interest in an automatic theorum prover he is working on.  I believe
that these things are worth showing (and proving), but you may certainly
feel free to disagree with these contentions.

> If you want prople on this list to repeat after you "I cannot be
> certain there is no compromising bugs or backdoors in X" Then I will
> go out on a limb and say everyone here will agree if system X is
> sufficiently large.

I don't believe I ever asked anyone on this list to repeat anything. 
All I did was ask questions and respond to responses to my questions.

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