FLAWS in the code, or 鈥渒ernel鈥�, that sits at the heart of modern computers leave them prone to occasional malfunction and vulnerable to attack by worms and viruses. So the development of a secure general-purpose microkernel could pave the way for reliable computing for us all.
The microkernel, dubbed seL4, is the work of technology research company and the University of New South Wales in Australia and Open Kernel Labs. Their kernel has been pared down to the minimum amount of code needed to link the computer hardware to the applications that run on it.
The team behind seL4 have proved in principle that it is possible to create secure computer code that will run on any system that requires guaranteed security and reliability.
Advertisement
Previous efforts to design code that is free of bugs and immune to malicious attack has produced kernels that were either restricted to a narrow range of tasks or limited to the types of systems they could be used in.
To prove mathematically that the 7500 lines of its kernel鈥檚 code were secure, of NICTA and his team first had to come up with a mathematical method to express the code. 鈥淚n the end, programs are just mathematics, and you can reason about them mathematically,鈥� says Klein.
His team formulated a model with more than 200,000 logical steps which allowed them to prove that the program would always behave as its designers intended. Potentially, the work could be extended to the more complex kernels used in modern operating systems.
鈥淭he model allowed them to prove that the program would always run as its designers intended鈥�
, head of the German government鈥檚 project, says that formal verification will become an increasingly popular method for testing software design. 鈥淚t鈥檚 the ultimate tool of reasoning and the ultimate base of trust you can achieve,鈥� he says. Independently of NICTA, Verisoft developed a verified microkernel in 2006. It was designed for academic purposes and ran too slowly to be commercially viable.
鈥淲e wanted to have a system that was not only verified, but also practically usable,鈥� says of , who headed the seL4 design team.
