Provably Correct Crypto?

[Dr. Frederick B. Cohen]

...
> >PGP, but in the algorithm itself. RSA-in-4-lines-perl is probably
>                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> >provably correct.  To guard against trapdoors in PGP, you should
>  ^^^^^^^^^^^^^^^^^
> >verify the correctness of the PRNG, Key Generator, and that no private
...
> This doesn't seem likely. I mean, doesn't "RSA-in-4-lines-of-Perl" *of
> necessity* make use of external library/utility functions? Such as the "dc"
> math routines for the PRNG? Part of its compactness is that it makes use of
> available libraries.

This issue is an interesting one and one worthy of being addressed. 
There are a couple of concerns here (I approximately quote from a
submitted paper on the secure W3 server with quotation marks):

Concern 1:
	"The secure (program) is designed in such a way that we can
	demonstrate (subject to the propriety of compilers, operating
	system functions, and other things in the environment) that once
	the daemon is started, only the desired affects result." 

Concern 2:
	The environment has an insecurity specific to the secure
	program used as a means of subverting the function of the
	secure program.

I pretty much believe that Concern 1 should be addressed by all programs
that claim to be secure.  That is, subject to the rest of the world woking
right, the secure program works right.

I believe that concern 2 should be addressed by all programs that claim
to be secure in a particular environment.  That is, beyond being secure
assuming the environment is secure, we might want to eliminate the
assumption about the environment by showing it to be justified.  In
terms of attacking systems, it is necessaary to subvert many different
environments for this issue to be important for widespread use of PGP,
or at least to subvert several of the more common environments (such as
what the Thompson c compiler mentioned in his Turing award talk did).

> Anything that "reaches out" to external libraries or utilities would then
> have the vulnerabilities of _those_ libraries and utilities, which may or
> may not be provably correct themselves. (And the issue of any PRNG being
> probably correct or not is of course an interesting, and deep, question.)
> 
> I do think the issues of modular design and provable correctness--or
> approximations to it--are interesting ones.

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. 

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