FLAWS in the code, or "kernel", 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 companyNICTA 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.
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's code were secure,Gerwin Klein of NICTA and his team first had to come up with a mathematical method to express the code. "In 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.
No comments:
Post a Comment