Feeds

Researchers forge secure kernel from maths proofs

Machine verified micro-kernel

Protecting against web application threats using SSL

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

Reducing the cost and complexity of web vulnerability management

More from The Register

next story
Early result from Scots indyref vote? NAW, Jimmy - it's a SCAM
Anyone claiming to know before tomorrow is telling porkies
TOR users become FBI's No.1 hacking target after legal power grab
Be afeared, me hearties, these scoundrels be spying our signals
Jihadi terrorists DIDN'T encrypt their comms 'cos of Snowden leaks
Intel bods' analysis concludes 'no significant change' after whistle was blown
Home Depot: 56 million bank cards pwned by malware in our tills
That's about 50 per cent bigger than the Target tills mega-hack
Hackers pop Brazil newspaper to root home routers
Step One: try default passwords. Step Two: Repeat Step One until success
NORKS ban Wi-Fi and satellite internet at embassies
Crackdown on tardy diplomatic sysadmins providing accidental unfiltered internet access
UK.gov lobs another fistful of change at SME infosec nightmares
Senior Lib Dem in 'trying to be relevant' shocker. It's only taxpayers' money, after all
Critical Adobe Reader and Acrobat patches FINALLY make it out
Eight vulns healed, including XSS and DoS paths
Spies would need SUPER POWERS to tap undersea cables
Why mess with armoured 10kV cables when land-based, and legal, snoop tools are easier?
prev story

Whitepapers

Secure remote control for conventional and virtual desktops
Balancing user privacy and privileged access, in accordance with compliance frameworks and legislation. Evaluating any potential remote control choice.
WIN a very cool portable ZX Spectrum
Win a one-off portable Spectrum built by legendary hardware hacker Ben Heck
Intelligent flash storage arrays
Tegile Intelligent Storage Arrays with IntelliFlash helps IT boost storage utilization and effciency while delivering unmatched storage savings and performance.
High Performance for All
While HPC is not new, it has traditionally been seen as a specialist area – is it now geared up to meet more mainstream requirements?
Beginner's guide to SSL certificates
De-mystify the technology involved and give you the information you need to make the best decision when considering your online security options.