Re: [SC-L] But what proof do we have that any of it makes a difference?

[Peter Amey]

 

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of Goertzel, Karen
> Sent: 25 June 2007 19:49
> To: Secure Coding
> Subject: [SC-L] But what proof do we have that any of it 
> makes a difference?
> 
> There are two closely-related questions that keep arising for 
> which I still can find no satisfying answer (for me 
> "satisfying" means "supported by concrete evidence"):
> 
> [1] Will using a secure SDLC methodology (or a set of secure 
> development "best practices") actually produce software that 
> will, when deployed "in the wild" resist or tolerate attacks 
> and attempted executions of inserted/embedded malicious code 
> better than software whose developers did not use a secure 
> SDLC methodology?
> 
> [2] Will software that adheres to a set of "security 
> principles", when deployed "in the wild", actually resist or 
> tolerate attacks and attempted execution of inserted/embedded 
> malicious code better than software whose developers did not 
> adhere to security principles?
> 
> 
You might find some useful evidence here: 

http://www.praxis-his.com/pdfs/issse2006tokeneer.pdf

The NSA were cetainly impressed with benefits of a rigorous engineering
approach to software development.

Peter



Peter Amey BSc ACGI CEng CITP MRAes FBCS


CTO (Software Engineering)

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



 


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. 

Although this email and any attachments are believed to be free of any virus or 
other defect, no responsibility is accepted by Praxis 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 can be contacted at [EMAIL PROTECTED]

Praxis High Integrity Systems Ltd:

Company Number: 3302507, registered in England and Wales

Registered Address: 20 Manvers Street, Bath. BA1 1PX

VAT Registered in Great Britain: 682635707


___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Tools: Evaluation Criteria

