RE: Theoretical question about vulnerabilities

["Peter Amey" <peter.amey () praxis-his com>]

> -----Original Message-----
> From: [EMAIL PROTECTED]
> [mailto:[EMAIL PROTECTED]
> Behalf Of der Mouse
> Sent: 12 April 2005 05:15
> To: [EMAIL PROTECTED]
> 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]

**********************************************************************