Slashdot Mirror

And the only correct documentation is the code itself. Anything else is a opinion and should be viewed accordingly.

Of course the code itself only tells you what the code does, not what the code is supposed to do, nor why it is doing it. Note that the difference can be rather crucial in maintenance and bug fixing.

I don't know how many times over my 30 year career that I've read documentation and started work only to find out later that it hadn't been updated. The first standard in your documentation rules should be that all relevant documentation is created and updated before code goes into production. No excuses.

Which is why it's always nice to have documentation that can be tested against the code. Now the "why" part of documentation is rather hard to verufy against code, but the "what it is supposed to do" should be able to be automatically verified if it is sensibly written: for instance in Eiffel requires and ensures clauses, or in JML, or splint, or SPARK; which allow for varying levels of static checking, runtime assertions, and automatic unit test generation (depending on what you are using) to ensure that if code and documentation falls out of sync an error should be immediately flagged.

Hmm...

I thought the idea of "Secure languages" was being able to PROVE there were no security bugs on your software because it was correct (if you're willing to pay the price in development time, of course).

At least at first glance, SPARK's claim to 'high security' is on that same line: http://www.praxis-his.com/sparkada/intro.asp

From that point of view, one of the big appeals of Java and other VM languages was precisely that software could potentially be 'provably secure' up to some level (typically with subsets / extensions of the language providing more or less comfortable definitions of 'secure'). Strong static typing and no pointer arithmetic means a duck will not turn into a dog on you - so you can trust strong pre/post conditions to a greater extent.

Provability of correctness is an objective statement. That doesn't make software magically secure - but it means it is *possible*, with enough work, to *prove* that *the part of the software you wrote* implements the security of your design *correctly*. You're still vulnerable to design gaps, and security bugs in any reused libraries / runtime - but that narrow proof of security still eliminates whole categories of end-of-the-world-scenarios from your list.

Making security bugs 'easier to avoid' - like other 'bug preventing language features' - is a much more subjective claim (how do you define a 'security bug' for such a claim anyway?), and is what can backfire into non-sensical assumptions. They're typically a net gain int he hands of an informed developer, but naive programmers can be misled that because a very specific type of security bug X 'cannot happen' in the language, 'security' is taken care of.

Take a look at http://www.praxis-his.com/sparkada/ and "correctness by construction" design process. Something good came out of DoD ;)

Don't know why is this news. Ada is used in High Integrity System
for long long time.

http://www.praxis-his.com/sparkada/index.asp/

Cheers
BT

Don't think it is just funny... it might be truth. BA is a customer of SPARKAda (as listed in http://www.praxis-his.com/sparkada/customers.asp). I expect the software run by the aircraft is proved to be correct to its specification using that, which is a variant of Ada.

Home builders have architectural plans. Machinist have blueprints. Electronic equipment builders have schematics. Software specifications are uniformly deplorable.

Well at least Ada still is: http://www.praxis-his.com/sparkada and very successfull as well.

And Ada isn't dead, it just got another rejuvenation in the form of Ada 2005: http://www.adaic.com/standards/ada05.html.

So the use of past tense was not appropiate.

Martin

In my opinion, something such as a fly by wire system that people's lives depend on need to be proved to be correct. It can be done, and can even be somewhat automated. There's at least one high-integrity Ada development system with an automated proof checker. One such system is SPARKAda. There's also the Motor Industry Software Reliability Association's set of C programming guidelines, plus C compilers that can auto-check for compliance with many of those rules.

Wrong, wrong wrong. A kid fresh out of college IS NOT equal to somebody who has been working for 20 years. NOT EQUAL. I'm sorry if that hurts somebody's feelings, but that's life. To assume that "all developers are created equal" is completely and utterly wrong. I don't know how better to explain it; this is kind of a common sense thing.

The fastest way through the project is to do it right Huh? No it isn't. The fastest is often to slap together something crude that works. It's all about ROI. If I hire a developer to write a quick and dirty DB interface that only I use, and he takes 6 weeks to do it, because he's sharing and holding hands, and documenting, and using source control, etc., then that developer will be fired.

Maybe he means this:)

