No crypto/privacy relevance, delete or flame now.... ... Now, Rice's Theorem says that all non-trivial properties of TMs are undecidable. If I pick a "non-trivial" property, I can't conceivably build a TM ("write a program", if you like) that, upon input of the specification of an arbitrary TM, can tell whether or not that TM exhibits the property I picked. This does not mean that I can't decide whether some particular TMs have that property or not -- I can. I just can't write down a procedure that handles the general case.
Also, this theorem clearly hinges on the meaning of "trivial". From what I've seen, a very strict interpretation is largely appropriate; nearly everything except the least exciting of trivial low-level properties of TMs seems to come out to be "non-trivial" in this regard. The proof of the theorem is more precise about this, naturally, but I've found this useful as a working colloquial definition.
Issue 1: Undecidable for arbitrary programs does not mean undecidable for every program. For all finite programs with finite input sequences, all properties are decidable. Complexity may make proofs for large programs infeasible at this time, but that is all. Now back to the point of the discussion. For certain classes of programs, we can prove many things that are relevant to information protection. Furthermore, as we attempt these proofs, we may find and fix the program anomolies (i.e., bugs) that would cause the program to fail in an undesirable way. Therefore, the proof techniques give us two benefits - they help us fix the programs, and they help increase the assurance that the programs do precisely what they are supposed to do and nothing else. Issue 2: The notion that mathematics somehow excludes linguistic proofs (forwarded I believe by a user with "may" in their email address) is nonsense. Mathematics at its core is based on linguistic notions that are defined in plain language. These notions develop a system of rules which may be applied to decide the veracity of a proposition. The rules themselves form a language with syntax and semantics just as the language that defines them has syntax and semantics. The notion of separating language from mathematics is a fine and interesting one, but it certainly does not apply to any mathematics currently in widespread use. A proof done without mathematical symbols is no less a proof. Issue 3: Let's get back to the point of this discussion. What can we really prove about algorithms? I have made the assertion that an intersting property for the purposes of assessing integrity, availability, and confidentiality for servers like the W3 server and the gopher server is the limitation of information flow. I have backed up my assertion with a demonstration in the form of programs that do this and English demonstrations that that is of real value. Does anyone disagree? Why? Is there a reason this same analytical technique cannot be used on PGP or other cryptosystems to demonstrate that there are no back doors (other than perhaps in the underlying inadequacy of the overall technique)? How hard is it to do this for such programs? What programming structures make this difficult? Will it reveal many programming errors and therefor be a useful general purpose tool for writing better programs? Just thought I would stir things up a bit. -- -> See: Info-Sec Heaven at URL http://all.net Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236