A group of computer scientists have finished worked on the first complex microkernel mathematically proven to be secure, according to the National Information Communication Technology Australia (NICTA) group.

The L4.verified project, which took an estimated 25-to-30 man-years, started with the general purpose L4 microkernel and modified it to allow a formal proof of its security. The work guarantees that certain attacks, such as buffer overflows, will not work on operations performs by the microkernel, Gerwin Klein, the principal researcher who led the project at NICTA, said in a statement.

"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," Klein said in the statement.

Creating secure software has become a major focus of government agencies, universities and the computer software industry. The U.S. government has begun to require that software makers ship their software in a limited number of configurations to make securing the systems easier. Microsoft has already started pushing its own secure-programming initiative to its developers. And, earlier this year, a coalition of industry experts and government agencies published a list of the Top 25 Most Dangerous Programming Errors.

The researchers verified 7,500 lines of code -- the entire seL4 microkernel's code, excluding the boot logic and assembly code. The proof exceeds 200,000 lines in the common proof script, Isabelle -- or about 3,500 pages.

Information on the L4.verified project and the microkernel created by the developers can be found on NICTA's Web site. NICTA plans to transfer the intellectual property in the technology to Open Kernel Labs.

If you have tips or insights on this topic, please contact SecurityFocus.