7500 lines of Bug Free Code, A Mathematically Verified Crash Proof Operating System Kernel

by

Computer researchers at UNSW (University of New South Wales) and NICTA (NICTA is Australia’s Information and Communications Technology (ICT) Centre of Excellence) have achieved a breakthrough in software which will deliver significant increases in security and reliability and has the potential to be a major commercialisation success.

A team had been able to prove with mathematical rigour that an operating-system kernel – the code at the heart of any computer or microprocessor – was 100 per cent bug-free and therefore immune to crashes and failures.

The breakthrough has major implications for improving the reliability of critical systems such as medical machinery, military systems and aircraft, where failure due to a software error could have disastrous results.

“A rule of thumb is that reasonably engineered software has about 10 bugs per thousand lines of code, with really high quality software you can get that down to maybe one or three bugs per thousand lines of code,” Professor Heiser said.

This will also be relevant to Artificial General Intelligence. Being able to prove that the code you write will do what you want 100% of the time is huge.

Bug Free Code is Possible

Verifying the kernel – known as the seL4 microkernel – involved mathematically proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years.

“The NICTA team has achieved a landmark result which will be a game changer for security-and-safety-critical software,” Professor Heiser said.

“The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake.”

7500 lines of Bug Free Code, A Mathematically Verified Crash Proof Operating System Kernel

by

Computer researchers at UNSW (University of New South Wales) and NICTA (NICTA is Australia’s Information and Communications Technology (ICT) Centre of Excellence) have achieved a breakthrough in software which will deliver significant increases in security and reliability and has the potential to be a major commercialisation success.

A team had been able to prove with mathematical rigour that an operating-system kernel – the code at the heart of any computer or microprocessor – was 100 per cent bug-free and therefore immune to crashes and failures.

The breakthrough has major implications for improving the reliability of critical systems such as medical machinery, military systems and aircraft, where failure due to a software error could have disastrous results.

“A rule of thumb is that reasonably engineered software has about 10 bugs per thousand lines of code, with really high quality software you can get that down to maybe one or three bugs per thousand lines of code,” Professor Heiser said.

This will also be relevant to Artificial General Intelligence. Being able to prove that the code you write will do what you want 100% of the time is huge.

Bug Free Code is Possible

Verifying the kernel – known as the seL4 microkernel – involved mathematically proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years.

“The NICTA team has achieved a landmark result which will be a game changer for security-and-safety-critical software,” Professor Heiser said.

“The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake.”