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.resear

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 f

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 mo

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

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 co

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

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 f

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

[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 exper

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 A