> -----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 Meunier wrote:
[snip] > > > All we can hope is to come reasonably close and produce > something useful, > > but not theoretically strong and closed. > > I think that there's lots of work going on in proof theory > and Semantics > that makes me hopeful we'll eventually get tools that are both useful > and strong. Model Checking is one approach and it seems to > have alot of > promise. It's relatively fast, e.g., and unlike deductive > approaches it > doesn't require a mathematician to drive it. See [Clarke] for details. > [Clarke] is very interesting, I think. He explicitly argues that model > checking beats other formal methods at dealing with the "state space > explosion" problem. > > Those with a more practical mind-set are probably laughing > that beating > the other formal methods isn't really saying much because they are all > pretty awful. ;-) > While I agree that model checking is immensely useful, I am not sure that the rest of the above statement is really true any more. Formal methods are much more widely used than is generally known and advances (especially in computing power) have made them much more practical. The "pretty awful" methods that Pascal alludes to generally suffered from trying to solve the wrong problem. They sought to allow proof of arbitrary properties of arbitrarily written programs in ambiguous programming languages. Given that challenge it is not suprising that they struggled. Where we see the greatest success is where languages are carefully designed to allow them to be provable and where the proof technology is used to help in the construction of correct programs rather than in the retrospective analysis of already constructed programs. Examples of this approach are SPARK from my own company and Perfect from Escher Technology. Using SPARK, we have built a a system for "a rather large USA security agency" to Common Criteria 5+ which has been independently analysed and tested with zero defects found. Since it was also cheaper than the system it replaced, this does at least suggest that more formal approaches are practical. regards Peter -------------------------------------------------------- Peter Amey BSc ACGI CEng MRAeS Chief Technical Officer direct: +44 (0) 1225 823761 mobile: +44 (0) 7774 148336 [EMAIL PROTECTED] Praxis High Integrity Systems Ltd 20 Manvers St., Bath, BA1 1PX, UK t: +44 (0)1225 466991 f: +44 (0)1225 469006 w: www.praxis-his.com -------------------------------------------------------- [snip] ********************************************************************** 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] **********************************************************************
