Re: [SC-L] Tools: Evaluation Criteria

2007-05-24 Thread 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

2007-05-23 Thread 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

2007-05-22 Thread 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

2007-01-02 Thread 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] Compilers

2007-01-02 Thread 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] Why Shouldn't I use C++?

2006-11-01 Thread 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.?

2006-08-31 Thread 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] Theoretical question about vulnerabilities

2005-04-13 Thread 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] Programming languages used for security

2004-07-12 Thread 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)

2004-07-09 Thread 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)

2004-07-08 Thread 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] Education and security -- another perspective (was ACM Queue - Content)

2004-07-08 Thread 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] ACM Queue article and security education

2004-07-02 Thread 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

2004-07-02 Thread 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

2004-07-01 Thread 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

2004-06-29 Thread 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

2004-06-09 Thread 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