Researchers mathematically prove security of new kernel

Researchers in Australia have determined a way to prove that the kernels in mission-critical systems are safe, through the magic of mathematics. This method, which is being reported by CNET, is said to prove that written code is free of many different forms of errors, and it's hoped that it does, as the systems it's aimed at are built for aircraft and other vehicles.

The company is called the Information and Communications Technology Centre of Excellence, and is aimed at private-sector research. The first ever kernel they developed with the new checking method is called the secure embedded L4 (seL4) microkernel, and will benefit a lot of different sectors, including businesses. A man named Lawrence Paulson, who is a professor of computational logic at Cambridge University's Computer Laboratory, said, "I regard the software industry as a real mess. If you've ever used a computer you know how unreliable they are. This is an important way of making it better."

A researcher at the company responsible for this, Gerwin Klein, said, "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." What this means is that many different attacks used in the technology world (like the ones exploiting buffer-overflow vulnerabilities, as CNET says) would not work against this new kernel.

This research has taken four years to complete, and will now be handed to the Open Kernel Labs for a bit more development, which is a company derived from the original developer.

Report a problem with article
Previous Story

iPhone 3GS satisfaction rate at 99 percent

Next Story

Neowin's top 10 Firefox Add-ons you can't live without

25 Comments

Commenting is disabled on this article.

This company does seem to be on the correct path. I love this paragraph they have in their article on it.

<quote>
Of course, the issue of software security and reliability is bigger than just the software itself and involves more than developers making implementation mistakes. In the contract, you might have said something you didn't mean (if you are in a relationship, you might have come across that problem). Or you might have meant something you didn't say and the proof is therefore based on assumptions that don't apply to your situation. Or you haven't thought of everything you need (ever went shopping?). In these cases, there will still be problems, but at least you know where the problem is not: with the developers. Eliminating the whole issue of implementation mistakes would be a huge step towards more reliable and more secure systems.
</quote>
http://ertos.nicta.com.au/research/l4.verified/

is this the same sort of modeling that gave us AGW? If so, be prepared for some serious security problems in new kernel

RealFduch said,
Well I see reports about Linux Kernel Vulnerabilities quite often. Rare for windows though.

One is open, the other isn't. How surprising.

xendrome said,
Oh so thats how we are going to flip it from now on?

Why not? The Linux kernel is open for everyone, no wonder there's greater scrutiny of the code by both developers and hackers.

RealFduch said,
Well I see reports about Linux Kernel Vulnerabilities quite often. Rare for windows though.

because the linux kernel is more complete and because is open source then, they can't put the report of vulnerabilities under the carpet.

xendrome said,
Oh so thats how we are going to flip it from now on?
Flip what?
Everybody is free to access, evaluate and hack on an open source kernel.
You can't do that on a closed-source kernel: the only reports are bound from the developing company itselft, which is simply not going to post vulnerabilities and their proof-of-concept of its own product.

Give it time, it will be broken. Just like that encryption method they said would never ever be broken, was broken, what, a day later using a laser?

Never say never, it will save you heartache.

I believe it was a quantum cryptography method (which I originally read about here, and some college student broke it the next day).

Amodin said,
Give it time, it will be broken. Just like that encryption method they said would never ever be broken, was broken

Any cryptography methods certain huge amount of work to be done to crack it. If computers become able to do this work in a few months then the method is considered unsafe. It doesn't always indicate some kind of flaw.

Amodin said,
Give it time, it will be broken. Just like that encryption method they said would never ever be broken, was broken, what, a day later using a laser?

Never say never, it will save you heartache.

I believe it was a quantum cryptography method (which I originally read about here, and some college student broke it the next day).


It won't be broken by developer mistakes in the code leading to e.g. buffer overflows, but it could be in other ways of course.

Ci7 said,
how long till Microsoft buy it out :P ??

You can download Singularity for some years. And it's not only kernel. It's an OS.

Now I just wish the kernal would get into the hands of consumers. It would be awesome if Microsoft took that kernal but I doubt they will.

well there's no point for it. any company applying such things into consumer operating systems would be wasting vast amounts of nothing. these kernels, as stated in the article, would be useful for critical tasks, like in an airplane or space shuttle or even satellites and space rovers. things that have very expensive liabilities and have huge risk, they need something that is guaranteed to work 100% of the time. people who just use their computer to surf the web don't need that reliability

Riiight because it's quite often space rovers and satellites have their buffer overflows attacked.

I don't think you quite understand what this means.

This is about security, not reliability.

Omen1393 said,
Now I just wish the kernal would get into the hands of consumers. It would be awesome if Microsoft took that kernal but I doubt they will.

Microsoft Research has created Singularity for this.

Omen1393 said,
Now I just wish the kernal would get into the hands of consumers. It would be awesome if Microsoft took that kernal but I doubt they will.

This is not a kernel aimed for consumer use.

A kernal that is not reliable can not be secure normally. Although I have grave mis-trust of this mathematical process of proving that it is secure without massive review by the community too often we have heard that something is proven secure and it turns out to be to well trusted and not reviewed well enough by the community. I still think that whatever mathematical process they are using is a great leap forward but for now it should not be 100% trusted.