World's First Formally-Proven OS Kernel 517
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.
The Amiga Hand? (Score:5, Interesting)
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.
Provable? (Score:2, Interesting)
I thought any sufficiently complex system was impossible to prove correct.
Godel's Incompleteness Theorem? (Score:1, Interesting)
As a once (very long ago!) C.S. major, I'm curious to know how they got around Godel's Incompleteness Theorem. While their system is certainly not "complete" if someone can explain (in advanced layman's terms!) what they left out and how that allowed them to formally prove the correctness of their kernel, it would be much appreciated. (Is it because, as an AC wrote, the spec was written in C? Does this "hide" the parts which are unprovable?)
Re:The Amiga Hand? (Score:4, Interesting)
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:Godel's Incompleteness Theorem? (Score:2, Interesting)
you dont have to "get around Godel's Incompleteness Theorem". (from wikipedia:): "Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory". it says "a statement" not "every statement". So, you can make formal theories where a lot of statements are provable, including a large class of computer programs.
Re:The Amiga Hand? (Score:5, Interesting)
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... (Score:4, Interesting)
It's a lot easier to get the kernel right when it only has twelve entry points...
It's paravirtualization (Score:3, Interesting)
Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.
Paravirtualization is where you modify a kernel so that it can run on something other than "bare hardware". Often in this situation you call the kernel that *does* run on bare hardware the "hypervisor" to distinguish it from the Linux (or whatever) kernel running on top. In this case Linux is running on top of their L4 kernel as a userspace program - instead of accessing parts of the hardware to get its job done it uses L4 system calls. This is basically the same as what Xen does, with L4 taking the role of the hypervisor. Researchers working on L4 have been playing with Linux-on-L4 for many years - longer than Xen has been about, AFAIK.
One nice trick you get, in this case, is that you have the ability to run Linux programs on your nice, formally-proven microkernel. But alongside that you can still run programs *directly* on the L4 kernel, independently of Linux (or with some controlled interaction with it). So, say you have some untrusted code you want to sandbox - you can run it directly on L4, which (now) has proven security properties. Or perhaps you have a crypto app which you want to isolate from Linux in case a root exploit leaves it vulnerable - you can run it directly on L4, outside Linux. You could potentially do similar things for programs that need realtime guarantees - let normal applications get scheduled by Linux's scheduler and realtime apps run directly on L4.
Basically, having L4 there is giving you an ability to start other "virtual machines" running paravirtualised OSes or high assurance applications. It's always been part of the goal that because L4 is simpler than Linux you get to have high assurance that it'll do what it's supposed to. Now a derivative has been formally proven the guarantees could potentially be even better.
The TUD:OS demo CD website has some interesting information about a real-world system that mixes the ability to run (multiple) Linux virtual machines, plus isolated secure applications, all under a security-oriented GUI. It's a pretty cool demo and you can run it as a LiveCD: http://demo.tudos.org/ [tudos.org]
Re:slow peice of crap (Score:1, Interesting)
most modern languages attempt to get speed boosts by abstracting-away low-level stuff and providing mechanisms to specify or ensure the exact constraints of a system, so that optimizations can be made.
C still gets all its speed boost from having no abstraction, forcing the programmer to hand-optimize everything, or to format code in such a way that the compiler can make a few sloppy guesses about when optimizations should be made (the "can be made" thing isn't really worth mentioning, since C doesn't allow enough type-constraints to let the compiler make anything resembling an intelligent decision, so all optimizations are pretty much "does this get used this way right here? No? Okay then, I can do this...", always lowest-common-denominator stuff- pretty much just glorified macros ("I've seen that pattern before, You seem to be looping through every element of an array and copying everything.. I'll just change that to a re-implementation of memcpy for you...")
Low-level optimizations and hand-optimizing things will only go so far- yeah, we can all just switch to assembly and get a minor speed-boost by hand-optimizing everything, but nobody does that (for speed) anymore. Eventually, being able to say "This loop is safe to run in parallel" or "just give me the first match, I don't care how you do it", is going to be faster than "loop through this. I've given you all the pointer offsets in advance, so you can skip a dereference step!" or "Let me tell you exactly how you should find a match...."
Re:spec? (Score:2, Interesting)
I'm not going to go into a lot of detail here, but the common criteria defines 7 levels of assurance; EAL 1-7. EAL 1 equates to no robustness. EALs 2-4 equate to medium robustness. EALs 5-7 equate to high robustness. An OS, or in the case of the kernel mentioned on the home page a hypervisor, is evaluated against a protection profile. The protection profile is the spec asked about by the original poster. I believe there is only one protection profile, applicable to an OS or hyperviser, that has been evaluated to high robustness - the separation kernel protection profile (SKPP). Generally, when an OS is evaluated against a PP, it is proven to meet at least the minimum requirements of that PP. Or, another way to look at it is, it will be proven do everything it says it is going to do and nothing else.
An OS/hyperviser is evaluated. The OS/hypervisor + applications + hardware is accredited. The OS/hypervisor + applications + hardware + installation is certified.
As an interesting side note, there is a protection profile that evaluates to medium robustness which specifies an OS on a computer not connected to a network in an enclosed room with an armed gaurd standing at the door. WinXP has been successfully evaluated to medium robustness against this PP.
Re:Give me six lines of code... (Score:2, Interesting)
In PHP I once had a bug in the whitespace of a comment. When I left the /* and */ away, and the comment just stood there as if it were code, it worked.
Go figure...
Nested comments maybe? If you hadn't noticed the outer comment markers, you'd get something that "didn't" work with the inner markers in place and "did" work without.
(In PHP, attempting to nest comments leads to the second '/*' being considered as enveloped by the first '/*' and the first '*/', leading to the second '*/' being flagged as erroneous, and the interpreter bailing out)
Re:spec? (Score:3, Interesting)
actualy it's both.. cosmic ray's flipping bits is a concern.. or disrupting clock cycles.. there is a reason they use slower larger circuits in long term space applications..
Re:spec? (Score:3, Interesting)
The study of the halting problem taught us that certain categories of algorithms cannot be formally proved to do certain things. Work on incompleteness tells us that we know algorithms must exist that fit that category.
The question, really, is whether the algorithms in and design of operating systems can be done in such a way that we don't run into incompleteness and halting-problem issues within the constraints of what we are trying to achieve
And the answer in this case is pretty certainly "Yes, we can"; the tasks you can't do without running into halting or incompleteness issues are pretty esoteric and well outside the sort of thing an OS kernel would sensibly be called on to do.
Re:spec? (Score:2, Interesting)
I worked as software engineer on avionics. The device I wrote for had a 486 chip and was basically the GUI for other avionics such as navigation and communication. It used a bunch of military and avionic standard protocols to communicate to the other boxes. I started coding for it in 2000 and at time it was just updates, new features and new boxes to integrate. However, they were on their way to porting this to PowerPC chips and using TCP/IP to a scalable multiple processor/box approach instead of a master/slave in two 486 boxes. The port to PowerPC also had forethought to write code that code be modular since the endian and bit size of the data had to be changed so code was was devised to know which architecture was being used for data.
The main reason for the port to PowerPC was the lack of 486 chips for new hardware for retrofitting other aircraft. At this point, they maybe looking for a new chip to replace the PowerPC.
Re:spec? (Score:3, Interesting)
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.
Re:Who proved the proof-checker? (Score:2, Interesting)
I'm not saying it's impossible, just that it's *much* harder to understand than simply writing it recursively.
Let me put it this way... suppose in C++ you have a template instantiation defined dimension matrix...
In order to do operations on the matrix, you have to iterate through an arbitrary number of dimensions, then loop over (a subset of) the length of the matrix in that dimension. It's like a for loop inside a for loop, but the number of for loops deep has to be *runtime defined* (well, in my case template defined, but you get the idea). Without recursion you end up either writing gotos, or some other funky math where you determine the overall size of the n-dimensional matrix (dimensions multiplied together) and then loop through that index, and figure out the actual n-dimensional coordinates as you go (messy).
Here it is in code...
template<typename OpType>
inline Array& eval(OpType op, IndexType index = IndexType(),
size_t dim = 0) {
for(size_t i = 0; i < extent(dim); ++i) {
index[dim] = i;
if(dim == Dimension - 1)
operator()(index) = op(index);
else
eval(op, index, dim+1);
}
return *this;
}
where IndexType is some vector unsigneds of size Dimension, extent is a member function that returns the size of the array in that dimension, and operator() retrieves the value at the given location.
This is a (modified for clarity) member function of a class I have called Array, that has template defined dimension. I'm filling the Array by calling the passed in function on every location in the Array, and assigning the result to the location.
You *can* write it without recursion, but it's even more confusing than what I wrote.
There are probably better examples of exponential time algorithms that are clearer, but they make my head hurt.
By the way, at my old job, our simulation had to interpolate lots and lots and lots of experimentally gathered data in big tables (like an 11 dimensional table for infrared signature data). Writing an arbitrary dimensional interpolation library was the *simplest* option :)
My experience with formally proven OS in the 80's (Score:3, Interesting)
I am aware of at least two instances of operating system kernels that were built in the late 1970's / early 1980's using formal proofs of correctness. I will talk about my experience with one of them.
One of them, produced in the late 1970's was a kernel designed for a specialized environment. This kernel/OS was a reasonably functional kernel complete with multiprocessing, time-sharing, file systems, etc. Unfortunately while the formal proof for this kernel was solid, the axiomatic set on which this formal proof was based did not perfectly match its operating environment. This mismatch proved to be fatal to the OS security.
This formally proven OS took years to create and prove its correctness. Those who developed and maintained the OS were very proud of their work. There were plans underway to create a commercial version of their work and to market it through a certain hardware vendor on which their OS ran.
When I was a student intern working for the organization where that developed this OS worked, I worked in their OS environment from time to time. I came in from the outside where my OS experience was with a wide variety OS' such as MVS, NOS, KRONOS, TOPS-10, RSTS/E, VMS, Multics, and Unix (5th/6th/7th edition). I had enough experience in jumping into new OS environments that I felt comfortable as a user in this one, even though it was unusual.
An important point to observe here is I was one of the first people who enter this OS environment from the outside. I was not steeped in the development world of the OS. I brought with me, ideas that differed from the OS developers. As a young student, I believed that the OS should work for me instead of getting in my way. To help come up to speed, I ported over my collection of OS-independent tools and soon began coding away on my assigned tasks.
Then one day, working within my OS-independent tools, something very odd happened. By mistake, I did something that produced an unusual result. I quickly realized that something was very wrong because the result was "impossible" according to the formal proof of OS correctness. Under the rules set down by my employer I immediately contacted the appropriate security officer and the next thing I knew, I was in a long sequence of meetings with people trying to figure out what in the hell happened.
In the first meeting after my mistake, I learned that I had been reassigned to a new team. I was assured that I was not being disciplined, far from it: I had made a number of people very happy and they moved paperwork mountains to move me into their team. This team was given a task of attempting to repeat my previous "mistake" as well as to discover if exploits that are more general were possible against this OS. We were assigned to work âoeundercoverâ as developers under test/QA installations using this OS. In the end, the team was successful in discovering a much more general form of the OS hole I accidentally found.
What went wrong with the OS formal proof? Well the mapping from the formal logic world to the real world of hardware, physics, people, and the environment was flawed. In other words, when you added in the "real-world", the proof was incomplete. Attempts by the OS developers to expand their proof to address the "real-world" only produced a set of inconsistent theorems. I believe the OS project was abandoned after the OS developers failed multiple times to expand their formal proof to deal with âoereal-worldâ environments.
During this experience I was introduced to two "Security Camps": One, "the absolutists" as they called themselves, included people who worked on this formally proven OS. The opposing camp called the