Feeds

Researchers forge secure kernel from maths proofs

Machine verified micro-kernel

Seven Steps to Software Security

Aussie boffins have developed an operating system micro-kernel mathematically established as free of many types of errors. The development points the road toward "safety-critical software of unprecedented levels of reliability" for applications such as aircraft and cars.

The software - called the secure embedded L4 (seL4) microkernel - was developed by Australia's Information and Communications Technology Centre of Excellence (Nicta). Computer scientists involved in the project say it's the first "formal machine-checked proof of a general-purpose operating system kernel".

The technology is designed for complex embedded systems where reliability is of critical importance, so applications in missiles and other defence-related systems are an obvious application of the software.

The four years of work involved the researchers going through 7,500 lines of code written in the C programming language. They "proved over 10,000 intermediate theorems in over 200,000 lines of formal proof". This proof was then machine-checked using the interactive theorem-proving program Isabelle in one of the largest exercises of its type ever attempted.

The 12-strong NICTA team had to make advances in the mathematical understanding of real-world programming languages and developed new techniques for rapid prototyping of operating system kernels during the project.

All this heavy mathematical lifting means that the kernel ought to be immune to common types of attack, such as buffer overflows. The work draws on the example of earlier projects but goes further, according to the researchers.

"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," explained Dr Gerwin Klein, NICTA Principal Researcher in a statement on the project.

Lawrence Paulson, professor of computational logic at Cambridge University's Computer Laboratory, who developed mathematical tools that Nicta adapted for its project, said that the research could have a knock-on benefit for business. "The project has yielded not only a verified microkernel but a body of techniques that can be used to develop other verified software," he said.

Rigorously testing high-quality code is a complex and expensive process. The project only looked at the kernel of the software. Adding application or networking software into the stack would make the bug-purging process and security proofing project even more complex.

We are, of course, light years away from a HAL-like system that's "foolproof and incapable of error". Nonetheless the project is a significant milestone on the road towards fully verified system software.

NICTA plans to transfer its intellectual property to NICTA spin-out firm Open Kernel Labs, which develops hypervisor (virtualisation) software. ®

Mobile application security vulnerability report

More from The Register

next story
Yorkshire cops fail to grasp principle behind BT Fon Wi-Fi network
'Prevent people that are passing by to hook up to your network', pleads plod
HIDDEN packet sniffer spy tech in MILLIONS of iPhones, iPads – expert
Don't panic though – Apple's backdoor is not wide open to all, guru tells us
NEW, SINISTER web tracking tech fingerprints your computer by making it draw
Have you been on YouPorn lately, perhaps? White House website?
LibreSSL RNG bug fix: What's all the forking fuss about, ask devs
Blow to bit-spitter 'tis but a flesh wound, claim team
Attackers raid SWISS BANKS with DNS and malware bombs
'Retefe' trojan uses clever spin on old attacks to grant total control of bank accounts
Manic malware Mayhem spreads through Linux, FreeBSD web servers
And how Google could cripple infection rate in a second
Mozilla fixes CRITICAL security holes in Firefox, urges v31 upgrade
Misc memory hazards 'could be exploited' - and guess what, one's a Javascript vuln
Don't look, Snowden: Security biz chases Tails with zero-day flaws alert
Exodus vows not to sell secrets of whistleblower's favorite OS
prev story

Whitepapers

Designing a Defense for Mobile Applications
Learn about the various considerations for defending mobile applications - from the application architecture itself to the myriad testing technologies.
How modern custom applications can spur business growth
Learn how to create, deploy and manage custom applications without consuming or expanding the need for scarce, expensive IT resources.
Reducing security risks from open source software
Follow a few strategies and your organization can gain the full benefits of open source and the cloud without compromising the security of your applications.
Boost IT visibility and business value
How building a great service catalog relieves pressure points and demonstrates the value of IT service management.
Consolidation: the foundation for IT and business transformation
In this whitepaper learn how effective consolidation of IT and business resources can enable multiple, meaningful business benefits.