Slashdot Mirror

Java is also the perfect high security language, because you can't make security holes with it. Same with C#. Same with VB.NET. We've heard this again and again from people who simply don't understand the problem.

Yes, the first assumption should always be that the NSA don't understand security... Or perhaps there are languages and tools that help you write more secure code. Let's be honest, the average Java program is more secure than the average C program, thanks to slightly stronger type checking and bounds checking. Sure, Java isn't a going to magically make your code perfectly secure, but it does make it a little harder to make mistakes, and a little easier to catch them when you do make them. One can imagine that perhaps there are other things that can be done to make mistakes harder again to make, and even easier to catch. Sure, it's all incremental, and nothing is going to be a silver bullet, but enough small gains and it can become worthwhile for software you want to be robust and/or secure.

I've programmed in C and Java, and I've also played with SPARK Ada. Believe me when I tell you that SPARK really does make a huge difference in catching mistakes. Just using SPARK won't magically make your code secure, but it will provide you with very powerful tools to help you write secure code. It really is a very distinct improvement. If it's the Ada part that you find distasteful, then check out JML and ESC/Java2 which provide similar (though not quite as powerful) facilities for Java.

Or another fun one.

/* function foo()
does this, that, and another thing. ... big long description of inputs, outputs, constants that affect it, whatever ...
*/
void foo() {blah }

... and the description is horribly out of date because it's been changed a million times.

One way to assist with these situations is to use something like JML, which gives you a more formal language to write your "does this, does that, constraints on inputs and outputs" comment wit the following bonuses: the formal comment gets included in the documentation; you can automatically generate unit tests from the formal comment, so tests will fail badly if the comment and code fall out of sync; you can use other tools (like ESC/Java2) to run automated checks that the rest of your code is using the function correctly (i.e. not assuming anything about inputs or outputs that can't be guaranteed by your formal comments). All up that's quite good gains for the tiny extra work of learning JML to write your comments in.

I've seen RSpec. Personally if I'm going that route I would prefer stepping up to proper specifications like JML. It's definitely better for providing documentation, at least in the form of API documentation. Then again, Eiffel or Spec# wold also fit the bill. I'm not really knocking RSpec: it's really very nice -- I'm more trying to point out that there are a few more strings you can add to your bow if you like that sort of approah (ad that literate programming is still one of them).

Just to make this a little more clear for the practical minded: the end result can be learning JML, a language that allows for annotations to Java (such as pre- and post-conditions for methods, assignability clauses for private variables, etc.). What benefit does that get you? Well you can use ESC/Java2 to run a theorem prover over those assertions about how things are supposed to work to verify that you code will actually meet all the claims you make of it (which is great for catching subtle unlooked for conrner cases). You can use the jmlunit tool from JML itself to create an automated set of unit tests to exercise you code against your annotations, and you also get (via jmldoc) to have your requirement annotations automatically included in your javadoc api documentation. When you consider that, for a lot of code, you ought to be writing those methods requirements up in api documentation anyway, all the extra extremely rigorous (and static/compile time) checking is just gravy. So there is plenty of practical benefit that's easy to get. To make best use of it, of course, you do need to have some grounding in how this sort of thing works so you can write your specifications well (no different, in many ways, than having some grounding in how CPUs work so you can write more efficient code).

JML is a formal specification language for writing contracts for your Java programs. (It has nothing to do with UML or XML, other than sharing two letters.)

There are a number of quality research tools that understand JML including a compiler (jmlc), a documentation generator (jmldoc), a unit test generator (jmlunit), and an extended static checker (ESC/Java2), a kind of automated theorem prover, like FindBugs on steroids).

These tools and technology let you do design by contract and contract-based unit testing in Java 1.4 and are used by many universities and companies to help them build quality software. See the ESC/Java2 FAQ for more information.

Disclaimer: I am part of the research community that develops JML and the co-author and maintainer of ESC/Java2.

Joe

ESC/Java has been picked up by a group based at the University of Nijmegan. Their new version, cleverly called ESC/Java2, supports the full syntax of JML for writing specifications and is more expressive than the last version from Compaq/SRC. The JML project also provides tools for runtime testing of assertions in Java code (like Java 1.4's assert, but much more expressive), and for automatically generating unit tests from method specifications.

Both the JML tools and ESC/Java2 are open source. ESC/Java2 is based on patches applied to the source available from Compaq/SRC; a combined binary download is available.

If you're interested you can get ESC/Java 2 or the JML tools by following the links.

Full disclosure (or shameless plug): The JML tools are developed primarily by my adviser's research group at Iowa State University. The tools run on top of the MultiJava compiler that I developed as part of my M.S. degree. JML works with pure Java, but you might be interested in the MultiJava language, which adds multiple dispatch and open classes to Java. More info. on Multijava is available from MultiJava.org.