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