[Peter Amey]

 

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of Wall, Kevin
> Sent: 24 May 2007 12:45
> To: McGovern, James F (HTSC, IT)
> Cc: SC-L@securecoding.org
> Subject: Re: [SC-L] Tools: Evaluation Criteria
> 
> James McGovern wrote...
> 
> > Maybe folks are still building square windows because we haven't 
> > realized how software fails and can describe it in terms of 
> a pattern.
> > The only pattern-oriented book I have ran across in my 
> travels is the 
> > Core Security Patterns put out by the folks at Sun. Do you think we 
> > should stop talking solely about code and start talking about how 
> > vulnerabilities are repeatedly introduced and describe 
> using patterns 
> > notation?
> 
[snip

I am very happy to accept that we may not understand /all/ or even
/most/ of the ways software fails but we do know an awful lot.  Buffer
overflows, numeric overflows and division by zero have been wee
understood for years.  The first was limited by various versions of
Pascal ages ago.  Yet we are still clinging to techniques that hope we
can spot a buffer overflow "pattern" after construction (and hopefully
before an exploiter!).

There is a nice symmetry about my aeronautical analogy.  The Comet
disasters occurred just over 50 years after the Wright brothers first
flew; and we are still fiddling around with buffer overflows just over
50 years after Colossus (at the Bletchley Park crypto centre of Enigma
fame) signalled the start of the computer age.

That's all, back to the asylum!


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. 

Although this email and any attachments are believed to be free of any virus or 
other defect, no responsibility is accepted by Praxis 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 can be contacted at [EMAIL PROTECTED]

Praxis High Integrity Systems Ltd:

Company Number: 3302507, registered in England and Wales

Registered Address: 20 Manvers Street, Bath. BA1 1PX

VAT Registered in Great Britain: 682635707


___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Tools: Evaluation Criteria

[Peter Amey]

 

[snip]
> 
> Good to see that folks are expanding the criteria in terms of 
> what it scans for, but criteria as to how it integrates is 
> also equally useful.
> 

On the contrary I find the idea of evaluating tools by "what they scan
for" very disturbing.  It shows a continuing belief that software
engineering involves building things then "scanning" them for defects.
We /must/ move to tools and methods that help us construct correct
programs rather than looking for defects in them afterwards.

Let me give you an example from my previous aeronautical career.  The
DeHavilland Comet was the world's first transatlantic jet airliner.  All
went well until after a year of two of service there were a series of
catastrophic airframe failures in flight, all with total loss of those
on board.  ISTR that there were 3 crashes in all.  The design defect
that caused the disasters was a combination of square cabin windows and
hull pressurisation on each flight.  The square windows caused amplified
stress at each window corner which, with the cyclic stress changes from
pressurisation caused metal fatigue failures and hull loss.  Metal
fatigue was little understood at the time.

Now for the lessons.  The aero industry quickly learned about metal
fatigue and stress raisers and used that information to design fuselages
that did not suffer from the Comet's defects.  That is why your airliner
window is oval not square.  There have been very, very few Comet-style
failures since (and they are usually associated with corrosion or poor
maintenance).  So, the problem was analysed, understood, disseminated
and hence eliminated.

In the software world we seem to content to build "window squareness
detection tools".  Some will find 70% of square windows but miss others
and produce false alarms in yet other cases.

Buffer overflows are the square windows of secure software: we shouldn't
be /scanning/ for them but using languages and tools that /prevent/
their introduction.

Regards


Peter

----

Peter Amey BSc ACGI CEng CITP MRAes FBCS

CTO (Software Engineering)
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



 



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. 

Although this email and any attachments are believed to be free of any virus or 
other defect, no responsibility is accepted by Praxis 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 can be contacted at [EMAIL PROTECTED]

Praxis High Integrity Systems Ltd:

Company Number: 3302507, registered in England and Wales

Registered Address: 20 Manvers Street, Bath. BA1 1PX

VAT Registered in Great Britain: 682635707


___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Tools: Evaluation Criteria

[Peter Amey]

 




From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of McGovern, James F
(HTSC, IT)
Sent: 22 May 2007 14:48
To: SC-L@securecoding.org
Subject: [SC-L] Tools: Evaluation Criteria


We will shortly be starting an evaluation of tools to assist in
the secure coding practices initiative and have been wildly successful
in finding lots of consultants who can assist us in evaluating but
absolutely zero in terms of finding RFI/RFPs of others who have
travelled this path before us. Would especially love to understand
stretch goals that we should be looking for beyond simple stuff like
finding buffer overflows in C, OWASP checklists, etc.
[PNA] 
 
For some "stretch goals ", take a look at www.sparkada.com and
some of the published papers there, especially one on a project called
Tokeneer.
(Caveat: I am commercially involved in the SPARK tools.
 
In my travels, it "feels" as if folks are simply choosing tools
in this space because they are the market leader, incumbent vendor or
simply asking an industry analyst but none seem to have any "deep"
criteria. I guess at some level, choosing any tool will move the needle,
but investments really should be longer term.


[PNA] 
Agreed
 
 
Peter
 

----

Peter Amey BSc ACGI CEng CITP MRAes FBCS


CTO (Software Engineering)

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 <http://www.praxis-his.com/> 



 



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. 

Although this email and any attachments are believed to be free of any virus or 
other defect, no responsibility is accepted by Praxis 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 can be contacted at [EMAIL PROTECTED]

Praxis High Integrity Systems Ltd:

Company Number: 3302507, registered in England and Wales

Registered Address: 20 Manvers Street, Bath. BA1 1PX

VAT Registered in Great Britain: 682635707

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Compilers

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of ljknews
> Sent: 02 January 2007 14:20
> To: Secure Coding
> Subject: Re: [SC-L] Compilers
> 
> At 2:18 PM + 1/2/07, Peter Amey wrote:
> > [snip]
> > 
> > 
> > We think so!  However, like everything else, it is how you 
> use things 
> > that matter most.
> 
> How you use things may be an "essential" aspect, but so is 
> the nature of "things".  Achieving the same quality by 
> toggling the machine code into the front panel is only 
> possible on a theoretical basis, and getting the same results 
> with a long strand of limp spaghetti is just impossible.

Larry,

I don't think I was intending to disagree with you!  The right languages
/allow/ demonstrable secure coding.  Conversely, without them, secure
coding is reduced to a fairly weak coding standard level.  

Peter

P.S.  Please watch for the unfortunate word wrap in the URL of my
original post.  The broken link still works but goes to thw wrong place!


___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Compilers

[Peter Amey]

[snip]

> Isn't the whole basis of Spark a matter of adding proof 
> statements in the comments ?  I don't think the general 
> compiler marketplace would go for that built-in to compilers. 
>  After all:
> 
>   1. The Praxis implementation can be used with multiple compilers
> 
>   2. The compiler market is so immature that some people are still
>  using C, C++ and Java.
> 
> But for the high-integrity market, Spark seems to fit the bill.
> --
> Larry Kilgallen

We think so!  However, like everything else, it is how you use things
that matter most.  What SPARK allows is very effective secure coding
(what this list is all about).  There is an entry on this subject on the
Build Security In website:
https://buildsecurityin.us-cert.gov/daisy/bsi/articles/knowledge/sdlc/61
3.html.

regards

Peter

___
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
___

Re: [SC-L] Why Shouldn't I use C++?

[Peter Amey]

 

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of Robert C. Seacord
> Sent: 01 November 2006 10:16
> To: Ben Corneau
> Cc: SC-L@securecoding.org
> Subject: Re: [SC-L] Why Shouldn't I use C++?
> 
> Ben,
> 
> I would not go so far as to say never use C++.  It is 
> probably the most powerful and expressive commercially 
> successful programming language available today ...

... other than Ada, which has all the OO capability of C++, language
level support for multi-threaded programs and suffers from none of the
problems that exercise this discussion list so regularly. 

regards


Peter



___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php

Re: [SC-L] How can we stop the spreading insecure coding examplesattraining classes, etc.?

[Peter Amey]

 

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of Tim Hollebeek
> Sent: 30 August 2006 18:23
> To: 'Wall, Kevin'; SC-L@securecoding.org
> Subject: Re: [SC-L] How can we stop the spreading insecure 
> coding examplesattraining classes, etc.?
> 
> 
> Really, the root of the problem is the fact that the simple 
> version is short and easy to understand, and the secure 
> version is five times longer and completely unreadable.  
> While there always is some additional complexity inherent in 
> a secure version, it is nowhere near as bad as current 
> toolkits make it seem.
> 

No, the root cause of the problem is the use of inadequate notations so
that we have to make secure versions 5 times as long in order to
overcome those inadequacies.  From my experience a typical secure SPARK
implementation (which we have proved to be free from buffer overflow,
numeric range violation etc.) is no longer or more complex than its
simple version.

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]

**


___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php

Re: [SC-L] Cost of provably-correct code

[Peter Amey]

 [Re-send, I am not sure the first copy made it to the list]

> -Original Message-
> From: [EMAIL PROTECTED]
> [mailto:[EMAIL PROTECTED]
 ] On Behalf Of Crispin Cowan
> Sent: 21 July 2006 18:45
> To: mikeiscool
> Cc: SC-L@securecoding.org
> Subject: Re: [SC-L] bumper sticker slogan for secure software
> 
> mikeiscool wrote:
> > On 7/21/06, Dana Epp <[EMAIL PROTECTED]> wrote:
> > 
> >>> yeah.
> >>> but none of this changes the fact that it IS possible to
> write completely secure code.
> >>> 
> >> And it IS possible that a man will walk on Mars someday. 
> But its not
> >> practical or realistic in the society we live in today. I'm sorry 
> >> mic, but I have to disagree with you here.
> >>
> >> It is EXTREMELY difficult to have code be 100% correct if an 
> >> application has any level of real use or complexity. There
> will be security defects.
> >> 
> > Why? Why accept this as a fact? It is not a fact. If you put 
> > procedures in place and appropriately review and test you can be 
> > confident.
> > 

> Sorry, but it is a fact. Yes, you can have provably correct code. Cost

> is approximately $20,000 per line of code. That is what the 
> "procedures"
> required for correct code cost. Oh, and they are kind of super-linear,

> so one program of 200 lines costs more than 2 programs of 100 lines.

I would be fascinated to know where this figure comes from. Our
experience is that formal development methods, which at least offer the
possibility of defect-free software, are /cheaper/ as well as resulting
in lower rates of defect. At least one major organization, with rather a
strong interest in security, agrees with us (see:
http://www.praxis-his.com/news/TokeneerNews.asp
  or, for the full
paper, http://www.praxis-his.com/pdfs/issse2006tokeneer.pdf
 ).

I think we have to /aim/ for zero defects and choose technical
approaches that make that aim credible. If we don't then what defect
rate shall we aim for and how will we know if we have achieved it? 

Of course, as good engineers, we should never allow ourselves the hubris
of /believing/ we have achieved zero defects but that doesn't invalidate
the aim. (Aircraft manufacturers do a great deal of mathematical
analysis of stresses in wings but still proof load test each new design;
they don't expect to find any problems because of the amount of analysis
they have done but, very occasionally, they do).

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]

