### Re: [SC-L] Theoretical question about vulnerabilities

David Crocker wrote: Well, that approach is certainly better than not guarding against buffer overflows at all. However, I maintain it is grossly inferior to the approach we use, which is to prove that all array accesses are within bounds. Proving that all array accesses are within bounds would

### RE: [SC-L] Theoretical question about vulnerabilities

Crispin wrote: 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

### RE: [SC-L] Theoretical question about vulnerabilities

Crispin Cowan wrote: 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

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

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

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

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

### Re: [SC-L] Theoretical question about vulnerabilities

David Crocker wrote: 3. Cross-site scripting. This is a particular form of HTML injection and would be caught by the proof process in a similar way to SQL injection, provided that the specification included a notion of the generated HTML being well-formed. If that was missing from the

### Re: [SC-L] Theoretical question about vulnerabilities

Nash wrote: ** It would be extremely interesting to know how many exploits could be expected after a reasonable period of execution time. It seems that as execution time went up we'd be less likely to have an exploit just show up. My intuition could be completely wrong, though. I would think

### Re: [SC-L] Theoretical question about vulnerabilities

Pascal Meunier [EMAIL PROTECTED] writes Do you think it is possible to enumerate all the ways all vulnerabilities can be created? Is the set of all possible exploitable programming mistakes bounded? I believe that one can make a Turing machine halting argument to show that this is impossible.

### Re: [SC-L] Theoretical question about vulnerabilities

Or until you find a bug in your automated prover. Or, worse, discover that a vulnerability exists despite your proof, meaning that you either missed a loophole in your spec or your prover has a bug, and you don't have the slightest idea which. On that basis, can I presume that you believe

### RE: [SC-L] Theoretical question about vulnerabilities

Pascal Meunier wrote: Do you think it is possible to enumerate all the ways all vulnerabilities can be created? Is the set of all possible exploitable programming mistakes bounded? No. It's not so much a programming problem, more a specification problem. Tools now exist that make it possible

### Re: [SC-L] Theoretical question about vulnerabilities

Pascal Meunier wrote: Do you think it is possible to enumerate all the ways all vulnerabilities can be created? Is the set of all possible exploitable programming mistakes bounded? By bounded I take you to mean finite. In particular with reference to your taxonomy below. By enumerate I take