Re: [SC-L] Tools: Evaluation Criteria
-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
[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
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
[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
-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] How can we stop the spreading insecure coding examplesattraining classes, etc.?
-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
-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
-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)
-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)
-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)
-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
-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
-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] SPI, Ounce Labs Target Poorly Written Code
-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
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