**


___
Secure Coding mailing list (SC-L)
SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php

RE: [SC-L] Theoretical question about vulnerabilities

[Peter Amey]

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

**

RE: [SC-L] Theoretical question about vulnerabilities

[Peter Amey]

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

**

RE: [SC-L] Theoretical question about vulnerabilities

[Peter Amey]

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

**

RE: [SC-L] How do we improve s/w developer awareness?

[Peter Amey]

[snip]
> 
> Remember that little incident in 2000 when the London 
> millennium bridge was
> closed immediately after opening due to excessive wobbling when people
> walked across it? I can't guarantee that my recollection is 
> accurate, but
> I'm sure they were trying to put this down to that software classic, a
> 'Design feature'.

The Millenium Bridge wobble is indeed instructive.  Engineering is usually a 
profession that is conservative and places great emphasis on codifying and 
learning from past mistakes.  Much bridge design work uses well-established, 
trustworthy principles.  The Millenium Bridge designers deliberately pushed the 
boundaries to produce something novel and exciting.  Never before had a 
suspension bridge had the suspension and decking in the same plane (i.e. the 
deck doesn't "hang" from the suspension, its balanced on/between the 
suspension).  The result was strong enough but had unexpected dynamics i.e. it 
wobbled!
I am confident that this experience is already in the text books, standard data 
tables and CAD tools.  The engineering body of knowledge had been added to and 
the problem should not recur.

