[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: [email protected] (Nathan Zook)*Subject*: Re: Provably Correct Crypto?*From*: [email protected] (Dr. Frederick B. Cohen)*Date*: Wed, 2 Aug 1995 04:30:42 -0400 (EDT)*Cc*: [email protected]*In-Reply-To*: <[email protected]> from "Nathan Zook" at Aug 2, 95 00:44:15 am*Sender*: [email protected]

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

**References**:**Re: Provably Correct Crypto?***From:*Nathan Zook <[email protected]>

- Prev by Date:
**Re: Pat Robertson Fears E-cash?** - Next by Date:
**Re: Provably Correct Crypto?** - Prev by thread:
**Re: Provably Correct Crypto?** - Next by thread:
**Re: Provably Correct Crypto?** - Index(es):