World's First Formally-Proven OS Kernel

An anonymous reader writes "Operating systems usually have bugs — the 'blue screen of death,' the Amiga Hand, and so forth are known by almost everyone. NICTA's team of researchers has managed to prove that a particular OS kernel is guaranteed to meet its specification. It is fully, formally verified, and as such it exceeds the Common Criteria's highest level of assurance. The researchers used an executable specification written in Haskell, C code that mapped to Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system." Does it run Linux? "We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well." Further technical details are available from NICTA's website.

Comments

The Amiga Hand?

[johannesg]

The Amiga Hand was the boot screen, not an error screen. You're thinking of the famous Guru Meditation.

Besides, who says that the Amiga kernel did _not_ meet the specifications? Have you read them? Does it mention "crash free" anywhere?

The Haskell code is called a "specfication", but if it is Haskell code, surely it should count as a _program_ already? How can you prove that that program is bug-free? How about conceptual bugs?

Was the toolchain verified? How about the hardware on which it runs?

What overhead does this approach have? Are the benefits worth it?

I'm not saying this is all bullshit, but it looks like me that they are pointing to one program, calling it a "specification", and then demonstrating machine translation / verification to a similar program. I'm not sure if I buy that methodology.

Re:The Amiga Hand?

[TheCycoONE]

Well the typical bugs that affect C programs, like buffer overflows, using a dereferenced pointer, etc; along with common mistakes made in procedural programming in general like off-by-one errors are much less likely to come up in a functional language like Haskel. In a lot of cases Haskel code is simply a LOT shorter and easier to read than it's C/C++ counterpart which makes it much easier to find a problem; not much harder than finding the problem in a spec on paper.

So, no I don't think it guarantees anything, but it's a lot better than C code on its own.

Re:The Amiga Hand?

[Tom]

How can you prove that that program is bug-free? How about conceptual bugs?

Formal verification does not tackle conceptual bugs. What it does is prove that the implementation conforms to the specification. If your specification is false, then it is false, but the implementation will correctly implement the false behaviour. In other words, this checks whether the house and the building plan are identical. If the plan has a window where there shouldn't be one, then that window will be there, because it's on the plan.

What overhead does this approach have? Are the benefits worth it?

RTFA. The amount of work required is staggering (four years, 200,000 theorems to prove) but since it's a verification of code, not additional testing code, there is zero overhead when the system is running.

OK, you had me going there for a while...

[pedantic bore]

This is a nice accomplishment, but L4 is such a minimal kernel that some folks argue that it's not even a microkernel. It's a picokernel.

It's a lot easier to get the kernel right when it only has twelve entry points...

Re:spec?

[kamatsu]

1) L4 is a microkernel. You have no idea what you're talking about. If L4 works, then you could apply similar principles for all the other servers that run in kernel space.

2)This is the largest formal proof ever done in this sort of field. Seriously, the results are not immediately useful, but it's a good start.

Disclaimer: I have worked at NICTA in the past.