David Crocker wrote: 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. For years, I have been trying to get formal specification advocates to explain the difference between high level programming languages and specification languages. From my point of view, formal specifications can be divided into two categories: * Those that can be mechanically translated into code, otherwise known as programs * Those that cannot be mechanically translated, otherwise known as documentation :) 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 ... 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). I agree with the other posters: the above could describe a formal specification, but could also describe a declarative programming language. 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. The assert() statements that David Crocker mentioned are an incomplete form of this; incomplete because the do not *completely* verify the program's behavior to be correct (because they are haphazardly placed by hand). So there's another midpoint in the spectrum: a formal spec that can only verify correctness but is complete, effectively is a program for non-deterministic machines (cf: NP completeness theory). A spec that is incomplete (does not specify all outputs) is more of an approximation. All of which begs the question: are these formal specs that are somehow not programs any easier to verify than actual programs? Probably somewhat easier (they are necessarily simpler) but some would argue, not enough simpler to be worth the bother. E.g. suppose 100,000 lines of code reduces to 10,000 lines of formal specification in some logical notation. A hard problem, but solvable, is a mechanical proof that the 10,000 line spec and the 100,000 lines of code actually conform. An unsolved problem is does the 10,000 line spec mean what the human *thinks* it means? Crispin -- Crispin Cowan, Ph.D. http://immunix.com/~crispin/ CTO, Immunix http://immunix.com
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 ? -- Larry Kilgallen
En un mensaje anterior, Blue Boar escribió: Fernando Schapachnik wrote: I smell a discusion going nowhere. What is the point of teaching a languague? Teach them to program in a paradigm (better, in all of them, and give them the tools to make educated choices about which is better for each context), and choose any language as an *example* of the paradigm. Ah... but beyond design problems, aren't most security problems language-specific abuses and bugs? I'm thinking things like I didn't realize it would let me mix signed and unsigned... I didn't realize it would let me right off the end of the buffer... I didn't realize I had to escape or filter certain characters Same thing happens with concurrency. You need to tell them about shared variables, mutexes, locking, atomicity, protected sections, etc. When they are going to undertake a real project in a specific language they need to know how these are implemented there. I expect them to be able to learn that from the multiple available resources, once the foundations are learn. Now s/concurrency/security/. Imagine next year, when language NEW appears and some people from this list are required to work in it. I suspect most of them would probably apply their existing knowledge and some searching around to understand the new thread model, and act acordindgly. Is the same scenario for students. Regards. Fernando.
-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
der Mouse is correct. I recall a product from the early 80s called The Last One. There was an advertisement for the product on Prof Doug Comer's door when I was a grad student at Purdue... the claim was that this product made designing applications so simple that you'd never have to program again. I'm sure you're all familiar with this product, since it made your lives obsolete. And it would have succeeded, if the Mafia hadn't hushed it up along with Jimmy Hoffa's death. One of the buzzwords du jour is model driven architectures (MDA); OMG has a working group on it (http://www.omg.org/mda/). It's just the latest iteration in what der Mouse called very-high-level languages. It has the same promises as we've heard by countless iterations of abstractions faster development, fewer bugs, less need for programmers, etc. I'm skeptical. Getting back to the point at hand, though, I think this discussion is confusing two related topics: languages that help you build code that doesn't have security implementation bugs, and languages that help you build code that doesn't have security design flaws. [Gary McGraw pushes the difference between bugs flaws, and I agree.] Example: Java helps you avoid a lot of the common *bugs* (by doing some things automatically like bounds checking, and providing libraries to do other things correctly like cryptography], but can't do much to help you avoid misdesigning the software. I think we're getting pretty good (relatively speaking) at building languages for bug-free code, but much less so for flaw-free code. To me, that's the *real* potential of the very-high-level languages... if things can be brought up to a point where the design becomes more obvious (since the implementation becomes somewhat automated), then there's a better chance of finding the security design problems. On the other hand, the problem with abstracting too much is that the security problems can get swept under the rug. To get REALLY back to the point, I'd like to comment on Fabien's comment that In my opinion, it's the most important things for a languages, something to easily validate user input or to encrypt password are a must have. Fabien is right, but increasingly that's only half the problem. There also needs to be something in the libraries for the language to securely store data that can't be one-way hashed, as are (inbound) passwords. For example, if I need to store the password my application needs to authenticate to a database, or other critical data, it would be nice to have that built into the language libraries, instead of having to build it myself. It would certainly reduce the number of programmers who build such storage mechanisms themselves, and insecurely at that. My $0.02 or equivalent in local currency. --Jeremy -Original Message- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] Behalf Of der Mouse Sent: Friday, July 09, 2004 4:18 PM To: [EMAIL PROTECTED] Subject: Re: [SC-L] Programming languages used for security 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? Then the high-level specification _is_ the programming language, albeit a relatively unusual one, with the thing you call the system being what is normally called the language's compiler. Such very-high-level languages are a perennial idea. As you point out, they aren't always appropriate, but when they are they can be helpful. But they don't eliminate programming, any more than COBOL (which was supposed to make it possible to write programs in plain English and thereby eliminate programming as a skill) did. And they won't eliminate coding error. They'll eliminate certain classes of coding error, just as assembly does as compared to machine language, or as C or Pascal does as compared to assembly language - but coding errors will still occur, just as they do in assembly or C. They'll just be errors at or above the level at which the code is written. Or, of course, they'll due to be bugs in the compiler. /~\ 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
So in all the discussions, I think I'm seeing several main themes: -Some holes are design or logic errors (possible in any language) -Some holes are failures to code safely in a given language (language specific; possibly addressable by switching to a safer language) -Some holes are harder to implement in a safer language (library, class...) And I'm sure I've missed a few important ones. Point is, I think in a number of cases, we mix these concepts in the same discussion, and I'm not sure that's always useful. If we're talking about logic problems... you can always get your boolean conditional jump backwards, doesn't matter what language you use. If we're talking about one flavor of secure coding (coding safely in a dangerous language), then that discussion/class neccessarily needs to be very language specific. This problem also extends to things like system APIs, libraries, and so on. I don't know that any significant project can get away from that, regardless of the main language used. If we're talking about secure coding in terms of picking a language that should help us not make whole classes of mistakes, then that's a different discussion. BB
To get REALLY back to the point, I'd like to comment on Fabien's comment that In my opinion, it's the most important things for a languages, something to easily validate user input or to encrypt password are a must have. Fabien is right, but increasingly that's only half the problem. There also needs to be something in the libraries for the language to securely store data that can't be one-way hashed, as are (inbound) passwords. For example, if I need to store the password my application needs to authenticate to a database, or other critical data, it would be nice to have that built into the language libraries, instead of having to build it myself. It would certainly reduce the number of programmers who build such storage mechanisms themselves, and insecurely at that. I'm really glad to see this point raised. I really have very little interest in the which language debate, because most of the software I see depends so heavily on *libraries*. The real genius of Java in my opinion is that they slapped a standard API on top of just about everything (graphics, databases, networking, phone systems, microplatforms, crypto, and much more). Some other languages have also been successful here in a somewhat less standardized way. But just slapping an API on something is not the same as making it easy to use securely. Java's JCE is a perfect case in point - they encrypted the API itself! ;-) To me, it's far more important that the libraries are easy to use securely than language syntax stuff. So how do we encourage library writers to write APIs that are easy to use securely? I'd like to see libraries that force the developer to explicitly do something special if they want to get around the default secure way of doing things. It's not enough to just include a bunch of security features into the libraries. I've seen far too many libraries that expose a very powerful API and make it too easy for a developer to make security mistakes. Does anyone have pointers to articles on designing API's so that they are easy to use securely? --Jeff Jeff Williams Aspect Security http://www.aspectsecurity.com