RE: Theoretical question about vulnerabilities

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

> -----Original Message-----
> From: [EMAIL PROTECTED]
> [mailto:[EMAIL PROTECTED]
> Behalf Of Nash
> Sent: 11 April 2005 21:38
> To: Pascal Meunier
> Cc: [EMAIL PROTECTED]
> 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]

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