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
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
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
-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
[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
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
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
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
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
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.
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
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
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
13 matches
Mail list logo
