Provably Correct Crypto?
At 4:15 PM 8/1/95, Ray Cromwell wrote:
That's a neat metaphor, but it doesn't always apply. It shouldn't apply to algorithms which are primitive recursive. Elementary algorithms like multiprecision add, sub, multiply, divide, modmult, and modexp (the basis of public key encryption) are all provably correct and all terminate. (the basis is polynomial operators over a ring) It is possible to verify the implementation (assuming the correctness of the compiler). Now there could be a "factoring" trapdoor in RSA, but that's a trapdoor not in the implementation of 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 key bits or session key bits are leaked. I would suspect this could be difficult, but approximations could be determined to within a high degree of confidence.
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. 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. --Tim May .......................................................................... Timothy C. May | Crypto Anarchy: encryption, digital money, tcmay@sensemedia.net | anonymous networks, digital pseudonyms, zero 408-728-0152 | knowledge, reputations, information markets, Corralitos, CA | black markets, collapse of governments. Higher Power: 2^756839 | Public Key: PGP and MailSafe available. "National borders are just speed bumps on the information superhighway."
[Tim responds to my note on "provably correct implementation"}
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.)
What I meant by my message is in some circumstances, an implementation can be proven correct (i.e. to do what it says it does correctly) What I mean by implementation is the source at the highest level, not the module dependencies which are abstractly disconnected from the application. (e.g. if a multiprecision math library that comes with the operating system is used by PGP, the source to PGP could be said to be "trapdoor free" even if the math library has an NSA monitoring function built into it) Each layer of course relies on the correctness of the layer beneath it, much like a theorem proof relies on the proof of the statements that makes it up. Thus, RSA-in-4-lines can be observed to be a correct implementation of RSA without any trapdoors (like secretly storing or leaking private key bits) at the level of its source code. Of course, the Perl interpreter itself would have to be proven correct, but we assume that no RSA trap doors have been put into perl because perl was available long before PGP and RSA-in-4-lines perl and is widely distributed. The probability of a trapdoor in perl is small. The hierarchy looks like this: RSA-in-4-lines :: DEPENDS_ON_CORRECTNESS_OF { Perl, DC, RSA_Algorithms } Perl :: DEPENDS_ON_CORRECTNESS_OF { C, Unix, Perl_Algorithms } DC :: DEPENDS_ON_CORRECTNESS_OF { C, Unix, DC_Algorithms } C :: DEPENDS_ON_CORRECTNESS_OF { C_compiler } C_compiler :: DEPENDS_ON_CORRECTNESS_OF { Assembler } Assembler :: DEPENDS_ON_CORRECTNESS_OF { instruction_set } instruction_set :: DEPENDS_ON_CORRECTNESS_OF { hardware } Now even if it were possible to prove the correctness of all those layers (which I find doubtful. Some kind of Goedel/Turing limitation is going to turn up somewhere), what if the 'hardware' isn't correct. (e.g. Pentium bug) There could be a one-in-a-zillion bug that randomly leaks keybits. IMHO, there's no sense in worrying about stuff like this. If your data is so valuable that you need absolute theoretical security, use a one-time-pad with a simple redundant provably secure device (also shielded from TEMPEST attacks), and have the thing implanted in your skull. ;-) -Ray
Hello Ray Cromwell <rjc@clark.net>, patl@lcs.mit.edu and tcmay@sensemedia.net (Timothy C. May) and cypherpunks@toad.com
At 4:15 PM 8/1/95, Ray Cromwell wrote: ...
PGP, but in the algorithm itself. RSA-in-4-lines-perl is probably ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ provably correct. To guard against trapdoors in PGP, you should ^^^^^^^^^^^^^^^^^ ... [emphasis tcmay]
To which tcmay responded:
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. ...
AFAIK (my 4 lines might differ from yours), there is no PRNG in the 4 lines of perl. The key is supplied as a parameter, and no guidance to its generation is given in the implementation. You are right about the dc, but it only uses that for modular exponentiation, which is a lot easier to prove correct than PRNG. Which is not to say that it *has* been proven. I guess that makes me a nit-picker... Jiri -- If you want an answer, please mail to <jirib@cs.monash.edu.au>. On sweeney, I may delete without reading! PGP 463A14D5 (but it's at home so it'll take a day or two)
...
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
Hmm. Instead of "vetting" the PGP PRNG code, as Dr. Cohen has been trying to tell me in private email is several programmer- years worth of work perhaps I should just write my own version of the PRNG using the algorithm as defined in whitepapernumberwhatever. If there are artificial "bugs" to throw off the PRNG currently in the PGP MIT code, they ought to simply not work right with the code I write independently and therefore cause a crash or something. Or perhaps just rewrite the program to use plain arrays instead of pointers. ;-) Phil
The shadowy figure took form and announced "I am Dr. Frederick B. Cohen and I s ay ... [ lots of purely subjective arguments that frequent alt.security.pgp ] 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. You should find this argument hauntingly familiar. 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'm sorry, the english prose your team writes holds no extra formal credibility over trust. It demonstrates more study - but has not proven security. 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. p.s X = thttpd -- <URL:http://www.comp.vuw.ac.nz/~matt> |~ |~ |~ o| o| ('< o| ,',) ''<< ---""---
...
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
On Tue, 1 Aug 1995, Dr. Frederick B. Cohen was alleged to have blathered:
Tim May mused:
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.
After all your griping over PGP, you spout this? Have you ever heard of Godel's theorem? I have a phrase for people who peddle their mark of approval that a given large program will work: "Snake oil salesman". 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. I repeat: Snake Oil Salesman <PLONK>
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
participants (8)
-
fc＠all.net -
futplex＠pseudonym.com -
Jiri Baum -
Matthew James Sheppard -
Nathan Zook -
Phil Fraering -
Ray Cromwell -
tcmay＠sensemedia.net