A computer crash and reboot are frustrating enough, but even more so when it’s an embedded system running a surgical robot, a weapons system or a self-driving car. Waste time rebooting and you could be dead.
Breakthrough Australian research could dramatically reduce the odds of that happening. Researchers at NICTA, Australia’s ICT Research Centre of Excellence, have just announced … well, how can I explain this?
Computer programs are complex machines made of mathematics — vastly more complicated than physical machines like nuclear reactors or spacecraft. Software is written by humans, and humans make mistakes. Typically, you can expect about 10 errors per thousand lines of computer code, and software like Microsoft’s Vista or OS X, or even applications like Microsoft Office or Adobe CS3, contain tens of millions of lines.
Given this complexity, programmers simply can’t test for every potential error. All software has bugs, and the bugs are only fixed when someone finds them. That’s why we all download and install software patches every month. Unless the hackers get there first. Which they do.
Safety-critical systems are better-written: “only” one to three errors per thousand lines. Even so, the engine controls of a Boeing 777 have 100,000 lines of code, the flight controls of an Airbus A380 millions, so that error rate is still unacceptable.
Software is just mathematics, though. For decades computer scientists have dreamt of using mathematics to prove that software works as advertised. It’s called formal methods. It’s incredibly time-consuming and therefore expensive, so it’s usually only done for things like those aviation systems.
That’s where this NICTA research comes in.
After four years of work, principal researcher Dr Gerwin Klein and a combined team from NICTA and UNSW have formally proved the correctness of the Secure Embedded L4 (seL4) microkernel — loosely speaking, the microkernel is the core part of a computer’s operating system which talks to the hardware and upon which everything else depends.
“What we have done is a general, functional correctness proof which has never before been achieved for real-world, high-performance software of this complexity or size,” says Klein.
Translation: They’ve verified the entire operation of this microkernel. Programmers can build software on top of it and be certain that it’ll function correctly.
The proof also shows that many kinds of common hacker attacks, such as buffer overflows, simply will not work on seL4.
Along they way, NICTA has developed automated tools and a body of techniques which speed up these formal methods, paving the way for a new generation of software capable of unprecedented levels of reliability.
NICTA will soon transfer the intellectual property to their spin-out company Open Kernel Labs, whose software is already used in millions of consumer devices worldwide.
“[This work] provides conclusive evidence that bug-free software is possible,” says Professor Gernot Heiser, OK Lab’s Chief Technology Officer.
“This will end up in products in one to two years,” he told The Australian. The Department of Defence seems to be very interested. Overall, it could be worth billions.
For the geeky details, see NICTA’s L4 verified project. A scientific paper will appear at the 22nd ACM Symposium on Operating Systems Principles (SOSP).
Before anyone else says it, yes, I do know that not all operating systems have a microkernel. But, like, how much Deep Geek can people cope with?
I know nothing about this at all, but suspect some hard maths has gone down. Very interesting stuff; I can cope with more nerdiness.
Presumably to get to the point of being able to prove that a program implements its specification correctly, one needs to go through extensive testing and debugging. The question would be how much time and effort one wants to devote to that task before releasing a program. Current practices show that there is a limit – a certain level of defects is accepted, especially with time pressures and commercial pressures.
This research may have its uses and I’m curious to know how easy it is to re-prove correctness after a change in specifications or implementation.
Certainly won’t result in bug-free software though.
Another problem with this approach is that it moves complexity from the implementation to the specification. I’d be interested in seeing what their formal specifications look like. If, as they say, a specification defines “what” something should do rather than the “how” it does it, it might be marginally better than the implementation. However, for a specification to fully define a problem I expect it would still be almost as complex.
If they have done what they say they have done then essentially we should be able to get a new programming language – the one used for the formal specification.
@Barry Brannan: Some good points and questions there. I’ll do some more digging.
Part of the point of a formal proof is that you wouldn’t need as much testing because, well, you’ve proved that it does what it was specified to do Yes, that does mean the specification needs to be in a formal language too, not just hand-waving manager-speak. Specification languages look kinda like programming languages — and there are many in existence already, though I daresay most working programmers never use them and may not even know they exist.
Yes, formal methods are a lot more work — at least until this NICTA work came along. My understanding is that all this dramatically changes the relative effort involved in formal methods, which in turn means they can be used in places where they’d previously have been too expensive.