Researchers prove kernel is secure
Can security of software code be proven mathematically? Researchers at an Australian organization believe they have a mathematical proof that it is possible. Australian researchers believe they created an absolute mathematical proof of just this type of function.
It is extremely important to secure the Operating System Core software. With the rise of hackers going after vulnerable systems, it was impossible to guarantee which parts of complex software such as an Operating System, were vulnerable to attacks and exploits. Researchers said they found a way to mathematically guarantee that the code they have written is free of errors. It is not exactly clear until peer reviews are done, whether the mathematical proof can cover every possible error. The security of software is very important, since it is used in aircraft and motor vehicles. It is extremely difficult to make sure that software does not crash and at the same time it is not vulnerable to attacks from hackers.
The Australian information centre, NICTA, a private sector research organization, has also announced the completion of the first formal machine-checked proof. It was run on a general-purpose operating system kernel called L4 microkernel. Cambridge University Computer Laboratory was also involved and they are predicting that the microkernel might lead to many breakthroughs for business software.
Everyone is familiar with news stories of hacked personal and business software systems. This creates havoc for individuals and businesses that leads to loss of billions of dollars each year. NICTA research is a significant step forward to minimizing the threat of software being exploited by hackers. The researchers are handing their mathematical proof over to Open Kernel Labs that will continue further research and development. The research took over four years to develop their program and will continue expanding as OS changes.