> -----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 > > > 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] **********************************************************************
