According to them, the Secure Embedded L4 microkernel has potential applications in defence and other safety and security industries where the flawless operation of complex embedded systems is of critical importance.
"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 or size," said Dr Gerwin Klein of NICTA in Australia, who led an international team.
According to the scientists, the proof also shows that many kinds of common attacks will not work on the seL4 kernel.
For instance, the microkernel is impervious to buffer overflows, a common form of software attack where hackers take control of programs by injecting malicious code. "Our kernel cannot be subverted by this kind of attack," Klein said.
The scientists have successfully verified 7,500 lines of C code and proved over 10,000 intermediate theorems in over 200 000 lines of formal proof. The proof is machine-checked using the interactive theorem-proving program Isabelle. It is one of the largest machine-checked proofs ever done.
"This is a remarkable achievement," said co-scientist Yale University's Zhong Shao. "It makes a significant advance toward building fully verified system software with meaningful dependability guarantees."
Added co-scientist Lawrence C Paulson of Cambridge University: "It is hard to comment on this achievement without resorting to cliches.
"Proving the correctness of 7,500 lines of C code in an operating system's kernel is a unique achievement, which should eventually lead to software that meets currently unimaginable standards of reliability."