Researchers in Australia have determined a way to prove that the kernels in mission-critical systems are safe, through the magic of mathematics. This method, which is being reported by CNET, is said to prove that written code is free of many different forms of errors, and it"s hoped that it does, as the systems it"s aimed at are built for aircraft and other vehicles.
The company is called the Information and Communications Technology Centre of Excellence, and is aimed at private-sector research. The first ever kernel they developed with the new checking method is called the secure embedded L4 (seL4) microkernel, and will benefit a lot of different sectors, including businesses. A man named Lawrence Paulson, who is a professor of computational logic at Cambridge University"s Computer Laboratory, said, "I regard the software industry as a real mess. If you"ve ever used a computer you know how unreliable they are. This is an important way of making it better."
A researcher at the company responsible for this, Gerwin Klein, said, "Formal proofs for specific properties have been conducted for smaller kernels, but 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." What this means is that many different attacks used in the technology world (like the ones exploiting buffer-overflow vulnerabilities, as CNET says) would not work against this new kernel.
This research has taken four years to complete, and will now be handed to the Open Kernel Labs for a bit more development, which is a company derived from the original developer.