This is where the software community can learn:

1.  We are appalling at learning from previous mistakes (other than in 
perfecting our ability to repeat them!)
2.  We routinely push the boundaries of what we try and achieve by leaping 
instead of stepping.
3.  We routinely adopt novel and untried technology in preference to proven and 
trustworthy alternatives.  Indeed, mature technology often seems to be rejected 
precisely because it is not new, novel or exciting enough.

The Millenium Bridge made news precisely because such engineering faiures are 
rare; software engineering failures make the news because they are so common 
the papers would be empty if they weren't reported! 

[snip]

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]

**

RE: [SC-L] Programming languages -- the "third rail" of secure co ding

[Peter Amey]

[snip]
> 
> As engineers, we need "good enough", not perfection.
> 

We also need:

(1) To recognise when things aren't "good enough"
(2) To have a migration path to "better"

Peter
 


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Programming languages -- the "third rail" of secure coding

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Michael S Hines
> Sent: 20 July 2004 14:17
> To: [EMAIL PROTECTED]
> Subject: RE: [SC-L] Programming languages -- the "third rail" 
> of secure
> coding
> 
> 
> I've been compiling a list of programming languages..   Some 
> of which were
> developed to 'solve' the insecure programming problem.  I 
> don't think we've
> made it yet.
> 
> Perhaps it's a personnel problem, not a technology problem?
> 

True.  Except that a major part of the "personnel problem" is the refusal of the 
personnel to be open minded and objective about their choice of technology!

Peter
 


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Programming languages used for security

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of ljknews
> Sent: 12 July 2004 14:24
> To: [EMAIL PROTECTED]
> Subject: Re: [SC-L] Programming languages used for security
> 
> 
> At 3:55 PM -0700 7/10/04, Crispin Cowan wrote:
> 
> > However, I think I do see a gap between these extremes. You 
> could have
> > a formal specification that can be mechanically transformed into a
> > *checker* program that verifies that a solution is correct, 
> but cannot
> > actually generate a correct solution.
> 
> Isn't that pretty much what the SPARK Inspector does ?

Yes, the "posit and verify" approach.  We adopted this because we think there are 
problems with refining specs into code.  One problem is that there can be (usually 
will be) more than one valid way of implementing a spec.  For example, the spec may 
make the abstract assertion that a list is "ordered".  The implementation could build 
an ordered tree structure, write to a buffer that is periodically quicksorted or even 
write to a set of temporary files that are periodically merge sorted.  The design 
choice may depend on non-functional requirements such as performance or amount of free 
memory.  Therefore we don't see how you can always generate the most appropriate code 
for the property "ordered".  

One solution to this is to use very low-levels of specification that avoid the gap 
between the abstract concept ordered and the code itself.  This can easily fall into 
the trap that the specification language simply becomes code (a problem with B for 
example).  Our approach is to embed the property "ordered" as an annotation in the 
code , allow the designer to choose an appropriate solution and then provide 
facilities to show that the implementation preserves the required property.  The SPARK 
Examiner generates the required proof obligations to do this.  There is therefore 
clear blue water between the specification ("what") and the code ("how") but with a 
rigorous way of showing correspondence between them.

Peter


This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Education and security -- another perspective (was "ACM Queue - Content")

[Peter Amey]