Hello,

I am sorry to tell you: If you need to write ultra-stable software then you need a propper "High Integrity Toolchain". My suggestions:

http://www.praxis-his.com/

and

https://www.adacore.com/gnatpro_high_integrity.php

There are no two ways around it. Speed is no issue - Ada is just as fast as C++. The libraries are more tricky. But then: have you ask yourself: "Are those libraries ultra-stable?"

If they are not then your efforts are furtile. And most likely they are not. Most C/C++ library vendors don't have ultra-stable in mind when they create there libraries. That's unlike for example Ada library vendors which allways take stability into account.

Others said it before, suggestion other languages and I repeat it: C++ is a no go for ultra stable.

Martin

You have to realize that, for the vast majority of programmers, that the structure is necessary. Those programmers working in dynamically-typed languages fail; they produce spaghetti. Sure, you *can* maintain structure in a dynamically typed language such as Smalltalk or Ruby. But programming is a constant struggle to keep the code from descending into chaos.

What gets me though, is that people will make these sorts of comments all the time, and yet when you suggest that it's quite easy to take the same idea just a little further it all of a sudden becomes completely unpalatable and "too much work". Never mind that that's the same argument the dynamic type people use against static types. Never mind that for the extra work of contracts or specifying a little more than just type signatures you can get static checking gains and improvements in maintainability on par with what you get from using static types over dynamic types.

If you really believe that specifying static types really does help reduce bugs and improve maintainability (and it certainly can) then check out the options for doing a little better again.

Jedidiah.

Can do: http://www.praxis-his.com/pdfs/svandxp.pdf

Then their ability to produce bug-free code depends, as usual, on control factors, not on real-world engineering.

In as much as a civil engineer depends on control factors via refusing customers who demand that the building have 6 stories not 4 just one month before construction is due to finish, yes. Real world engineering makes certain demands of the client. Someone who wants to build a treehouse for their kids doesn't consult an architect and a civil engineer, and civil engineers don't take contracts from people who refuse to set out some limits on what they want built, and what they expect of it.

Praxis uses solid engineering. Their "Correct by Construction" approach is solidly grounded in axiomatic mathematics and uses similar sorts of formal calculations and logical and mathematical proofs as you might expect to see from civil, electrical, aerospace, or ny other kind of engineers. Take the time to read sample chapters from the SPARK book to get an idea of exactly what they are doing. There is very definitely quite solid engineering going on.

Yes, small teams help, but I think it really is worth taking a look at the tools and methods that Praxis uses because there are some remarkably good ideas in there. Take a look at SPARK Ada - the Wikipedia article has some basic examples, and Praxis provides sample chapters of a book on SPARK for download. Seriously, take a little time out of your day, sit down, and read a little about how they do what they do. There really are good ideas that go well beyond just "small teams" if you want to deliver correctly functioning code.

Jedidiah.

Praxis uses SPARK Ada, which is a subset of the Ada programming language and annotations that provide for extended static checking, and theorem proving. You can find more about SPARK at the Praxis website, or the Wikipedia article isn't too bad. It's a very nice language, and has fantastic tool support.

If you find that interesting, but Ada isn't to your taste, you can try JML for Java which provides similar (but lacking quite the same robustness and tool support) annotations. JML lets you automatically generate JUnit tests based on your annotations, and with ESC/Java2 allows for extended static checking.

If, as you appear, you are more of a fan of functional languages then I'd suggest you check out Extended ML and HasCASL which provide similar sorts of formal specification capabilities for ML and Haskell. Tool support for these is still a little limited, but they are both quite powerful and provide very expressive specification syntax.

Jedidiah.

Uh, did you RTFA(s)? They are using automatic verification - take a look at their SPARK Ada toolkit.

