Re: [SC-L] Conditional Compile statements-- coding standards, and code review
When my organization develops code in C++, we generally ban use of #ifdef and #if defined(X), but we otherwise allow use of #if. The reason is that if you mis-spell the identifier that follows #ifdef, the compiler can't warn you. For example, if you write #ifdef FRDE ... #endif when you meant #ifdef FRED, the compiler doesn't warn you, and the conditional may not be interpreted as was intended. Best regards David Crocker, Escher Technologies Ltd. http://www.eschertech.com -Original Message- From: sc-l-boun...@securecoding.org [mailto:sc-l-boun...@securecoding.org] On Behalf Of Bennett, Jason Sent: 16 February 2009 09:46 To: 'sc-l@securecoding.org' Subject: Re: [SC-L] Conditional Compile statements-- coding standards,and code review Robert/Sean, It's a good question and one that I've never seen a really good answer to! Robert your option certain works but I feel that it somewhat prone to error if deployed on a large source base. So for example if a developer actually uses: #ifdef FRED # define MACRO(x) (x + 5) #endif ... then it's quite possible that this is missed by the review team and there is of course no guarantee that all code is reviewed manual. There is also the problem that there may be more than a single target release build for different variants i.e. it's not just a binary choice of release or debug versions. To make a more 'fool proof' mechanism I believe that it's better to have a more controlled use of which pre-processor directives are allowed for conditional compilation and ensure their use is consistent -- this is particular true of debug information which I believe causes the most problems. Following this approach would allow you to perform automatic searches for directives that are not on a defined white list. A word of warning this isn't as easy as it seems once you start getting statements of the following type -- this just re-enforces the problem of conditional compilation: #if defined c1 !(defined c2 || defined c3) ... #elif defined C4 ... #endif What would be really nice is to have an automatic tool that can check that for say build target A you can only have I, J and K defined but for not L and M -- using 3rd party code which is often designed to be ported to multiple targets sorting out what is actually used is not easy at all! Use should also looked at carefully to ensure that conditional compilation is only used where 'required'. So as an example do you really want all those call traces and information output used during development left in the code? In conclusion I believe that you should aim for as much automation as possible and also taking the problem out of the developer's hands. It's much easier to ensure that you've done something right once in your build system than expect every developer to do it right every time -- in my experience developers are happy to change what is in their 'local domain' but think about things a bit more carefully if they are making a change the can affect the entire development. Obviously these are just some ideas and I'm sure that there or other equally good solutions and as with all these things it does depend on what level of assurance you want otherwise you get the answer of don't allow conditional compilation! Consider the environment before printing this mail. Thales e-Security Limited is incorporated in England and Wales with company registration number 2518805. Its registered office is located at 2 Dashwood Lang Road, The Bourne Business Park, Addlestone, Nr. Weybridge, Surrey KT15 2NX. The information contained in this e-mail is confidential. It may also be privileged. It is only intended for the stated addressee(s) and access to it by any other person is unauthorised. If you are not an addressee or the intended addressee, you must not disclose, copy, circulate or in any other way use or rely on the information contained in this e-mail. Such unauthorised use may be unlawful. If you have received this e-mail in error please delete it (and all copies) from your system, please also inform us immediately on +44 (0)1844 201800 or email postmas...@thales-esecurity.com. Commercial matters detailed or referred to in this e-mail are subject to a written contract signed for and on behalf of Thales e-Security Limited. ___ 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. ___ ___ 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
[SC-L] 5th IEEE International Conference on Software Engineering and Formal Methods
Hi all, Seeing that formal methods have been used to prove aspects of system security, I thought that some members might be interested in the 5th IEEE SEFM conference, which will be held on 12-14 September in London. The conference program (http://www.iist.unu.edu/SEFM07/programme.html) includes papers on the following: Verifying the Mondex Case Study (verifying that a smart card money-exchange protocol is secure) Recovery from DoS Attacks in MIPv6 Verification of C Programs Using Automated Reasoning (my own paper - includes absence of buffer overflow) See http://www.iist.unu.edu/SEFM07 for more details. Regards, David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com ___ 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] Harvard vs. von Neumann
Crispin Cowen wrote: IMHO, all this hand wringing is for naught. To get systems that never fail requires total correctness. Turing tells us that total correctness is not decidable, so you simply never will get it completely, you will only get approximations at best. What Turing actually tells us is that it is possible to construct programs that may be correct but whose correctness is not decidable. This is a far cry from saying that it is not possible to build well-structured programs whose correctness _is_ decidable. Having humans write specifications and leaving programming to computers is similarly a lost cause. At a sufficiently high level, that is asking the computer to map NP to P, and that isn't going to happen. I don't understand what you are getting at here. If you are saying that humans can map NP to P, but that it is impossible in principle to have computers do the same thing, then that sounds like a religious argument to me. If you are saying that you can write a specification that is unsatisfiable (or whose satisfiability is undecidable) and that therefore cannot be implemented as code, then this applies equally to human programmers. Incidentally, I have heard of a few cases in which programming teams have wasted effort trying to implement sets of requirements which, when the requirements were formalised, turned out to be contradictory. At a less abstract level, you are just asking the human to code in a higher level language. This will help, but will not eliminate the problem that you just cannot have total correctness. The higher the level in which the human codes, the less mistakes there are to be made, assuming equal familiarity with the language etc. And you are just repeating the same fallacious proposition by saying you cannot have total correctness. Had you instead said you can never be sure that you have established that the requirements capture the users' needs, I would have had to agree with you. Programmable Turing machines are great, they do wonderful things, but total correctness for software simply isn't feasible. People need to understand that programs are vastly more complex than any other class of man made artifact ever, , and there fore can never achieve the reliability of, say, steam engines. Same old flawed proposition. And, in software, the behaviour of the components we build programs out of (i.e. machine instructions) are much more well-defined and reliable than the materials that steam engines are built out of. The complexity of software is beginning to approach living organisms. People at least understand that living things are not totally predictable or reliable, and s**t will happen, and so you cannot count on a critter or a plant to do exactly what you want. When computer complexity clearly exceeds organism complexity, perhaps people will come to recognize software for what it is; beyond definitive analyzability. Sure, if you develop a complex software system without a good design process that carefully refines requirements to specifications to design to code - and propagates changes in requirements down the chain too - then it may be impossible to meaningfully analyse that software. That is why my approach is to formalise requirements, write specifications that are proven to satisfy them, then refine the specification to code - automatically where possible, but with manual assistance where e.g. a data structure or an algorithm needs to be made more efficient. We can never solve this problem. At best we can make it better. We can never solve the problem of being certain that we have got the requirements right. I think that one implication for security is that there may be whole new classes of threats out there that nobody has thought of yet, and which we therefore can't refer to in the requirements. But we _can_ solve the problem of ensuring that software meets the stated requirements, as long as these are well-defined. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com ___ 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] Harvard vs. von Neumann
to outline, the additional complexity of automatic refinement of specifications to code can be mitigated, for example through the use of automated verification. As for compiler reliability: it's now 8 years since I had to workaround bugs in the C++ compilers that are the primary targets for our code generator. That is not to say that there are none, just that the probability that we will hit one is small enough that we don't have to worry about it outside the critical software markets. People who use low-volume specialist compilers for some embedded processors may have a different experience; but the reality for many (most?) of us is that finding a bug in our executable code that is caused by a faulty compiler is a rare event. More than forty years ago, we started the move from assembly language programming to a higher level of abstraction - high level programming languages. This raised productivity, and almost certainly reduced error rates. I think the time has come for a shift to an even higher level of abstraction. This posting has drifted a little more off-topic than I intended, however I do think it has a direct bearing on security. In order to get secure software, we need to: 1. Identify security as a requirement of the software right from the start; and 2. Use a development process that ensures that the finished software meets the requirements. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com ___ 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] FW: What's the next tech problem to be solvedin softwaresecurity?
IMO the real problem is that software developers are still focussed on programming, not on specification. We should leave programming to computers, instead of wasting money paying people to do it and hoping that the resulting system meets user requirements, including some semblance of security. If instead we pay people to perform the more skilled tasks of establishing requirements and specifying the systems to meet them, and use computers to generate programs that meet the specifications, then such things as freedom from buffer overflow come free of charge. By freedom here, I don't mean the sort of freedom that comes in safe languages such as Ada and Java - in which the buffer overflow raises an exception, probably requiring a restart of the subsystem - but rather, genuine immunity. Other security issues (like freedom from SQL injection and cross-site scripting attacks) may not always come free but are relatively easy to add to the specification, as long as people are aware of the need to do so. It amazes me that software development techniques have progressed so little in the last 50 years. In the 1950s we had assembler. This was followed in the 1960s by high level programming languages. Nearly 50 years later we have... slightly better high level programming languages. For example, one of the major languages in use today is C, which is more than 30 years old. The only significant advance since the invention of C (and Algol before it) is object-oriented programming - a welcome improvement, but far short of the paradigm shift that is desperately needed. Let's stop focussing on the minute detail of the steps that a computer needs to execute in order to solve a software problem, and turn our attention instead to describing what the program is supposed to achieve - including its resistance to hostile input. Until we do so, we will be doing little more than patching up outdated technology. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com -Original Message- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of SC-L Subscriber Dave Aronson Sent: 07 June 2007 13:53 To: SC-L@securecoding.org Subject: Re: [SC-L] FW: What's the next tech problem to be solvedin softwaresecurity? Michael S Hines [mailto:[EMAIL PROTECTED] writes: Product integration - why have an editor, separate source code analizer, separate 'lint' product, compiler, linker, object code analyzer, Fuzz testing tools, etc...apart from marketing and revenue stream - it doesn't help the developer any. It may. IME, all-in-one products usually integrate the pieces well. On the other claw, they don't tend to do most, if any, of the pieces well. On the third hand, integration doesn't have to mean they're no longer separate. They can play nicely together if they adhere to relevant standards for interoperability. Witness how you can develop a lot of software without leaving Emacs, or Eclipse. However, I don't think that's all that relevant to software security in particular, as opposed to software development in general. -Dave -- Dave Aronson Specialization is for insects. -Heinlein Work: http://www.davearonson.com/ Play: http://www.davearonson.net/ ___ 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. ___ ___ 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] Could I use Java or c#? [was: Re: re-writingcollege books]
Hi Attila, I wouldn't worry about not being able to see the assembly code while debugging. In practice, there is less need for debugging Java or C# code than with C++. For example, in C++, out-of-bounds array writes and incorrect type conversions can give rise to bugs that are hard to find, because the effect may be felt some time after the cause (e.g. the out-of-bounds array write corrupts some data). In Java or C#, the runtime system catches this sort of bug immediately. My company uses a code generator that can generate either C++ or Java. Although the production version of the products we ship are built using C++ code, for development and initial testing we generally use the Java code because bugs are caught much earlier. The performance improvement you can get from using C++ rather than Java or C# is significant only if the program uses really huge amounts of CPU time, in which case you might be able to make a case that the hardware cost saving outweighs the higher cost and time to develop in C++ rather than Java or C#. Otherwise, for application-level programming, Java or C# would generally be a more productive choice. Regards David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com -Original Message- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of SZALAY Attila Sent: 09 November 2006 11:20 To: [EMAIL PROTECTED] Cc: Secure Coding Subject: Re: [SC-L] Could I use Java or c#? [was: Re: re-writingcollege books] Hi All, On Thu, 2006-11-09 at 10:20 +1100, mikeiscool wrote: You can definately get appropriate information via the stack trace with java's exception handling. It's strange to see you say debugging is _eaiser_ in c, typically people find it far easier in a managed language :) People are different. :)) I personally want to know what happens and I don't believe anything waht I can't see. In C I can see the assembly code what (I hope) is a deterministic thing. An interpreter is to big (to me) to think about it as a deterministic thing. And yes, with ``normal'' bugs a managed language could give me more possibility to find the place of the problem. But I want to hope, that we don't commit normal bugs. :) And with mysterious bugs, when you cannot reproduce it in a test system, just the costumer some hundred miles away, I think that the stability of the compiled code (and the core file what may created) is give more more chance to find the right place. That's a java applet; please don't judge Java the language based on applets; they are a really bad representation. Serverside java will be very effective and useful; what sort of client are you writing? Is it a website or a desktop app? Even if it's a desktop app, perhaps look to azureus to see a good, well running app written in java for the desktop. There are others. This is a desktop application in a client-server model. I will look after azureus. ___ 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 ___ 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] re-writing college books [was: Re: A banner year for software bugs | Tech News on ZDNet]
Crispin, It is most certainly true that C++ can be appropriate in those cases. C++ programs can perform just as well as C programs, while also being much better structured. Of course, it will be necessary to avoid performing frequent allocation and deallocation of heap memory in the C++ program - but the same is true of C programs. Poorly-performing programs can be written in either language. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com -Original Message- From: Crispin Cowan [mailto:[EMAIL PROTECTED] Sent: 03 November 2006 04:46 To: David Crocker Cc: 'Secure Coding' Subject: Re: [SC-L] re-writing college books [was: Re: A banner year for software bugs | Tech News on ZDNet] David Crocker wrote: Unfortunately, there are at least two situations in which C++ is a more suitable alternative to Java and C#: - Where performance is critical. Run time of C# code (using the faster .NET 2.0 runtime) can be as much as double the run time of a C++ version of the same algorithm. Try telling a large company that it must double the size of its compute farms so you can switch to a better programming language! - In hard real-time applications where garbage collection pauses cannot be tolerated. Except that in both of those cases, C++ is not appropriate either. That is a case for C. Crispin -- Crispin Cowan, Ph.D. http://crispincowan.com/~crispin/ Director of Software Engineering, Novell http://novell.com Hack: adroit engineering solution to an unanticipated problem Hacker: one who is adroit at pounding round pegs into square holes ___ 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] Proving the security properties of transaction protocols - 10 years on
Members of this list might be interested in an article in this month's IEEE Computer Journal about the use of automatic and semi-automatic theorem proving to prove the security of a transaction protocol. The article - which is called First Steps in the Verified Software Grand Challenge - concerns the transaction protocol that was used by the Mondex electronic purse, which was developed and formally verified (by hand) around ten years ago. Several teams have recently attempted to apply modern tools to the problem. In the process, several of the teams working on the project found that the original hand-developed proof was incomplete, but could be patched. More details can be found at http://csdl2.computer.org/persagen/DLAbsToc.jsp?resourcePath=/dl/mags/co/toc=co mp/mags/co/2006/10/rxtoc.xmlDOI=10.1109/MC.2006.340#abstract . Non-subscribers can download the article for $19. My own company provided one of the teams working on this problem, and we found it is quite a challenge to prove the protocol correct by fully-automatic means. Proofs that software is free from buffer overflows for all possible inputs are almost trivial by comparison. Regards David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com ___ 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] re-writing college books [was: Re: A banner year for software bugs | Tech News on ZDNet]
Crispin Cowan wrote: For me, the enemy in the room is C++. It gives you the safety of C with the performance of SmallTalk. There is no excuse at all to be writing anything in C++ yet vastly too many applications are written in C++ anyway. Instead of trying to coax developers to switch from C++ to something weird like SML, lets encourage them to switch to Java or C#, which are closer to their experience. Unfortunately, there are at least two situations in which C++ is a more suitable alternative to Java and C#: - Where performance is critical. Run time of C# code (using the faster .NET 2.0 runtime) can be as much as double the run time of a C++ version of the same algorithm. Try telling a large company that it must double the size of its compute farms so you can switch to a better programming language! - In hard real-time applications where garbage collection pauses cannot be tolerated. However, I suspect that most security-critical programs do not fall into either of these categories, so C# or Java would indeed be a better choice than C++ for those programs. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com ___ 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 codingexamplesattraining classes, etc.?
Also, exceptions (unlike gotos) cannot be used to jump backward, thereby creating hidden loops. Used correctly, exceptions eliminate large amounts of code that would otherwise be required to handle unexpected failures at every level in a function call stack and propagate such failures upwards by way of return codes etc. to a point at which some remedial action can be taken. Exceptions can certainly be misused, but they are much better than the alternatives in many situations. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com -Original Message- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of der Mouse Sent: 31 August 2006 22:45 To: SC-L@securecoding.org Subject: Re: [SC-L] How can we stop the spreading insecure codingexamplesattraining classes, etc.? ever heard of exceptions? They're basically goto plus limited state. Spaghetti lives! Not at all. Exceptions are not like gotos; in particular, an exception cannot be used to jump *into* a construct. The major problems with gotos are that they can be used to do branches that are downward or sideways in the code parse tree (versus structured constructs, which do such branches upward only). Exceptions are upward-only branches, and as a result don't have most of the problems gotos do. /~\ The ASCII der Mouse \ / Ribbon Campaign X Against HTML [EMAIL PROTECTED] / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B ___ 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 ___ 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] Java keystore password storage
I'm by no means an expert in the field of security and Java, but I believe that the usual technique is to encode the password that the user types using a 1-way hashing algorithm, then store (and hide/protect) the encoded version and use that as the password. If an attacker manages to read the password hash, he still has to construct a password that will encode to the same value. There are a number of hashing algorithms available. SHA1 used to be considered fairly good for this sort of thing, but I understand it has been broken recently. This technique does make it impossible to recover the password; if the password is lost, it has to be reset to a new one. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com -Original Message- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of john bart Sent: 25 April 2005 08:56 To: SC-L@securecoding.org Subject: [SC-L] Java keystore password storage Hello to all the list. I need some advice on where to store the keystore's password. Right now, i have something like this in my code: keystore = KeyStore.getInstance(JKS); keystore.load(new FileInputStream(keystore.jks),PASSWORD); the question is, where do i store the password string? all of the possibilities that i thought about are not good enough: 1) storing it in the code - obviously not. 2) storing it in a seperate config file is also not secure. 3) entering the password at runtime is not an option. 4) encrypting the password - famous chicken and egg problem (storing the encryption key) Any ideas?
RE: [SC-L] Theoretical question about vulnerabilities
Crispin wrote: Here's an example of a case it cannot prove: if X then Y - initial value endif ... if X then Z - Y + 1 endif The above code is correct in that Y's value is taken only when it has been initialized. But to prove the code correct, an analyzer would have to be flow sensitive, which is hard to do. The whole science of program proving is based on exactly this sort of flow analysis. The analyser will postulate that Y is initialised at the assignment to Z, given the deduced program state at that point. This is called a verification condition or proof obligation. It can then attempt to prove the hypothesis; for this example, the proof is trivial. I guess it would have been more difficult 20 years ago when Hermes was written. The alternative solution to the problem of uninitialised variables is for the language or static checker to enforce Java's definite initialisation rule or something similar. This at least guarantees predictable behaviour. An issue arises when a tool like Perfect Developer is generating Java code, because even though PD can prove that Y is initialised before use in the above example, the generated Java code would be violate the definite initialisation rule. We have to generate dummy initialisations in such cases. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Theoretical question about vulnerabilities
Crispin Cowan wrote: Precisely because statically proven array bounds checking is Turing Hard, that is not how such languages work. Rather, languages that guarantee array bounds insert dynamic checks on every array reference, and then use static checking to remove all of the dynamic checks that can be proven to be unnecessary. For instance, it is often the case that a tight inner loop has hard-coded static bounds, and so a static checker can prove that the dynamic checks can be removed from the inner loop, hoisting them to the outer loop and saving a large proportion of the execution cost of dynamic array checks. 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. What exactly is your program going to do when it detects an array bound violation at run-time? You can program it to take some complicated recovery action; but how are you going to test that? You can abort the program (and restart it if it is a service); but then all you have done is to turn a potential security vulnerability into a denial of service vulnerability. So the better approach is to design the program so that there can be no buffer overflows; and then verify through proof (backed up by testing) that you have achieved that goal. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Theoretical question about vulnerabilities
Pascal Meunier wrote: Do you think it is possible to enumerate all the ways all vulnerabilities can be created? Is the set of all possible exploitable programming mistakes bounded? No. It's not so much a programming problem, more a specification problem. Tools now exist that make it possible to develop single-threaded programs that are mathematically proven to meet their specifications. The problem is knowing what should be included in the specifications. Let me give you some examples: 1. Buffer overflow. Even if nobody realised that buffer overflows could be used to bypass security, it is an implied specification of any program that no array should ever be accessed via an out-of-bounds index. All the tools out there for proving software correctness take this as a given. So buffer 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. You don't even need to write a specification for the software in this case - the implied specification is enough. 2. SQL injection. If the required behaviour of the application is correctly specified, and the behaviour of the SQL server involved is also correctly specified (or at least the correct constraints are specified for SQL query commands), then it will be impossible to prove the software is correct if it has any SQL injection vulnerabilities. So again, this would be picked up by the proof process, even if nobody knew that SQL injection can be used to breach security. 3. Cross-site scripting. This is a particular form of HTML injection and would be caught by the proof process in a similar way to SQL injection, provided that the specification included a notion of the generated HTML being well-formed. If that was missing from the specification, then HTML injection would not be caught. 4. Tricks to make the browser display an address in the address bar that is not the address of the current HTML page. To catch these, you would need to include in the specification, the address bar shall always show the address of the current page. This is easy to state once you know it is a requirement; but until last year it would probably not have been an obvious requirement. In summary: If you can state what you mean by secure in terms of what must happen and what must not happen, then by using precise specifications and automatic proof, you can achieve complete security for all possible inputs - until the definition of secure needs to be expanded. This should have consequences for source code vulnerability analysis software. It should make it impossible to write software that detects all of the mistakes themselves. Is it enough to look for violations of some invariants (rules) without knowing how they happened? The problem is that while you can enumerate the set of invariants that you currently know are important, you don't know how the set may need to be expanded in the future. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Programming languages used for security
Peter Amey wrote: 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. You seem to be assuming that there is only one appropriate solution to the problem and the system cannot be trusted to find it. In reality, there are often many appropriate solutions and it matters little which one is chosen. In the example you give, either of the first two solutions would likely be acceptable, and I think it would be perverse for a code generator to choose the third (i.e. an external sort on internally-stored data). But I'm not proposing that you should have to accept whatever the code generator comes up with: if you don't like the result, the language should provide a way of expressing (in outline at least) how you want the ordered property to be achieved. 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). You seem to be missing the point that B allows you to specify one abstract machine that talks about a sequence being ordered and then refine it to another that talks about sorting a list. B does indeed allow you to write code-like executable specifications; but it also allows you to write higher-level abstract specifications. I agree that there may be a temptation for developers to just write the executable version. This is why in PD we have a semantic distinction between specification and implementation, and you can't write an implementation without having a specification to attach it to. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Programming languages used for security
Crispin Cowan wrote: The above is the art of programming language design. Programs written in high-level languages are *precisely* specifications that result in the system generating the program, thereby saving time and eliminating coding error. You will find exactly those arguments in the preface to the KR C book. Whilst I agree that the distinction between specification and programming languages is not completely clear cut, there is nevertheless a fundamental difference between specification and programming. In a programming language, you tell the computer what you want it to do, normally by way of sequential statements and loops. You do not tell the computer what you are trying to achieve. Indeed, current programming languages provide hardly any means of expressing what you want to achieve; typically, the only concession they make in this direction is an assert statement, which lacks the expressivity needed (e.g. you can't easily use an assert statement to say that an array contains the same objects that it did on entry to the current function, but they are now arranged in ascending order). In a specification language, you tell the computer what you are trying to achieve, not how to achieve it. This is typically done by expressing the desired relationship between the input state and the output state. The state itself is normally modelled at a higher level of abstraction than in programming (e.g. you wouldn't refer to a hash table, because that is implementation detail; you would refer to a set or mapping instead). The distinction becomes somewhat blurred when you assemble a program from library classes, because you are relying on those classes to represent some data without worrying about how they represent it, and calling their methods to achieve some state changes without worrying about the steps they go through to achieve it. Unfortunately, in the absence of precise specifications for those classes, it sometimes happens that what is achieved by calling a method is not quite what you wanted; or you may sometimes fail to meet the preconditions of the method, resulting in a crash or exception. My belief is that a software development language should be capable of expressing both specification and programming. Most of the time, its users will write the specifications and let a tool refine them to a program. Where a higher degree of optimization is needed, the software developer can manually refine parts of the specification to a program. It is not difficult to extend such a language to be capable of expressing expected behaviour as well. This paves the way for tools that attempt to prove that the specification exhibits the expected behaviour (and that any manual refinements are correct implementations of the corresponding specification). In case anyone is wondering what this has to do with security, expected behaviour includes things like array indices are always in bounds (i.e. no buffer overflows no matter what input is provided), and the browser address bar always shows the full URL of the current page. David Crocker Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Education and security -- another perspective (was ACM Queue - Content)
Crispin Cowan wrote: In programming language terms, Ada is grossly primitive. Its object orientation mechanisms are crude at best. A *great* deal of progress in language technology has been made since Ada was developed. For just about any kind of concept or safety feature, students and developers would be better served to consider Java, C#, or ML instead of Ada. I'm no fan of Ada (I find the language cumbersome and verbose, and it makes a pigs ear of trying to be fully O-O) - but I have to defend Peter Amey in this case. There is a tendency to regard every programming problem as an O-O problem. Sometime last year I read a thread on some programming newsgroup in which contributors argued about the correct way to write a truly O-O Hello world program. All the solutions provided were cumbersome compared to the traditional printf(Hello, world!) solution. The point is, printing Hello, world! is not an O-O problem! Although for most commercial application packages an O-O architecture is the best choice at present, for many embedded systems there is absolutely no reason to use polymorphism with dynamic binding - which are the main language features that distinguish the O-O approach from earlier methods. Ada has always provided the other benefits associated with O-O languages (encapsulation, information hiding, genericity). In safety-critical work there is a good case for regarding dynamic binding as dangerous unless you formally prove it to be safe using rigorous methods. And much as I dislike Ada, I have to admit that if you don't intend to use dynamic binding and don't need the low-level features of C, Ada is one of the safest languages around. BTW there is probably more embedded programming being done using C rather than anything more modern. Java is ruled out for most real-time embedded applications because garbage collection pauses cannot be tolerated. [My own preference for embedded work is MISRA C extended with a few features from C++ - but it needs good tool support in order to ensure that all the worst unsafe features of C/C++ are avoided.] Java, C#, and ML are strictly better than Pascal and Ada for almost everything. But they did not spring out of the earth, they were built on the progress of previous languages. Java in particular contains no novel features at all, but rather shows good taste in the features it borrows from others. What made Java interesting was the accident of history that caused it to become the first strongly typed polymorphic programming language to become widely popular. I disagree with your almost everything because there is a huge amount of embedded software developed for which Java is unsuitable. Java is certainly a big improvement on C++ for anyone not needing the low-level control that C++ can give, but unfortunately the designers of Java still borrowed too much from C/C++. In particular, mixing automatic type conversion with overloading is a _very_ bad idea. Indeed, for safety-critical work, almost any sort of automatic type conversion is a very bad idea. The depressing thing about Java is that it contains almost nothing new. In contrast, the designers of Eiffel added language features designed to make producing correct programs easier. You *can* teach object orientation with Simula 67 or SmallTalk, if you really want to. But teaching object orientation with Java is a lot more approachable in the contemporary context. I certainly wouldn't advocate teaching Simula or Smalltalk. But focussing solely on Java and O-O programming does not set students up well for embedded software development. David Crocker Consultancy, contracting and tools for dependable software development www.eschertech.com
RE: [SC-L] Programming languages used for security
I think there are two other questions that should be asked before trying to answer this: 1. Is it appropriate to look for a single general purpose programming language? Consider the following application areas: a) Application packages b) Operating systems, device drivers, network protocol stacks etc. c) Real-time embedded software The features you need for these applications are not the same. For example, garbage collection is very helpful for (a) but is not acceptable in (b) and (c). For (b) you may need to use some low-level tricks which you will not need for (a) and probably not for (c). 2. Do we need programming languages at all? Why not write precise high-level specifications and have the system generate the program, thereby saving time and eliminating coding error? [This is not yet feasible for operating systems, but it is feasible for many applications, including many classes of embedded applications]. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com Kevin Wall wrote: If a GENERAL PURPOSE programming language were designed by scratch by someone who was both a security expert and programming language expert, what would this language (and it's environment) look like? More specifically, + What set of features MUST such a language support (e.g., strong static typing, etc.)? + Perhaps just as importantly, what set of features should the language omit (e.g., pointer arithmetic, etc.)? + What functionality should the accompanying libraries support (e.g., encryption, access control, etc.)? + What would be the optimal paradigm (from a theoretical, rather than pragmatic perspective) that such a language would fit into (e.g., object-oriented, functional, imperative, logic programming, etc.)? [Note: I mention theoretical, rather than pragmatic so that such a language would be unduly influenced by the fact that presently developers familiar with OO and imperative styles vastly out number all the others, with functional coming up a distant 3rd.] + (Related to the previous item) Would such a language be compiled or interpreted or something in between. Also, if anyone chooses to discuss these issues, let's leave things like portability and performance out of the equation UNLESS you feel these things directly have an impact on secure coding. I think that we can all agree that we'd desire a portable and fast-executing language (although perhaps a slow-executing language would be more secure in that it might slow down the propagation of malware ;-).
RE: [SC-L] opinion, ACM Queue: Buffer Overrun Madness
ljknews wrote: And there are ways of using Assembly Language to avoid pitfalls that it provides. There are ways of using horse-drawn carriages to avoid the major reason (think street cleaning) why the automobile was embraced in urban areas during the early part of the 20th century. What there are _not_ are reasons for new development to cling to languages which make flawed constructs easy for the individual programmer to misuse. There is often one very good reason for clinging to such languages: because there is no other suitable language available. As has already been pointed out, there is usually very little alternative to C/C++ when it comes to kernel mode code. I would love to see a safer alternative to C/C++ for writing operating system kernels, device drivers and real-time embedded applications (yes, I know Ada can be used for the latter, buts its package structure and associated with-ing problem can be a real pain in large systems). The newer programming languages such as Java, C# and Eiffel are all designed for applications and make heavy use of garbage collection (which is a boon to application writers, but a no-no for kernel code and many embedded apps). What I don't understand is why the language standardisation committees don't remove some of the unsafe dross when they bring out new language revisions. A classic example is the failure to define the type of a string literal in C as const char*. Just imagine if we had a new version of C++ with all the unsafe stuff removed. Backwards compatibility would not be a problem in practice, because the compiler suppliers would provide switches to make their new compilers accept obsolete constructs. As for non-real-time application-level code, I gave up writing them in C++ by hand long ago. [Actually I prefer to write specifications, verify them, and let a code generator produce correct C++ from them; but that is another story.] David Crocker Consultancy contracting for dependable software development www.eschertech.com
RE: [SC-L] opinion, ACM Queue: Buffer Overrun Madness
Sloppy coding can be done in any language, but C and C++ have 3 features that aggravate the problem: 1. The array=pointer idiom. Given a parameter which is an array, you can't ask at run-time how big the array is - you have to do extra work and pass the size in an additional parameter (whereas most languages pass the size of an array automatically as part of the array). So doing buffer overflow checks requires more than just inserting the check - you have to make sure that an extra array size parameter is passed all the way down the call stack. [C and C++ cannot be considered strongly typed, in part because of the lack of distinction between pointers and arrays]. 2. By permitting pointer arithmetic, C and C++ encourage you to pass a pointer into the middle of a buffer, rather than passing the [start of the] buffer and an index into it, which makes bounds checking even more tedious to do (you have to pass a pointer to one-past-the-end-of-the-array as well, and even then this is less useful than having an index and a limit). 3. The lack of automatic bounds checking. Of course, run-time bounds checking is by no means a complete solution, but it does at least prevent a buffer overflow being used as a security attack, turning it into a denial-of-service attack instead. Apart from the obvious solution of choosing another language, there are at least two ways to avoid these problems in C++: 1. Ban arrays (to quote Marshall Cline's C++ FAQ Lite, arrays are evil!). Use classes from the STL, or another template library instead. Arrays should be used only in the template library, where their use can be controlled. 2. If you really must have naked arrays, ban the use of indexing and arithmetic on naked pointers to arrays (i.e. if p is a pointer, then p[x], p+x, p-x, ++p and --p are all banned). Instead, refer to arrays using instances of a template class ArrayX that encapsulates both the pointer (an X*) and the limit (an unsigned int). Such an object needs only 2 words of storage (compared to 1 word for a naked pointer), so it can assigned and passed by value. You can provide an operator to return the value of the limit, and an indexing operator (with optional bounds checking). If you really must, you can even implement pointer arithmetic operators for the class which update the limit at the same time as updating the pointer. David Crocker Consultancy contracting for dependable software development www.eschertech.com