> -Original Message-
> From: Crispin Cowan [mailto:[EMAIL PROTECTED]
> Sent: 09 July 2004 04:27
> To: Peter Amey
> Cc: ljknews; [EMAIL PROTECTED]
> Subject: Re: [SC-L] Education and security -- another perspective (was
> "ACM Queue - Content")
> 
> 
> Peter Amey wrote:
> 
> >>>What is wrong with this picture ?
> >>>
> >>>I see both of you willing to mandate the teaching of C and yet not
> >>>mandate the teaching of any of Ada, Pascal, PL/I etc.
> >>>  
> >>>
> >>Makes sense to me. what is the point of teaching dead 
> languages like 
> >>Ada, Pascal, and PL/I?  Teach C, Assembler, and Java/C# (for the 
> >>mainstream), and some lisp variant (Scheme, ML, Haskell) and Prolog 
> >>variant for variety. But Ada, Pascal, and PL/I are suitable 
> >>only for a "history of programming languages" course :)
> >>
> >>
> >I do hope that is a sort of smiley at the end of your 
> message.  Please.
> >  
> >
> It is a sort-of smiley. On one hand, I find the whole thing 
> amusing. On 
> the other hand, I find it patently absurd that someone would suggest 
> that curriculum in 2004 would comprise Ada, Pascal, and PL/I, all of 
> which are (for industrial purposes) dead languages.
> 
> On one hand, university should be about learning concepts rather than 
> languages, because the concepts endure while the languages go 
> in and out 
> of fashion. 

[snip]

I would have to (at least partly) diagree on two counts.  

Firstly a tactical one: Ada is by no means a dead language.  There is a great tendency 
in our industry to regard whatever is in first place at any particular point in life's 
race to be "the winner" and everything else to be "dead".  In practice very 
substantial use may continue to be made of things which are not in the ultra-visible 
first place.  For example, OS/2 was killed by Windows yet most ATMs in the USA still 
run OS/2.  We have't discussed the dead languages Cobol and Prolog but both are 
actually still in widespread use, the latter in the specific niches for which it is 
suitable.  Ada is actually still doing rather well in areas where high reliability is 
valued more than fashion (the Ada side of my business is growing steadily and has been 
for years).  Since we are concerned on this list with improving the security (a form 
of reliability) of systems, study of a language which has a proven track record in 
delivering relibaility is wholly appropriate.

Secondly, in response to your suggestion that we teach concepts (which I wholly agree 
with), languages, including dead ones, encapsulate and illustrate concepts.  Pascal 
was designed to teach structured programming.  Occam provides a splendid introduction 
to concurrency.  Modula-2 and Ada are ideal for illustrating the vital concepts of 
abstraction, encapsulation and the separation of specification and implementation.  
The languages are worth studying for these reasons alone.  Those exposed to them will 
be better programmers in any language and will find adoption of new ones much easier.  

As you say, languages come in and out of fashion; what I find sad is that so many of 
the new languages have failed to learn and build on the lessons of those that have 
gone before.  I think it highly probable that this is because their designers have 
casually dismissed those that went before as dead and therefore of no interest.  They 
would have done better to emulate Newton and "stood on the shoulders of giants" such 
as Wirth.

I would never recruit someone just because they knew Ada rather than C; however, I 
would be highly unlikely to recruit someone who had such a closed mind that they 
thought Ada had nothing to teach them and was only fit for snide mockery.


Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Education and security -- another perspective (was "ACM Queue - Content")

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of der Mouse
> Sent: 08 July 2004 03:47
> To: [EMAIL PROTECTED]
> Subject: Re: [SC-L] Education and security -- another perspective (was
> "ACM Queue - Content")
> 
> 
> > I see both of you willing to mandate the teaching of C and yet not
> > mandate the teaching of any of Ada, Pascal, PL/I etc.
> 
> > This seems like the teaching of "making do".
> 
> And is not making do an important skill?
> 

Absolutely, "making do" is an important skill.  However, those being taught have to be 
told that they are "making do" and made properly aware of the alternatives.  In fact 
showing them the superiority of the alternatives should help them understand the 
limitations of C and why they need to know how to "make do"!

What is not acceptable is to deprive them of the knowledge of superior alternatives 
and leave them thinking that "making do" is the state of the art.

Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Education and security -- another perspective (was "ACM Queue - Content")

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Crispin Cowan
> Sent: 07 July 2004 23:29
> To: ljknews
> Cc: [EMAIL PROTECTED]
> Subject: Re: [SC-L] Education and security -- another perspective (was
> "ACM Queue - Content")
> 
> 
> ljknews wrote:
> 
> >What is wrong with this picture ?
> >
> >I see both of you willing to mandate the teaching of C and yet not
> >mandate the teaching of any of Ada, Pascal, PL/I etc.
> >  
> >
> Makes sense to me. what is the point of teaching dead languages like 
> Ada, Pascal, and PL/I?  Teach C, Assembler, and Java/C# (for the 
> mainstream), and some lisp variant (Scheme, ML, Haskell) and Prolog 
> variant for variety. But Ada, Pascal, and PL/I are suitable 
> only for a 
> "history of programming languages" course :)
> 