While C++ is more strongly typed than C, C++ is not type safe. Type safety means that the language ensures that no operation will ever be applied to a variable of the wrong type. However, C++ supports the ability to access arbitrary memory locations, allows type casting, and automatically converts types in many instances. Java is more strongly typed than C++, as it doesn't allow access to arbitrary memory locations, but it also supports casting and automatic conversions, and so is not type safe. If you want type safety, try a language like Ocaml or SPARK Ada.

What parts do what should be clear from the names of function calls and variables, but whenever a function becomes longer than something really short, yes, it needs comments describing what happens where. If a function does something complicated, it's worth starting with a comment describing pre- and post conditions.

Now there is an excellent idea! It doesn't take a lot of effort - you should be able to come up with some basic constraints on inputs and outputs if you have any decent idea of what the function does - but it is very helpful documentation to anyone else, particularly for people who have to call the function (as it clerly delimits exactly what they need to provide, and exactly what they can expect to get back). Better yet, as long as you use a system that supports it you can get a whole lot of benefits in terms of automated checking and debugging of your code, saving you a lot of effort later.

Eiffel and D support pre and post conditions directly in the code (instead of in comments). Java has JML which is a syntax for writing pre and post conditions in comments, as well as some tools to do extra checking, add runtime checks to your code (or not) based on the conditions, write the conditions into JavaDoc properly, and automatically generate JUnit tests based on the conditions. If you program in Ada there's SPARK which supports pre and post conditions as comments as well as a range of other annotations, and provides extremely powerful tools to do extensive static checking and analysis and even generate automatically simplied proof obligations based on your annotations. If you program in Python there's PyContract which allows you to write pre and post conditions into docstrings and switch on or off runtime checking of those contracts. I expect there are plenty more, so hopefully other people can mention those.

Jedidiah.

When you are writing software for life-critical applications, there is various software and techniques that ensures bug-free code. Just look at all the airplanes, powerplants, car computers, etc. It's not very usual at all to see one fail critically.

