Researchers prove kernel is secure

Australian researchers have demonstrated a way to prove core software for mission-critical systems is safe.

The researchers this week said they can prove mathematically that code they have developed, designed to govern the safety and security of systems in aircraft and motor vehicles, is free of many classes of error.

Australia's Information and Communications Technology Centre of Excellence (Nicta), a private-sector research organization, this week announced the completion of the first formal machine-checked proof of a general-purpose operating-system kernel. The kernel is called the secure embedded L4 (seL4) microkernel.

Lawrence Paulson, professor of computational logic at Cambridge University's Computer Laboratory, who developed the Isabelle generic proof assistant Nicta modified to check its kernel, told ZDNet UK that the microkernel breakthrough would have a trickle-down effect for businesses.

"I regard the software industry as a real mess," Paulson said on Thursday. "If you've ever used a computer you know how unreliable they are. This is an important way of making it better."

While rigorously testing high-quality code is expensive, said Paulson, developing such tests and operating systems for specialized purposes would have the secondary effect of improving software in general.

Paulson added that teams in Europe had also made breakthroughs in the formal verification of computer systems, giving the German Verisoft project as an example.

Nicta principal researcher Gerwin Klein, who leads the formal verification research team, said in a statement that previous research had concentrated on giving proofs for specific system properties.

"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," said Klein.

Nicta claimed that many kinds of attack, such as those exploiting buffer-overflow vulnerabilities, would not be successful against the seL4 microkernel.

The intellectual property generated by the Nicta research will be handed over to Open Kernel Labs, a Nicta spinoff firm, for further development. The research took four years, and was conducted by 12 Nicta researchers, in conjunction with the University of New South Wales.

Tom Espiner of ZDNet UK reported from London.

[Seaspray0]

What language was it programmed in?

[n3td3v]

C code.

[mbenedict]

First they validated the design, probably in some abstract language.

Then OS functions were coded in Haskell, and then proved to meet all of the design. The proofs are machine checked for correctness.

Then they re-implemented each function in C and assembler manually (by hand), while proving that this re-implementation (refinement) is equivalent to the Haskell implementation.

Whenever a change is made, they followed this process over again. I.e., a design change means another implementation in Haskell, proving that against the design, then making the corresponding manual change in C/assembler, then another refinement proof. Basically a lot of work over a couple of years.

The assumptions are that the C compiler, assembler, proving tools and hardware components are all bug-free. Of course they're not... but because the team is able to prove the C/assembly implementation against the original design, they can have an extremely high confidence of the system's behavior, which includes certain security guarantees.

[SIGHUP]

Sounds like the QA department at the company I use to work for. "It's secure in theory? Trust us?.

[jaguar717]

"Here grab me in a chokehold, I learned this move to get out of it every time. Can't fail, always wins."
...
"No not like that, you have to put your hand there. No you're doing it wrong, grab me like this. You have to move your other hand for it to work, then I win EVERY time."

[powersville21]

LOL jaguar. Nice one.

[SlimGem]

@ jaguar717,

Thanks for the chuckle.

[EvanSei]

kernel is always secure...... except when it's not (but I promise not to tell)

[pentest]

Proving an algorithm or design is secure is one thing. Proving that an implementation is secure is something else entirely.

Take encryption, most of the algorithms are provably solid, it is the implementations that cause the flaws.

[Seaspray0]

And considering this is just the basic core, there would be alot of implementing to bring it up to the caliber of a modern OS. Even so, I do like the idea that someone is attempting this.

[mbenedict]

They proved the implementation is secure, not just the design.

[pentest]

"They proved the implementation is secure, not just the design."

Not likely, as that is nearly impossible for all but the simplest implementations. I haven't seen enough to justify that claim.

[mbenedict]

So maybe you should actually take a look at what they did, rather than speculating on what you obviously don't know.

The team proved their C+assembly implementation meets the validated design.

[Chibiabos]