I do hope that is a sort of smiley at the end of your message.  Please.

Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] ACM Queue article and security education

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Blue Boar
> Sent: 01 July 2004 21:03
> To: ljknews
> Cc: [EMAIL PROTECTED]
> Subject: Re: [SC-L] ACM Queue article and security education
> 
> 
> ljknews wrote:
> > I think it will be properly considered when the most strict portion
> > of the software world is using language X.   I have used many
> > programs where the flaws in the program make it clear that 
> I care not
> > one whit about whether the authors of that program have 
> opinion about
> > anything I might use. They are simply not competent, either as
> > individuals or else as an organization.
> 
> By "most strict portion", do you mean people that care most about 
> correct code, proofs, and such?  I don't deny that the bulk 
> of the heavy 
> lifting will be done by people well-qualified to do so.  
> However, I'm of 
> the school of thought that certain types of people who like to break 
> things, and whose chief skill is breaking things, will always have a 
> decent shot at finding a problem.  There are people who 
> couldn't build 
> it, but they can sure break it.
> 
> You don't typically get their attention until something is really, 
> really popular.  So yes, you can write your stuff in Language X, and 
> assume it's secure.  It might not actually be until the whole 
> world has 
> had its way with Language X, but (hopefully) that's not a 
> problem.  You 
> can still do the dance of patching the last 5 problems in Language X, 
> and end up better off that if you'd just used C.
> 
> Even Knuth has to write checks ocassionally, and he does a 
> lot of proof 
> work, doesn't he?
> 
> So, if Language X only has 5 problems total, even if it takes 
> years to 
> ferret them out, butthey are fixable, please proceed with getting the 
> whole world to use Language X.
> 

I'm not entirely sure I follow this.  I _think_ you are saying: "since we can't be 
sure that X is perfect (because it might have 5 remaining flaws) then there is no 
point in adopting it".  You seem to be saying that it doesn't matter if X is 
_demonstrably_much_better_ than Y, if it is not perfect then don't change.  Have I got 
that right?

This is a variant on the Goedel gambit often used to attack formal verification.  It 
goes "since Goedel's Theorem places strict limits on what we can formalize and prove, 
let's not bother at all and just do a few unit tests instead".  It also reminds me of 
what I call the asprin analogy: "aspirin doesn't cure cancer so there's no point in 
taking it for headaches".

The reality is that demonstrable improvements in quality, safety and security can be 
achieved by using the right tools, languages and methods.  It is for those who choose 
_not_ to use the strongest engineering to justify their position not the other way 
round.


Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] ACM Queue article and security education

[Peter Amey]

> -Original Message-
> From: Blue Boar [mailto:[EMAIL PROTECTED]
> Sent: 01 July 2004 17:11
> To: Peter Amey
> Cc: [EMAIL PROTECTED]
> Subject: Re: [SC-L] ACM Queue article and security education
> 
> 
> Peter Amey wrote:
> > There are languages which are more suitable for the construction of
> > high-integrity systems and have been for years.  We could have
> > adopted Modula-2 back in the 1980s, people could take the 
> blinkers of
> > prejudice off and look properly at Ada.  Yet we continue to use
> > C-derived languages with known weaknesses.
> 
> So we trade the known problems for a set of unknown ones?  

[snip]

A mindset that would have kept us building aircraft in wood!

In any case, we _do_ adopt new languages and methods, frequently.  In the time I have 
been using SPARK I have had people say: "that's neat, if only you could do it for X".  
Where X has been C, C++, Java and C# in that order and at about 5 year intervals.  
What we _don't_ do is make those choices based on any kind of objective assessment or 
engineering judgement.

[snip]

> Language X may very well be a much better starting point, I 
> don't know. 
>   I do believe that it will never be properly looked at until 
> the whole 
> world starts using it for everything, though.

And how will the whole world start using it if everyone waits for everyone else?

In any case, I don't expect the whole world to adopt any one method (any more than I 
build bicycles in carbon fibre even though that is the material of choice for, say, 
racing cars).   What I do expect is that principled engineers, the kind of people who 
care enough about their profession to contribute to groups like this, will seek to use 
the best and most appropriate technology for their purposes.  


Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] ACM Queue article and security education

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Michael S Hines
> Sent: 30 June 2004 17:00
> To: [EMAIL PROTECTED]
> Subject: RE: [SC-L] ACM Queue article and security education
> 
> 
> If the state of the art in automobile design had progressed 
> as fast as the
> state of the art of secure programming - we'd all still be 
> driving Model
> T's.  
> 
> Consider-
>   - System Development Methods have not solved the (security) 
> problem -
> though we've certainly gone through lots of them.
>   - Languages have not solved the (security) problem - though we've
> certainly gone through (and continue to go through) lots of them.
>   - Module/Program/System testing has not solved the 
> (security) problem -
> though there has been a plethorea written about system 
> testing (both white
> box and black box).
> 