When you are writing software for life critical systems, there are methods you can follow that allow you much greater assurance of correct code and drastically reduce the testing burden (byt being abel to prove that certain classes of errors don't exist in the code). It's akin to static types, which allow you to statically catch a lot of type errors obviating reducing the need to spend time testing for possible type errors.

The languages and methods used are things like SPARK and B-method The beauty of systems like SPARK is that they provide a degree of flexibility in how much work you go to depending on how much extra assurance you want. It is quite possible to simply specify critical portions of code with a little extra formality (basically extended static checks beyond what type checing alone can give you) through to fully specifying everything and doing formal proofs for the whole system. You can tailor the effort and assurance to the needs of the project.

(This time without that dangling link - that'll teahc me not to preview)

Jedidiah

When you are writing software for life-critical applications, there is various software and techniques that ensures bug-free code. Just look at all the airplanes, powerplants, car computers, etc. It's not very usual at all to see one fail critically.

When you are writing software for life critical systems, there are methods you can follow that allow you much greater assurance of correct code and drastically reduce the testing burden (byt being abel to prove that certain classes of errors don't exist in the code). It's akin to static types, which allow you to statically catch a lot of type errors obviating reducing the need to spend time testing for possible type errors.

The languages and methods used are things like SPARK and B-method among others. The beauty of systems like SPARK is that they provide a degree of flexibility in how much work you go to depending on how much extra assurance you want. It is quite possible to simply specify critical portions of code with a little extra formality (basically extended static checks beyond what type checing alone can give you) through to fully specifying everything and doing formal proofs for the whole system. You can tailor the effort and assurance to the needs of the project.

Jedidiah.

It's probably closser to SPARK, but yes, it's the same general idea though in this case with the little more emphasis on static analysis and theorem proving. Eiffel is great though - I wish more people would use it, or something similar like SPARK, JML, Spec# etc.

Jedidiah.

This is just a research OS written in C#.

No, it's written in Sing# which is an extension of Spec# which is an extension of C#. People really ought to pay more attention to Spec# - it's a nice extension of C# that allows for more formality if and when you require it. It's in the same class of language as SPARK which is an extension of Ada, JML which extends Java with specification semantics, BitC, Extended ML, HasCASL, and I guess to a lesser extent things like Eiffel and D.

Think of it this way: static types and type signatures for functions allow you to specify things about the software that the compiler can statically check and make sure there aren't any silly errors. The languages listed above (to varying degrees) allow for more exacting specification about the software, and hence you can (with the right tools) do far more comprehensive static checking and ensure various properties of the software. The difference is that, with most of these languages, the amount of specification is optional - you can be as exacting as you want where you need it, and not bother where you don't. It's like a dynamically typed language that lets you declare and use static types (and check them)just for those areas of code where it matters (except you start with static types and can provide more exacting specification where it matters). It's well worth checking out.

Jedidiah.

No, it cannot.

But that doesn't mean that all attempts at any kind of proof (either through testing or through formal deduction and inference) are a waste of time. It's not a question of "proving something 100%". It's a question of gaining sufficient confidence that the system will work as intended. How much is "sufficient"? That depends on the application. In some cases, testing is more than sufficient to build the necessary level of confidence. The key thing to keep in kind is that formal logical proofs are able to cover a much wider range of inputs than testing can possibly cover, so for high-confidence applications they start to make more sense. That doesn't necessarily mean that you have to logically prove the entire app, just the "critical" parts (while only testing the non-critical parts).

As an aside, there's a good case to be made for logical proof actually being more cost-effective than testing - see, for example, this paper.

Really? And yet these guys seem to do a pretty good job of consistently delivering on-time, on-budget, and with an order of magnitude less defects than the rest of the industry. Is their methodology "guaranteed"? Of course not. Neither are development projects in other engineering domains. There's always risk involved in a new development. But the approach used by Praxis (careful requirements elicitation; risk-driven planning; formal specification where necessary; design by contract; etc. etc.) has been consistently demonstrated to increase the likelihood that the product you get is the product you wanted.

There is nothing inherent in software that makes it impossible to engineer. In fact, in many ways it's easier to engineer - you don't have to account for material failures, interactions between physical laws, or any of the million-and-one other things that make designing a physical product hard. All you need to do is develop a logical construct. Software development will only remain "an art" if the practitioners of software development continue to treat it as one. And that will only be tenable for as long as people are willing to accept software that is buggy and often malfunctions. The reason that every other engineering discipline emerged was that regular failure of the products in that domain could not be tolerated. It will be no different with software.

A programming method that involves designing an application such that you break each top level logical component/ability down until you a) know that you have to impliment it or b) it is found to have already been done.

That already exists, and the specification is indeed amenable to proof tools (several specification languages use HOL as their proof assistant even!). Check out B-method, HasCASL, SPARK, Extended ML, or even Z and VDM. There are tools like Perfect Developer. There are specification extensions to Java like JML that support extended static checking and proof via other tools.

Uptake has been slow, and the tools associated with this stuff are still maturing (despite the fact that formal specification is a relatively old field - tracing it's way back to Djikstra and Hoare in the late 60's). Doing specification properly tends to require a little more math background, and does take some work. More importantly, for a great many projects, it simply isn't suitable. There is no magic process you can follow that makes everything work, and there is no "final" programming model. There are whatever mix of techniques and models suit the project at hand. Good developers are ones who know lots of models and techniques and adapt them to best fit the problems at hand.

That said, specification is sorely underrated and underused as a programming technique. Too few people are well acquainted with it, and almost all the complaints that often get raised are based on myths and misnomers. It's not right for everything, but there are plenty of places where perhaps it could and should be used. Knowing how to do proper formal specification is simply another weapon in a good developers arsenal, and I wish more people spent the little extra time required to learn something about it.

Jedidiah.

Care to name a few companies which have significant CS R&D labs?

There are plenty out there, though a lot of them are small and thus probably under your radar. For a random example of one I've encountered try Praxis Critical Systems who do a lot of interesting work in verification, refinement systems and that sort of thing. You could try Certicom who have a lot of interesting work in the cryptography front - and a decent portion of that is work of efficient algorithms and secure protocols as well as the pure math side. There's Telecom Italia who are doing interesting work in agent architectures (I just happen to know of then having used JADE, their agent system, once).

If none of that appeals I'm sure there are literally hundreds more companies, those were just random ones I knew off the top of my head. And beyond that you have government work: DARPA, NSA, and many others are all quite interested in cutting edge CS work (look at SELinux from NSA for example, a demonstration of their research work into secure architectures).

If you open your eyes and look there is no shortage of opportunities.

Jedidiah.

Care to name a few companies which have significant CS R&D labs?

There are plenty out there, though a lot of them are small and thus probably under your radar. For a random example of one I've encountered try Praxis Critical Systems who do a lot of interesting work in verification, refinement systems and that sort of thing. You could try Certicom who have a lot of interesting work in the cryptography front - and a decent portion of that is work of efficient algorithms and secure protocols as well as the pure math side. There's Telecom Italia who are doing interesting work in agent architectures (I just happen to know of then having used JADE, their agent system, once).

If none of that appeals I'm sure there are literally hundreds more companies, those were just random ones I knew off the top of my head. And beyond that you have government work: DARPA, NSA, and many others are all quite interested in cutting edge CS work (look at SELinux from NSA for example, a demonstration of their research work into secure architectures).

If you open your eyes and look there is no shortage of opportunities.

Jedidiah.

Aside from the compulsory Slashdot Java FUD, it's really not a joke. Java has a big advantage in that the the bytes codes produced can be verified, and so the program tested, without any concerns of the final deployment platform. This is a major advantage for an organisation like NASA which most likely has a wide range of hardware on which software is deployed.

Which is nice, but when it comes to serious mission critical software where faults can't be tolerated Ada has some advantages. Call me when Java has anything equivalent to SPARK for validating code.

Jedidiah

If you learned Ada then you may want to spend the little extra time required to learn SPARK and learn how to write useful comments that can actually be used to reduce errors by (based on case studies) a factor of about 100 over C code.

Jedidiah.

There is nothing they couldn't dream up as a terrorist or other attack on the IT infrastructure that hasn't been thought up already by others, even in the terror game it is hard to be truely original. And at least by going through the exercise of thinking like an attacker they may help spur the development of better defenses, traps, early warnings, recovery procedures , what have you.

The problem is not that no one has thought about the problems of security of software assurance enough to have come up with solutions, the problem is the solutions haven't made their way out of theory and into practice. It's not that the theory is new either - a lot of the ideas are 10 years old or more. The problem is that there are too many people who are happy with what they have and never bothered to look at what the theorists have actually devised. Why do you think the NSA created SELinux? It wasn't because they were planning to create a secure operating system - they themselves say that they did it to demonstrate that such controls can easily be built into "mainstream operating system". Read that as: the've done the research, know the solutions (this sort of architecture is, research wise, quite old), and are so frustrated that no one was actually using it that they hacked it into the most mainstream OS they could just to show people how.

If you consider the task of writing secure software applications, rather than just OS architectures to vastly enhance security, there are still perfectly good options out there. If you're serious about high integrity software (be it for security, or for fault tolerance) you ought to be proving your code. No, seriously - you can statically mathematically prove your code providing you use the right tools. For instance there are things like B-method or SPARK which use allow you to actually prove the partial correctness of your code (partial correctness in the sense of "if it terminates, it terminates with these properties..."). The concept of having a separate prover as a safety and correctness checker, as opposed to letting static typing and the compiler catch the most glaring errors, seems eminently sensible. The techniques for how to do this sort of thing are quite old, and it is becoming increasingly practical to do full proofs given the power of computers these days. Again, this is the category of "something we know how to do, but mostly never bother with".

Jedidiah.