This article is very badly worded. "Prove it is secure" tells me its going to "prove" it is secure. If it were a viable test, it would "Test the security" or "Prove whether it is secure or not." If you seek to prove a hypothesis instead of testing the hypothesis, your "test" is inherently flawed and in violation of the scientific method.

[mraardvark]

The article indicates the proof is mathematical and not through the empirical scientific method. While you never truly prove a positive through the scientific method you can mathematically. The two are not the same.

In the inherently mathematical realm of computers, such proofs could end up being really important. It doesn't rule out, as pentest mentioned, the implementation being botched with coding errors, problems with the hardware, and most importantly, user error.

[onoropu]

"While you never truly prove a positive through the scientific method you can mathematically."

Prove it!

[lordmorgul]

The less a piece of software is capable of doing the more secure it can be. A microkernel is not very functional. 'Proving' the absolute security by black box testing of a fully functional monolithic kernel is a whole different ball game. I'm sure this is useful and productive research, but it is just a small step toward helping software developers design correct code in the first place in my opinion... because it might be possible to do better black box testing of portions of a monolithic kernel in this fashion.

[Dango517]

Perhaps, perhaps not, When speaking of absolutes the phrase Mathematical Law's must be applies. I do not believe we'll be seeing any Noble Prizes handed out for this effort, Years of patient testing will be needed to see if this actually is a breakthrough or just more garbage going in, to bring more garbage out. It must hold up under the "scale" of advances complex systems.

No guarantee C is any good at absolutes, by the way. Only binary code is absolute but must work within hardware that can have errors in design, manufacture and operation

Yes, computing is a mess but much of this is human error and the lack of testing methodologies Administrators, managers and coders all have a hand in the mess it has been, is, and will become.. I suspect many, many more years of patient striving before we'll have absolutely reliable software perhaps decades or more. Maybe it will never be achieve because perfection is only an illusion.

[inachu1]

It may prove the kernel is rock solid but then this is where hiring managers hire sloppy code junkies who never update their own code and introduce lots of bad code no matter how solid the core.

Sometimes they will even rely on branch of code that has known holes as to retain compatibility. It is at this point the managers need to fire the entire staff for a broken branch of code.

[alegr]

But what was their definition of "secure"? Does that just mean it never crashes? How about information disclosure? Does their kernel include access control?
It may be possible to formally prove a small microkernel. But as soon as you built the whole system, it becomes much more difficult.

[alegr]

Wow! 8700 lines of C code! That's not much. So far, there's been very little (if any) vulnerabilities in "microkernel" part of modern kernels - Linux and NT. So what's the big deal?

[James Anderson Merritt]

Ya gotta start somewhere. I remember when the profs at Cal asked us poor CS students to earn our A's by proving code snippets correct by hand (back in the early days of "software engineering"). I could see the ultimate value in the ability to prove larger systems; at the time, however, I didn't see how the effort to do so could be practical. Now, 30 years later, we have more experience, and we can get the machines to do a lot of the grunt work for us, so we are -- if this press release is to be believed -- able to prove larger, more complex components correct. I think resonances of Goedel's theorem apply here: We will always be able to create systems of such size and/or complexity that they will defy our formal methods of proof. But perhaps we can extend and expedite those methods to the point where a broad range of very useful and important systems can be proven correct.

Of course, being "proven correct" against a design that itself is poorly understood or even faulty guarantees little. I would be very interested to see what the present methods of proof can determine unequivocally about the general characteristics of a particular example of software: What does "secure" mean, for example, and how "secure" is the software in that context? I hope more details of this exercise will emerge as time passes.

[StoshNick]

"Researchers prove kernel IS SECURE" != "is free of many classes of error"

Some might claim without offering real empirical evidence that there is a relationship. None will be able to give you a numeric formula that expresses said relationship.

Remember when it was at least a challenge to spot the market-speak B.S. artists?

[onoropu]

"No amount of experimentation can ever prove me right; a single experiment can prove me wrong." ? Albert Einstein