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).