Feeds

Researchers forge secure kernel from maths proofs

Machine verified micro-kernel

Internet Security Threat Report 2014

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. ®

Top 5 reasons to deploy VMware with Tegile

More from The Register

next story
Regin: The super-spyware the security industry has been silent about
NSA fingered as likely source of complex malware family
Why did it take antivirus giants YEARS to drill into super-scary Regin? Symantec responds...
FYI this isn't just going to target Windows, Linux and OS X fans
Privacy bods offer GOV SPY VICTIMS a FREE SPYWARE SNIFFER
Looks for gov malware that evades most antivirus
Home Office: Fancy flogging us some SECRET SPY GEAR?
If you do, tell NOBODY what it's for or how it works
HACKERS can DELETE SURVEILLANCE DVRS remotely – report
Hikvision devices wide open to hacking, claim securobods
'Regin': The 'New Stuxnet' spook-grade SOFTWARE WEAPON described
'A degree of technical competence rarely seen'
Syrian Electronic Army in news site 'hack' POP-UP MAYHEM
Gigya redirect exploit blamed for pop-rageous ploy
Astro-boffins start opening universe simulation data
Got a supercomputer? Want to simulate a universe? Here you go
prev story

Whitepapers

10 ways wire data helps conquer IT complexity
IT teams can automatically detect problems across the IT environment, spot data theft, select unique pieces of transaction payloads to send to a data source, and more.
Getting started with customer-focused identity management
Learn why identity is a fundamental requirement to digital growth, and how without it there is no way to identify and engage customers in a meaningful way.
How to determine if cloud backup is right for your servers
Two key factors, technical feasibility and TCO economics, that backup and IT operations managers should consider when assessing cloud backup.
Reg Reader Research: SaaS based Email and Office Productivity Tools
Read this Reg reader report which provides advice and guidance for SMBs towards the use of SaaS based email and Office productivity tools.
Security and trust: The backbone of doing business over the internet
Explores the current state of website security and the contributions Symantec is making to help organizations protect critical data and build trust with customers.