Crispin wrote:
>>
Proving that all array accesses are within bounds would seem to be
Turing undecidable. Either you are not proving what you way you are
proving, or your programs are not full Turing machines.
Proof:
Issue: Some people may regard diagonalized programs are a contrivance,
and are
> -Original Message-
> From: [EMAIL PROTECTED]
> [mailto:[EMAIL PROTECTED]
> Behalf Of Crispin Cowan
> Sent: 15 April 2005 20:58
> To: David Crocker
> Cc: SC-L@securecoding.org
> Subject: Re: [SC-L] Theoretical question about vulnerabilities
>
>
> Davi
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 see
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 tha
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 sen
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.resear
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 f
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 mo
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
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
>>> [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 f
> -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 alway
>> 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 be
der Mouse wrote:
>>
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.)
<<
It is of cour
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 impossib
> [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 doi
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
> -Original Message-
> From: [EMAIL PROTECTED]
> [mailto:[EMAIL PROTECTED]
> Behalf Of Nash
> Sent: 11 April 2005 21:38
> To: Pascal Meunier
> Cc: SC-L@securecoding.org
> Subject: Re: [SC-L] Theoretical question about vulnerabilities
>
>
> Pascal Meunie
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 specificati
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
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 possi
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?
Yes and no.
Yes, if your enumeration is "1" and that is the set of all errors that
allow an attacker to induce un
22 matches
Mail list logo
