Re: [SC-L] Theoretical question about vulnerabilities
David Crocker wrote: Exactly. I'm not interested in trying to write a program prover that will prove that an arbitrary program is correct, if indeed it is. I am only interested in proving that well-structured programs are correct. The Hermes programming language took this approach http://www.research.ibm.com/people/d/dfb/hermes.html Hermes proved a safety property called Type State Checking in the course of compiling programs. Type State offers very nice safety properties for correctness, including proving that no variable will be used before it is initialized. But the Hermes Type State Checker was not formally complete; there were valid programs that the checker could not *prove* were correct, and so it would reject them. Here's an example of a case it cannot prove: if X then Y <- initial value endif ... if X then Z <- Y + 1 endif The above code is "correct" in that Y's value is taken only when it has been initialized. But to prove the code correct, an analyzer would have to be "flow sensitive", which is hard to do. Here's where it gets interesting. The authors of Type State went and analyzed a big pile of existing code that was in production but that the Type State checker failed to prove correct. In (nearly?) every case, they found a *latent bug* associated with the code that failed to pass the Checker. We can infer from that result that code that depends on flow sensitivity for its correctness is hard for humans to reason about, and therefore likely to be wrong. Disclaimer: I worked on Hermes as an intern at the IBM Watson lab waay back in 1991 and 1992. Hermes is my favorite type safe programming language, but given the dearth of implementations, applications, and programmers, that is of little practical interest :) Crispin -- Crispin Cowan, Ph.D. http://immunix.com/~crispin/ CTO, Immunix http://immunix.com
Re: [SC-L] Theoretical question about vulnerabilities
der Mouse wrote: [B]uffer overflows can always be avoided, because if there is ANY input whatsoever that can produce a buffer overflow, the proofs will fail and the problem will be identified. Then either (a) there exist programs which never access out-of-bounds but which the checker incorrectly flags as doing so, or (b) there exist programs for which the checker never terminates (quite possibly both). (This is simply the Halting Theorem rephrased.) Precisely because statically proven array bounds checking is Turing Hard, that is not how such languages work. Rather, languages that guarantee array bounds insert dynamic checks on every array reference, and then use static checking to remove all of the dynamic checks that can be proven to be unnecessary. For instance, it is often the case that a tight inner loop has hard-coded static bounds, and so a static checker can prove that the dynamic checks can be removed from the inner loop, hoisting them to the outer loop and saving a large proportion of the execution cost of dynamic array checks. How much of this optimization can be done is arguable: * The Jones&Kelly GCC enhancement that does full array bounds checking makes (nearly?) no attempt at this optimization, and suffers slowdowns of 10X to 30X on real applications. * The Bounded Pointers GCC enhancement that does full array bounds checking but with a funky incompatible implementation that makes pointers bigger than a machine word, does some of these optimizations and suffers a slowdown of 3X to 5X. Some have argued that it can be improved from there, but "how much" remains to be seen. * Java compilers get the advantage of a language that was actually designed for type safety, in contrast with C that aggressively makes static type checking difficult. The last data I remember on Java is that turning array bounds checking on and off makes a 30% difference in performance. Crispin -- Crispin Cowan, Ph.D. http://immunix.com/~crispin/ CTO, Immunix http://immunix.com
RE: [SC-L] Theoretical question about vulnerabilities
der Mouse wrote: >> Basically, the same arguments usually made for any higher-level langauge versus a corresponding lower-level language: machine versus assembly, assembly versus C, C versus Lisp, etc. And I daresay that it provides at least vaguely the same advantages and disadvantages as for most of the higher/lower level comparisons, too. But it is hardly the panacea that "proving the program correct" makes it sound like. As someone (who? I forget) is said to have said, "Beware, I have only proven this program correct, not tested it". << There are actually 2 separate issues here: 1. There are tools (such as Perfect Developer) that allow you to write specifications and will then generate all or most of the code automatically. This is the "VHLL" situation you are talking about. This approach increases both reliability and productivity, because the software developer has less to write and the specification is much closer to the problem than the code needed to implement it. 2. Proving programs correct with respect to some specification (including implied specifications such as absence of buffer overflow). I defend the use of the term "proof" here, provided that the software developer can amass a reasonable body of evidence that the proof process is sound. Possible evidence includes: testing the software thoroughly and finding ZERO bugs; checking the proofs using independent proof checking software; manually checking a selection of the proofs; and using similar techniques to prove the proof-generating software correct, whilst taking care to avoid circular arguments. Of course, one could write a buggy prover, in the same way that one can write a buggy compiler; but just as the compilers from the best suppliers mature until they are considered trustworthy by their customers, so can proof tools gain in maturity and stature. Tools such as SPARK and Atelier B have already reached this level of trust, and I am confident that Perfect Developer will be equally trusted after a few more years commercial usage. BTW it is by no means unknown for a body of mathematicians to consider a theorem proven and then for a mistake in the proof to be found (e.g. the early "proofs" of the four-colour theorem); so I really don't think that proofs that are manually derived and manually checked are necessarily better than computer-generated proofs. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Theoretical question about vulnerabilities
Nash wrote: >> On Wed, Apr 13, 2005 at 11:01:11AM -0400, der Mouse wrote: > > Take the code for the checker. Wrap it in a small amount of code that > makes a deliberate out-of-bounds access if the checker outputs `no > problem'. Then write another small bit of code which ignores its > input and runs the wrapped checker on itself. > > Run the original checker on the result. > > This is basically the same diagonalization argument Turing used to > demonstrate that the Halting Problem was unsolvable; that's the sense > in which I call it the Halting Theorem rephrased. First off, I think you're more or less correct. Sortof. There is no computable predicate that will decide for any ARBITRARY PROGRAM whether ANY ARBITRARY CONSTRAINT is satisfied. But, this is just the statement of the fact that there are constraints that are, themselves, not computable. But, this is highly naive. A useful checker would not be designed to try to meet this objective. I think that's why he used the term "constrained environment." << Exactly. I'm not interested in trying to write a program prover that will prove that an arbitrary program is correct, if indeed it is. I am only interested in proving that well-structured programs are correct. This does of course constrain the software developer to write well-structured specifications and programs if she wants them to be proven correct; but I see such a constraint as a positive feature rather than a disadvantage, since it makes the resulting programs and specifications easier to understand. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
Re: [SC-L] Adding some unexpected reliability expectations
Date sent: Wed, 13 Apr 2005 08:18:06 -0400 From: ljknews <[EMAIL PROTECTED]> > http://www.cnn.com/2005/TECH/04/12/remote.control.mines.ap/index.html > > I think this causes reliability issues not anticipated by those who wrote > the operating system for the laptop computer. Amen. The Register on Matrix too: http://www.theregister.co.uk/2005/04/12/laptop_triggered_landmine/ (Any comments about "minefield" testing a new technology?) With the US being one of the few holdouts against the ban on landmines, there are predictable concerns about the danger the new mines hold for civilian populations. However, there would also seem to be any number of potential dangers to the troops using them. There are very few details provided in regard to the new mines. There appear to be different types. They have some kind of wireless capability. (The CNN article refers in one place to yards, and another to more than a mile. Of course, if it's designed for yards and someone has a good antenna ...) They have remote detonation capability. Based upon what is said, we can determine some additional aspects of the technology, as well as surmise more. They likely communicate via radio frequencies. They will have some kind of (likely minimal) software for reception of signal, authentication, and activation. (Deactivation is likely accomplished by activating the mine when [hopefully] nobody is around.) The mines are probably individually addressable: blowing an entire minefield for a single intrusion would not seem to be an effective use of resources. Radio communication would imply that either the mines are battery powered, or that they contain an antenna and transponder. Given the purpose and use of mines, it is likely that there is an alternate and more standard triggering mechanism such as pressure plates or tripwires that does not require wireless activation. There are, of course, other more advanced possibilities for such a technology. Mines could be remotely enabled and disabled, could communicate with each other, or could communicate sensor results with a central location. However, these functions are unlikely in a first generation device. The potential risks are numerous. With radio communications mines that are buried, or placed under or behind metal or water, may fail to detonate when needed, or deactivate. Any kind of software is, of course subject to failures (which, in this case, could be literally catastrophic). Authentication would be a fairly major issue: sniffing of radio traffic could easily determine commands, replay attacks, static passwords, or number sequences. (Note that the mines require "minimal training" for use.) Failure of authentication could, again, result in failure of either detonation or deactivation. Battery failure would be an issue and therefore transponders are more likely, but transponders would be more difficult to troubleshoot. (Should the transponders retransmit? That would assist with finding and disarming mines, but broadcasting a signal with known improper authentication would result in a means of determining the location of mines.) Overall, mines still seem to be a pretty bad idea. [Ed. Let's please allow this thread to die out, or get back to issues directly related to software security per se. KRvW] == (quote inserted randomly by Pegasus Mailer) [EMAIL PROTECTED] [EMAIL PROTECTED] [EMAIL PROTECTED] The Internet may promise to improve the way we educate and learn, but so did early television. TV technology has instead reduced our attention spans, reduced intellectual conversations to sound bits, and left us with the impression that in order to be informed, we must first be entertained. - Lew Platt, of HP http://victoria.tc.ca/techrevorhttp://sun.soci.niu.edu/~rslade
Re: [SC-L] Theoretical question about vulnerabilities
On Wed, Apr 13, 2005 at 11:01:11AM -0400, der Mouse wrote: > > Take the code for the checker. Wrap it in a small amount of code that > makes a deliberate out-of-bounds access if the checker outputs `no > problem'. Then write another small bit of code which ignores its input > and runs the wrapped checker on itself. > > Run the original checker on the result. > > This is basically the same diagonalization argument Turing used to > demonstrate that the Halting Problem was unsolvable; that's the sense > in which I call it the Halting Theorem rephrased. First off, I think you're more or less correct. Sortof. There is no computable predicate that will decide for any ARBITRARY PROGRAM whether ANY ARBITRARY CONSTRAINT is satisfied. But, this is just the statement of the fact that there are constraints that are, themselves, not computable. But, this is highly naive. A useful checker would not be designed to try to meet this objective. I think that's why he used the term "constrained environment." So, there are lots of cool ways to constraint the environment. You could constrain the language in order to make certain constraints easy to prove. You would still be unable to make proofs about all constraints, but the sub-theory you're working in for a particular constraint might be complete, which means that whether a program meets that constraint would be fully computable. This is just the assertion that if T is a deductively closed theory (in logic) and S is a sub-theory, that T's incompleteness doesn't imply S's incompleteness. At one level, this is just the statement that every formal theory contains Logic itself as a sub-theory and that logic is complete (Goedel's Completeness Theorem). Another more interesting example is the sub-theory of Number Theory that contains only zero, the successor function, and addition. Its a perfectly good sub-theory of Number Theory and its been proved complete. But, its embedded** within a much stronger Number Theory that's not complete. Also, one might seek to constrain the program's resource use during a given computation. E.g., build the run-time environment with a suitably strict watch-dog. Then, infinite loops may be made impossible and every constraint becomes fully computable. This is basically computation within the realm of strictly recursive functions, rather than the larger class of partial recursive functions. So, you may be in trouble if the program you need to write is a partial recursive function. There's some interesting semantics of programming language being built on top of Topological Fixed Point Theory. I read about it briefly, but can't really comment on how well it addresses this problem. It seems to be a promising possibility, though. See Nielson for more. ciao, -nash "Semantics with Applications", Nielson & Nielson, Wiley, 1992. Available as a PDF here: http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html ** By "embedded" I mean in the strict mathematical sense, but in this case the formal languages do not differ, so we can be a bit loose. It is not necessary that this happen, though. The Arithmetization technique used by Goedel gives us nice ways of embedding theories from other languages into a larger theory. Also, I think this is more or less what Cohen does with Forcing languages. In fact, all of mathematics is considered (by logicians) to be embedded inside what's called Set Theory (typically given by an axiom system called ZFC). Set Theory is very powerful and is hence, incomplete. But, there are lots of theories in mathematics that are complete. The Theory of the Real Field, the above Number Theory, and others. Here are some references: http://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory http://www.solace.net/nash/math/Set_Theory/zfc_axioms.pdf "The Handbook of Mathematical Logic", Jon Barwise, North Holland Publishing Co., 1977. ISBN 0 444 86388 5. (No longer in print, but you may find a copy at your local Univ. library) > > > I really do find this line of argument rather irritating; the > > theoretical limits of proof are quite a different thing from the > > practical application of proof-based technology in a suitably > > constrained environment. > > Entirely true. But if you use theoretical language like "proof", you > have to expect to be held to a theroetical standard of correctness. > > /~\ The ASCIIder Mouse > \ / Ribbon Campaign > X Against HTML [EMAIL PROTECTED] > / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B -- An ideal world is left as an exercise for the reader. - Paul Graham
Re: [SC-L] Theoretical question about vulnerabilities
>>> [B]uffer overflows can always be avoided, because if there is ANY >>> input whatsoever that can produce a buffer overflow, the proofs >>> will fail and the problem will be identified. >> Then either (a) there exist programs which never access >> out-of-bounds but which the checker incorrectly flags as doing so, >> or (b) there exist programs for which the checker never terminates >> (quite possibly both). (This is simply the Halting Theorem >> rephrased.) > Could you explain why you believe that proof of a specific property > in a constrained environment is equivalent to the Halting Problem? Take the code for the checker. Wrap it in a small amount of code that makes a deliberate out-of-bounds access if the checker outputs `no problem'. Then write another small bit of code which ignores its input and runs the wrapped checker on itself. Run the original checker on the result. This is basically the same diagonalization argument Turing used to demonstrate that the Halting Problem was unsolvable; that's the sense in which I call it the Halting Theorem rephrased. > I really do find this line of argument rather irritating; the > theoretical limits of proof are quite a different thing from the > practical application of proof-based technology in a suitably > constrained environment. Entirely true. But if you use theoretical language like "proof", you have to expect to be held to a theroetical standard of correctness. /~\ The ASCIIder Mouse \ / Ribbon Campaign X Against HTML [EMAIL PROTECTED] / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B
Re: [SC-L] Re: Application Insecurity --- Who is at Fault?
So you blame the grunts in the trenches if you lose the war? I mean, that thinking worked out so well with Vietnam and all... ;-) regards, -dsp I couldn't agree more! This is my whole point. Security isn't 'one thing', but it seems the original article [that started this discussion] implied that so that the blame could be spread out. If you actually look at the actual problems you can easily blame the programmers :)
[SC-L] Adding some unexpected reliability expectations
AP reports a military system using laptop computers to control land mines: http://www.cnn.com/2005/TECH/04/12/remote.control.mines.ap/index.html I think this causes reliability issues not anticipated by those who wrote the operating system for the laptop computer. -- Larry Kilgallen
Re: [SC-L] Re: Application Insecurity --- Who is at Fault?
On 4/13/05, der Mouse <[EMAIL PROTECTED]> wrote: > >>> I would question you if you suggested to me that you always assume > >>> to _NOT_ include 'security' and only _DO_ include security if > >>> someone asks. > >> "Security" is not a single thing that is included or omitted. > > Again, in my experience that is not true. Programs that are labelled > > 'Secure' vs something that isn't. > > *Labelling as* secure _is_ (or at least can be) something that is > boolean, included or not. The actual security behind it, if any, is > what I was talking about. > > > In this case, there is a single thing - Security - that has been > > included in one and not the other [in theory]. > > Rather, I would say, there is a cluster of things that have been boxed > up and labeled "security", and included or not. What that box includes > may not be the same between the two cases, even, never mind whether > there are any security aspects that aren't in the box, or non-security > aspects that are. > > > Also, anyone requesting software from a development company may say: > > "Oh, is it 'Secure'?" Again, the implication is that it is a single > > thing included or omitted. > > Yes, that is the implication. It is wrong. I couldn't agree more! This is my whole point. Security isn't 'one thing', but it seems the original article [that started this discussion] implied that so that the blame could be spread out. If you actually look at the actual problems you can easily blame the programmers :) -- Michael
RE: [SC-L] Theoretical question about vulnerabilities
> -Original Message- > From: [EMAIL PROTECTED] > [mailto:[EMAIL PROTECTED] > Behalf Of der Mouse > Sent: 12 April 2005 05:15 > To: SC-L@securecoding.org > Subject: Re: [SC-L] Theoretical question about vulnerabilities > > > > [B]uffer overflows can always be avoided, because if there is ANY > > input whatsoever that can produce a buffer overflow, the proofs will > > fail and the problem will be identified. > > Then either (a) there exist programs which never access out-of-bounds > but which the checker incorrectly flags as doing so, or (b) > there exist > programs for which the checker never terminates (quite possibly both). > (This is simply the Halting Theorem rephrased.) > Could you explain why you believe that proof of a specific property in a constrained environment is equivalent to the Halting Problem? When I explain and even demonstrate the benefits of formal reasoning I find that, increasingly often, someone pops up with Godel or Turing to "prove" that it is all a waste of time. Having done so they then, presumably, go back to using the less rigorous approaches which are a demonstrable cause of failure in the systems our industry builds. I really do find this line of argument rather irritating; the theoretical limits of proof are quite a different thing from the practical application of proof-based technology in a suitably constrained environment. For the record, I am quite confident that we can prove freedom from buffer overflow in a large and useful class of programs without hitting any of the limits you suggest. Indeed we, and our customers, are routinely doing so. Peter ** This email is confidential and intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient, be advised that you have received this email in error and that any use, disclosure, copying or distribution or any action taken or omitted to be taken in reliance on it is strictly prohibited. If you have received this email in error please contact the sender. Any views or opinions presented in this email are solely those of the author and do not necessarily represent those of Praxis High Integrity Systems Ltd (Praxis HIS). Although this email and any attachments are believed to be free of any virus or other defect, no responsibility is accepted by Praxis HIS or any of its associated companies for any loss or damage arising in any way from the receipt or use thereof. The IT Department at Praxis HIS can be contacted at [EMAIL PROTECTED] **