I agree that we have not solved the problem by the above means but I think it should 
be said that this is due more to the refusal of our industry to make a serious attempt 
to use them than because they have used them and failed.  The reality is that most 
system development still uses ad hoc, informal approaches and inherently insecure and 
ambiguous implementation languages.  Testing cannot make up for these deficiencies 
because of fundamental limitations of coverage etc. see [1,2,3].

There are development approaches, such as the use of formal methods, which have a 
proven track record of success.  They are still being used successfully today.  Yet 
most of our industry is either unaware of them, regards formal methods as some 
academic failure from the 1970s or demands "evidence" (although they never seem to 
need evidence before adopting the latest fashionable fad).

There are languages which are more suitable for the construction of high-integrity 
systems and have been for years.  We could have adopted Modula-2 back in the 1980s, 
people could take the blinkers of prejudice off and look properly at Ada.  Yet we 
continue to use C-derived languages with known weaknesses.  All we hear are appeals to 
better training, tools to help find the stupidities the poor development approaches 
make inevitable and pious hopes that future developments in computer science will 
rescue us.  What we really need is to use the good stuff we already have.

Just to back this random polemic up a bit:  we have just delivered a secure system to 
an important customer which has been independently evaluated to a high level.  Zero 
defects were found.  It was cheaper than the system it replaces.  (Draconian NDAs 
limit what can be said to that unfortunately).  The system was formally specified in 
Z, coded in SPARK and proofs carried out to ensure that it was wholly free from 
run-time errors (and hence from attacks such as buffer overflow) and that essential 
security invariants are maintained.  None of this is bleeding edge technology.  Z has 
been around for ages, SPARK for 14 years.  



regards



Peter


1. Littlewood, Bev; and Strigini, Lorenzo: Validation of Ultrahigh Dependability for 
Software-
Based Systems. CACM 36(11): 69-80 (1993)
2. Butler, Ricky W.; and Finelli, George B.: The Infeasibility of Quantifying the 
Reliability of
Life-Critical Real-Time Software. IEEE Transactions on Software Engineering, vol. 19, 
no.
1, Jan. 1993, pp 3-12.
3. Littlewood, B: Limits to evaluation of software dependability. In Software 
Reliability and
Metrics (Proceedings of Seventh Annual CSR Conference, Garmisch-Partenkirchen). N.
Fenton and B. Littlewood. Eds. Elsevier, London, pp. 81-110.



**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] SPI, Ounce Labs Target Poorly Written Code

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Blue Boar
> Sent: 28 June 2004 21:35
> To: Kenneth R. van Wyk
> Cc: [EMAIL PROTECTED]
> Subject: Re: [SC-L] SPI, Ounce Labs Target Poorly Written Code
> 
> 
> Kenneth R. van Wyk wrote:
> > The article quotes SPI Dynamics' CTO 
> > as saying, "It doesn't require developers to learn about 
> security," which 
> > strikes me as being a rather bold statement.
> 
> I seriously doubt that there is a programming language that can do 
> anything useful that one can't do something stupid with.  Never bet 
> against the quality of idiots available in the world. :)
> 

Always willing to rise to a challenge.  But I'll cover my bets by slightly changing 
Blue Boar's words by adding "which wouldn't be obvious".  

I would assert that using SPARK it is very /hard/ to something stupid and /impossible/ 
to do something stupid that wouldn't be obvious to the SPARK Examiner tool.  In fact, 
the only way I can think of doing so would be to construct a formal specification for 
stupidity and then correctly implement it (which is clearly feasible).  

The first part of your challenge "that can do anything useful" is proved by the 
existence of real, useful prgorams written in SPARK.

Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] opinion, ACM Queue: Buffer Overrun Madness

