RE: Theoretical question about vulnerabilities

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

> -----Original Message-----
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Crispin Cowan
> Sent: 15 April 2005 20:58
> To: David Crocker
> Cc: [EMAIL PROTECTED]
> Subject: 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 seem to be 
> Turing undecidable. Either you are not proving what you way you are 
> proving, or your programs are not full Turing machines.

Since we do it and have been doing it for years then there must be some explanation.  I suspect the answer is that the 
programs for which we perform such proofs are indeed "not full Turing machines".  Typically they are jet engine 
controllers, crypto switches or other rather less generalised devices.

I am willing to agree that there may be a class of programs that are free from buffer overflows which cannot show to be 
so; however, this does not matter.  We are interested in avoiding the class of programs which _do_ have a buffer 
overflow vulnerabilities and those we can indeed find.  If we encounter something that is in the first class, the only 
effect is that we might have to strengthen the code in some, strictly unnecessary, way in order to complete the proof.

> Proof: <insert diagonalization argument here :>
>
> Issue: Some people may regard diagonalized programs are a 
> contrivance, 
> and are only interested in correctness proofs for real programs (for 
> some value of "real").

Correct, I am only interested in real cases but for an extremely large set of values of "real" (into which set has 
fitted every real-world program that I have been involved in in the last 10+ years).  Furthermore, as discussed above, 
the cases which fall outside "real" fall outside in a safe way.

> Crispin's rebuttal: Suppose I want to prove that your program checker 
> does not have any illegal array references ...

Well you can't other than by applying pragamatic means such as analysing itself, using someone else's tool to analyse 
it or, of course, testing it a lot (none of which constitute proof).  This point is, firstly, a quite separate one from 
theoretical limitations of proof, it is a question about tool trustworthiness which applies to compilers, linkers and 
microprocessors equally well.  And, secondly, it is largely irrelevent to the question of whether proof techniques help 
us build better programs and can provide protection against the kinds of error that we know are significant in safety 
and security.  To suggest, as some people seem to, that application of the Entscheidungs principle somehow eliminates 
proof from consideration is risible.  There are equally good proofs (from Bev Littlewood and Butler and Finelli) that 
dynamic testing is incapable of giving confidence in the reliablity of software beyond certain rather low limits; 
however,  I don't here people arguing that we!
  should stop testing! 


[snip]
> Crispin


regards

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]

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