Slashdot Mirror
Google Brings Design-By-Contract To Java
angry tapir writes "Google is developing a set of extensions for Java that should aid in better securing Java programs against buffer overflow attacks. Google has announced that it open sourced a project that its engineers were working on to add a new functionality into Java called Contracts, or Design-By-Contract. 'Contracts exist to check for programmer error, not for user error or environment failures. Any difference between execution with and without runtime contract checking (apart from performance) is by definition a bug. Contracts must never have side effects.'"
There have been several projects that have tried to do this before but the developers never saw it through. When annotations were added in JDK5 this was one of the features I've been looking for. Being able to define invariants on the interface will make implementations much more safe and consistent!
I did not realize buffer overflows were a problem for apps written in Java. Java has built-in "generic" dynamic data structures which should be suitable for 99% of the software any of us write. Why would we ever be manually managing memory in Java? Doing so should be "considered harmful" to a far greater degree than goto statements.
A slashdotter who didn't build his own computer is like a Jedi who didn't build his own lightsaber.
Actually, Google is bringing Programming by Contract to Java. Design by Contract is trademarked by Eiffel Software (and Bertrand Meyer).
I'm sure Oracle will be only too happy to work with Google to add this to the JDK, right? Right?
GCHQ Quantum Insert installed. If only our tongues were made of glass, how much more careful we would be when we speak
It is a String-based implementation, which is awful in terms of consistency, type-checking, etc. and vulnerable in code refactoring. I would stay away or use something more type-safe and IDE-safe.
By the way, Eiffel already pattented "design by contract". Therefore, it cannot be open sourced.
Using strings instead of compiled code is too fragile. org.apache.commons.lang.Validate or com.google.common.base.Preconditions are much better for this kind of validation.
Is what this sounds like to me. I've always felt an important part of strong C programming was to put a set of asserts at the top of each function that asserts the properties of the function's input (numeric ranges, non-NULL pointers where applicable, etc). Again, not for user input validation, but for validating software design assumptions that make up the contractual interface between caller and callee.
Java does not have buffer overflows unless the JVM has a bug, or you're calling out to unsafe code via JNI. The lack of such memory errors is the very definition of memory safety.
Higher Logics: where programming meets science.
The software engineering group at MIT (Liskov, Guttag, etc) have been pushing for this since the early 1980s. Guttag told us in lecture that he tried unsuccessfully to get these concepts built into the Ada specification.
According to Wikipedia there are already quite a few projects doing DbC:
Java, via iContract2, Contract4J, jContractor, Jcontract, C4J, CodePro Analytix, STclass, Jass preprocessor, OVal with AspectJ, Java Modeling Language (JML), SpringContracts for the Spring framework, or Modern Jass, Custos using AspectJ,JavaDbC using AspectJ, JavaTESK using extension of Java.
Do we really need an entirely new one? If none of those are sufficient, why not build on top of and improve an existing project? Starting over is not always a good thing...
Isn't throwing an error a side-effect?
WARNING! This girl exceeds the MAXIMUM SAFE standards established by the FDA for BRATTINESS
I'm still waiting for a decent compile time DbC. Runtime checks won't catch an untested control flow, and when the fault does happen you better hope it happens in your lab and not on a client's computer. You can read my analysis of this in my Master's thesis (which focused on unique references that were ensured to be unique at compile time):
http://www.worldcat.org/title/applying-uniqueness-to-the-java-language/oclc/701244184&referer=brief_results
It's not a side effect, it's the INTENDED effect.
Isn't throwing an error a side-effect?
You can do all of this range checking yourself manually in your code if you want, there is nothing new here.
These annotations just do the dirty work of pumping out the boilerplate code. You could do it yourself with an emacs macro or some such.
@Requires({
"Collections.isSorted(left)",
"Collections.isSorted(right)"
})
@Ensures({
"Collections.containsSame(result, Lists.concatenate(left, right))",
"Collections.isSorted(result)"
})
List merge(List left, List right);
Seriously, let's just toss out the whole idea of syntax checking or anything. I could put these into individual asserts and they would be hilighted by my IDE and checked by my compiler, and with a simple //REQUIRES or //ENSURES comment, it would be no less obvious to the reader. Now real DBC also involves checking things like class invariants and making sure that preconditions never narrow and postconditions never expand, but I know Google's little hack doesn't do class invariants, so I kind of doubt it does the latter two either.
Google has some great Java code -- guava is probably the best collections library out there, for instance -- but this sad little hack is not it.
I've seen that contract thing being used on a project. It was gruesome, and needless most of the time. I had to remove all the contract enforcements just to understand the underlying code. I guess I'm allowed to be a skeptic on this technique.
tl;dr Contracts suck.
I rarely respond to comments. Also, don't ask for clarifications: a brain and Google are faster, believe me!
Where's the bury button? Oh yeah - shitdot doesn't have one.
A bug in a contract is like a bug in a specification - it might be harmless but it means you are allowing potentially dangerous/poorly working implementations to be given the rubber stamp of approval.
Contracts are effectively ways of saying "the state of the program before this operation will adhere to rules P" and "after you do this operation I promise that the state of the program will adhere to rules R". Sometimes it is possible to check whether the rules would be broken using a static checker (weeding out certain problems at compile time). Some properties can only be checked at runtime (and thus a runtime exception is thrown giving a better clue as to where the problem lies when it blows up). Contracts are tools to help programmers write correct programs to be written and like a bad test suite, bad contracts won't help you all that much in achieving that.
The idea of contracts is that clients write their code to work with anything which fulfills the contract. So let's say you have some client code written, but then determine that there's a bug in the contract. What does this mean? The client code is either written for the "buggy" contract, or the client code was ALSO buggy and written for the intended contract. At that point, it seems that the client has failed to grasp what the contract is in the first place. The idea is that the contract cannot be buggy, since it is the definition of correct. If your clients code to the contract, you can't go changing it without breaking clients. The contract may be badly-designed, and it's good to avoid bad designs, but once you have clients, to go in and try to fix a "buggy" contract is to water down what contracts mean in the first place. It encourages clients to ignore contracts and code to what they imagine the routine should do. At that point, you might as well abandon contracts because they aren't being used as the definition of what is correct anymore, just a vague guide as to what the routine might do.
Eiffel and Ada have had 'design by contract' as a key language feature for 25+ years, and this is a major contribution to both 'safety' and correctness of design. It's good to see Java catch up.
The "definition of correct" is the system working the way it should. I'm not sure what you're suggesting here: that a system should stick with the original, possibly flawed, contracts rather than fix them to operate properly? That once you make an error in a contract, you should live with it forever? I fail to see how that perspective is helpful or realistic, and, forgive me if I'm wrong, but I suspect you may be lacking in practical experience with Design by Contract.
Patrick Doyle
I mod down every jackass who puts his moderation policy in his sig. Oh, wait a sec....
One of the best ones was the DEC Extended Static Checker for Java in the late 1990s. That project died after Compaq acquired DEC and shut down research. But it formed part of Microsoft's efforts for Spec#, which has a formal verification system.
Microsoft has had a huge success with formal proof of correctness - the Static Driver Verifier. This is a system which tries to formally prove that a Windows driver can't crash the operating system. All drivers for Windows 7 have to pass this verifier to be signed, It's an impressive system which works by symbolic case analysis. It yields a proof, a counterexample, or times out analyzing too many cases. About 3% of programs time out. (If your kernel driver has undecidable behavior, it needs work.)
I headed a team that did a proof of correctness system for Pascal back in the early 1980s. That was pushing the limits of what you could do back then; verifying a small program took 45 minutes on a 1 MIPS VAX. Today, with about four orders of magnitude more CPU power, it's a practical technology.
There have been many attempts to bolt some "design by contract" features onto various languages, but they're usually not very good. The problem is saying things about collections. The hacks that try to do design by contract at run time tend to avoid expressions which examine big data structures, since they have to run them over the whole data structure every time. Real verifiers prove or disprove such things at compile time. It turns out, though, that a few standard cases for collections cover many of the usual things you want to say.
Another big issue, which Spec# handles and this Google hack apparently doesn't, is the "insideness" issue for object invariants. Object invariants are supposed to be true whenever control enters and exits an object. But what if an object calls one of its own public methods, perhaps through a long chain of calls? Now, control is inside the same object twice. That violates the invariant rule.
This class of bugs is common in window systems, where all the widget, pane, window, and event objects are frantically calling each other. It also comes up in concurrency, which I don't see Google's hack addressing either.
Does it really require a language extension to throw a runtime error whenever a boolean is met with false? Or is the amazing part that google has found a way to make java even more verbose? I didn't think it could be done.
Securing Java programs against buffer overflow attack implies never to use unbounded strings in code everywhere.
In order to enforce this, it would be important to have some compile-time mechanisms in the language.
In Ada, the strength is the deliberate compile-time definition of the range boundaries for the acceptable values. At compile time, many checks are done, but certain types(i.e. unbounded string) and their related services aren't easily compiled unless you are deliberately aware they are being used and are wrapped with all sorts of protection functions to allow the compiler to proceed. At run-time, if the creation/assignment of a particular type is being done, there are inherent range-boundary constraint-checks for the assigned values.
In Java, similar concepts may be achieved by making Classes/Types which have boundary checking in the constructor functions and in the assignment functions/assignment operator functions which throw exceptions when input values are not valid. That should be adequate. Contracts are may be deliberate descriptions, but in order for it to be more useful, it should be part of the language and not built as an external api for the java language or a precompiler tool for the language. Ada got it right and like you said it's been around for over 25 years. But java language maintainers are listening because they have brought in Ada-like generics, Ada-like enumeration types, and c++ templates into the new versions of the language. The fact that there are different existing apis using different vocabulary and dancing around the same "Design by contract for java" concepts is the subtlety to listen to. If the language designers listen to this, they might admit the java language spec is in some respects still immature in terms of code maintenance stability. It wouldn't surprise me to see in upcoming Java language releases they bring in new Ada-like concurrency, constraint/boundary checking and Eiffel-like Design-by-Contract(i.e. make it difficult to compile with unbounded strings) into the Java Language also.
This is one of the most ignorant articles I have read in a while. Some priceless quotes:
"Primarily touted as a technique to ease programming, Contracts could also provide an easy way for developers to guard against buffer overflow attacks, the researchers said."
Really?! I'd love to see you explain that one to me. There is no way to guard against buffer overflow attacks in Java because you don't have low-level access to memory in the language, hence you don't need to do any guarding.
"In December, Microsoft identified 2.6 million possible attacks that could be waged using a stack-based buffer overflow in the JRE (Java Runtime Engine)."
Actually, no. What Microsoft said was that 2.6 million attacks took advantage of JRE flaws involves buffer overflows, not that there were 2.6 million possibly vulnerabilities in the JRE. There were in fact only 3 and they were patched months ago.
My 2 cents: I love the idea behind design by contract but sticks code in String annotations is just plain ugly. I'd rather stuck to Asserts, thank you very much.
Guilty as charged. Still, my point was that in the case you describe, there is a problem with the design of the system, not merely the contract.
I was learning Eiffel and had been coding in Ada for a couple of years when Java showed up. I was surprised then that Sun's language designers had given us a language that was already 15 years behind the state of the practice, let alone 30 years behind the state of the art.
human seldom subscribes/stick to contracts or stuff like that.
for performance trade-off..even it's only compile-time.
and how can human make error-nil contracts?..
they even can't write code..let alone the checking stuff.
pls contracts the contracts..ohoh..dead-loop'n'recursive
Or you could use the .Net Code Contracts which do all this with static analysis. Therefore you get proof up front that your contracts will never be violated by non exposed code, and without a performance penalty at run time. If a contract cannot be verified, warnings are given. You can then introduce appropriate branching to provide guarantees as necessary. http://research.microsoft.com/en-us/projects/contracts/
Ah I see what you mean now. Actually I think you've hit upon the key feature of Design by Contract that most people miss. It's not just tossing assertions all over your code. It's a design discipline that shapes the way you write the system, and that's why it's good at finding design problems.
Patrick Doyle
I mod down every jackass who puts his moderation policy in his sig. Oh, wait a sec....
In fact it does do class invariants, and inheritance with preconditions that never narrow and postconditions that never expand.
You can also use Eclipse's as-you-type compilation to get instant syntax checking.
Perhaps you should actually look at the project before you criticize :)