[Peter Amey]

der Mouse (Maus surely?) wrote
[snip]
> 
> Well, actually, but for the world's addiction to sloppy coding.
> 
> It's entirely possible to avoid buffer overflows in C; it 
> just requires
> a little care in coding.  C's major failing in this regard - and I
> don't actually consider it all that major - is that it doesn't provide
> any tools to help.  It assumes that you the programmer know 
> what you're
> doing, and the mismatch between that and the common reality is where
> the problem actually comes from.


I dislike this commonly-used argument that essentially says "you should only employ 
above average people who don't make mistakes".  It is flawed on lots of levels.

1.  On average ability over our industry is average!
2.  Even brilliant, infallible programmers like me make mishtukes shummtimes.
3.  Even if above average, non-sloppy programmers can avoid mistakes, the effort they 
spend doing so is a distraction from their real job of solving the problem the program 
is intended for.
4.  The levels of mental abstraction needed to solve an application domain problem and 
to worry about operator precedence and buffer overflow are completely different; there 
is good evidence that humans don't work well at more than one abstraction level at a 
time.

> 
> All that a "better" language will bring you in this regard is that it
> will (a) push the sloppiness into places the compiler can't check and
> (b) change the ways things break when confronted with input beyond the
> design underlying their code.
> 

This sounds like the Syrius Cybernetics defence (from the Hitch Hiker's Guide to the 
Galaxy);  essentially you seem to be saying it is OK if all the deep and complex flaws 
in a product are completely obscured by all the shallow and obvious ones.  You can't 
assume that the sloppy programmer in C /only/ introduces shallow errors.

In practice, well designed languages can do much more than you claim.  They can 
completely eliminate whole classes of error that currently exercise our attention, 
make sloppiness very hard to conceal and make it much easier to find any subtle errors 
that remain.

Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Anyone looked at security features of D programming language compared to Spark?

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Jim & Mary Ronback
> Sent: 22 April 2004 19:57
> To: Greenarrow 1
> Cc: Kenneth R. van Wyk; [EMAIL PROTECTED]; James Walden; 
> Rod Chapman
> Subject: [SC-L] Anyone looked at security features of D programming
> language compared to Spark?
> 
> 
> Has anyone compared D with Spark. Spark is the high-integrity 
> Ada subset 
> which allows a very powerful static analysis, using a tool called the 
> Spark Examiner.

Might be interesting; however, I always deeply suspicious of feature comparison lists 
because what matters is "are the features useful or appropriate?".  You can easily 
conclude that an old and battered saloon/sedan car is better than a F1 racing car:

Sedan   F1
Number of doors 4  0
Number of windows   6  0
Seats   4  1
Fuel consumption   20  3
etc.

All great fun but not much good if you are going motor racing!

SPARK has a set of features carefully chosen to be suitable and sufficient for serious 
work while still allowing fast and very deep static analysis.  So your comparison 
tables would need some additional rows:

Exact semantics (source code completely predicts compiled behaviour)  YES
Complete freedom from implementation dependencies (e.g eevaluation order) YES
Statically verified design by contract YES
Static proof of freedom from all run time errors, array bounds violation etc. YES

and probably quite a few others.


Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk

RE: [SC-L] Missing the point?

[Peter Amey]

> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED]
> Behalf Of Pascal Meunier
> Sent: 20 April 2004 20:00
> To: Michael A. Davis
> Cc: [EMAIL PROTECTED]
> Subject: Re: [SC-L] Missing the point?
> 
> 
[snip]
> However, the PSP and 
> TSP seem to 
> be working well enough.  I wish I knew more about them, and that they 
> were not proprietary.
> 
> Cheers,
> Pascal Meunier
> 

Since you mention PSP and TSP then you shouldn't leave out Praxis's work on CbyC 
(Correctness by Construction).  CbyC was the only other process to compare favourably 
with TSP in the report "Improving Security Across the Software Development Lifecycle" 
just published by http://www.cyberpartnership.org).

And no, it's not proprietary, we would love to educate the world!  For starters, there 
are some CbyC papers on www.sparkada.com.

Peter


**
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.  The IT Department at Praxis Critical Systems can be contacted at 
[EMAIL PROTECTED]
This footnote also confirms that this email message has been swept by
MIMEsweeper for the presence of computer viruses.
www.mimesweeper.com
**



This e-mail has been scanned for all viruses by Star Internet. The
service is powered by MessageLabs. For more information on a proactive
anti-virus service working around the clock, around the globe, visit:
http://www.star.net.uk