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.
spec? (Score:5, Insightful)
but is the spec useable ? bugfree ?
Re: (Score:2)
Re: (Score:3)
Re: (Score:2)
Re: (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:4, Insightful)
Re:spec? (Score:5, Informative)
It only means it meets the spec, not that the spec is correct ...
It does not mean that the faulty or erratic hardware cannot crash the system
It does not mean that other programs cannot crash and lose your data ...
It does not mean that buggy device drivers can make your system unusable
It does not mean that the system is perfect, only that it will always do what it is supposed to ... which may not be what you want ...
Re: (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: (Score:2)
but is the spec useable ? bugfree ?
And does it match the user or system needs ? And how easily can it be modified to cover new needs ?
Re:spec? (Score:4, Insightful)
If you pass the customer a mix of water, flour, yeast, eggs and sugar and the customer says "That's not cake, it's not acceptable".
And you then say - "But we meet the cake spec we agreed on, so by that definition it's cake, you have to pay us".
Sure you can go sue the customer and force them to pay you the full sum, but unless most other people agree the customer has just been way too fussy, you might have fewer customers in the future.
Re: (Score:2)
first write it in a formal language, then in a functional language.M
I don't believe Java fits either of those.
Re: (Score:3, Funny)
In your case? I think the second word is "*WHOOSH*".
Re: (Score:3, Informative)
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 -- after all, we aren't trying to achieve the impossible, just
Re: (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: (Score:3)
...and somewhere between halting and incompleteness, Omega sits, mocking us.
Thank goodness (Score:2, Insightful)
Re: (Score:2, Insightful)
As opposed to programming languages that aren't logic-based? What separates Haskell, Ocaml, Lisp, Scheme, etc. from others is that they are functional programming languages, as opposed to imperative-based languages like C.
Both use logic, just in different ways.
Re: (Score:3, Insightful)
You know the funny thing about this whole discussion is that the OS linked to in the article is not the first. Integrity from Green Hills Software was proven correct a while ago. It is popular for safety critical stuff like flight controls for airplanes and is one of the dominant players in that niche. :)
http://www.informationweek.com/blog/main/archives/2008/11/green_hills_sof.html [informationweek.com]
And what is truly amusing about following this argument, is that Integrity is written in C.
Although I can see that you're amused, what you're saying is false: Integrity is not formally proven correct, it only has some amusing but mathematically irrelevant industry certificate.
Re: (Score:3, Informative)
You're conflating two different concepts. Common Criteria Evaluation Assurance Level focuses on security while this test focuses on complete mathematical provability IOW, can it be mathematically proven that the kernel meets all of its specifications and that the compiled kernel is exactly what was specified in the source code? CC EAL focuses only on security aspects.
Furthermore, a system that was specified as being completely secure[1] would, in theory, be equivalent to a EAL 7, not merely "6+".
[1] I mea
Re:Thank goodness (Score:4, Insightful)
People are starting to see the value of this. Also of programming in logic based languages like Haskell, ML etc.
People have seen the value of this since the first days of programming. In fact, the value is so enormous that no one can afford it... And they have just finished proving that first few lines of code they wrote. In another five decades they hope to be able to have Notepad proven and ready to run so you can actually get some work done!
Re: (Score:2)
In another five decades they hope to be able to have Notepad proven and ready to run so you can actually get some work done!
Progress has been slow, mainly because for most of the last 20 years, they've been hung up trying to formally prove that a newline character looks like a rectangle.
Re: (Score:3, Insightful)
Name the logic that C is based on, then.
C may be "logical" in a colloquial sense. It's not based on a formal logical calculus.
Do you even know what the hell you are talking about?
Re: (Score:3, Insightful)
Re: (Score:3, Insightful)
Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.
C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.
Re: (Score:3, Insightful)
Re:Thank goodness (Score:4, Insightful)
It's a paradigm, technically. Although Haskell isn't a logic language, it's functional. Prolog is logical, and nigh useless for most applications.
No, it's just more difficult to write the program for most applications.
IMO, it's because it's more difficult to precisely articulate the problem and method (for Prolog) than to work through the solution (for an imperative language).
Amiga Hand? (Score:5, Informative)
Or do you mean the "Guru Meditation Error"?
Re: (Score:2)
I prefer SACF interrupts, much more exciting
Re: (Score:2)
Amiga 1000s and early Amiga 3000s had the kickstart on floppy too -- you would first get a hand/floppy image with the word "Kickstart" on it, upside down of course, and only after that would it ask for "Workbench", possibly with a version number (which inexplicably wasn't written upside down on the floppy itself. Sloppy).
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.
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:The Amiga Hand? (Score:5, Informative)
The missing word is formal.
They use a formal specification [wikipedia.org], which is then formally verified [wikipedia.org].
The overhead? It took something like 5 years for a 10,000 line program. The benefit is if the specification is right, the program should be right.
Other questions are answered in the FAQ linked in the summary and this page [nicta.com.au].
And if the spec has bugs the program will have bug (Score:2)
So who gets to prove the spec then?
Re:The Amiga Hand? (Score:5, Insightful)
We'll have to prove the specification does what we want, then. Of course, then we have to make sure our conception of what we want is right...
Personally, I think it's elephants all the way down.
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.
Give me six lines of code... (Score:5, Funny)
"If you give me six lines of code written by the most diligent of programmers, I will surely find enough in them to crash the OS" - Cardinal Ritchielieu
Re:Give me six lines of code... (Score:5, Funny)
Every program contains at least one bug, and can be shortened by at least /old, I know.
one instruction. By induction, every program can be reduced to a single
instruction which doesn't work.
Re:Give me six lines of code... (Score:5, Funny)
HACF?
And that instruction is... (Score:2)
And that instruction is...
HCF [wikipedia.org].
Re: (Score:2)
Excellent line, but I don't think it really holds up. Certainly a literal reading could be a nontrivial problem, perhaps impossible, but even just assuming the general idea that app-level code can always be used to crash the underlying OS seems fraught with troubles.
Re: (Score:2)
I guess you missed the cultural reference...
Re:Give me six lines of code... (Score:5, Funny)
/*
*
*
*
*
*/
Apps running on top will crash... so (Score:3, Insightful)
Re:Apps running on top will crash... so (Score:5, Informative)
> Even if we have a perfect kernel, it won't insulate us from bugs in the
> software running on top of that kernel, so do we really gain much?
Since a kernel crash kills all your applications and background processes, kills your network connection, requires you to reboot, and can scribble anywhere on the disk, yes.
Re: (Score:2, Informative)
Well, kernel bug brings down whole OS and all the applications running top of it. But the kernel is usually most secure and stable. Most errors comes from drivers.
http://www.usenix.org/publications/login/2006-04/openpdfs/herder.pdf [usenix.org]
And that is the problem with the monolithic OS's. One bug in the driver or any other part of the OS, brings it down. But even it is about monolithic OS, it can be as secure as microkernel-based OS's like Hurd, Minix or NT.
And I believe that the star of the next 10 years will come
Re:Apps running on top will crash... so (Score:5, Insightful)
Yes, it gains you a lot.
Firefox crashing means your userland memory is fucked up and can't be trusted anymore. No problem, kill it, clean it and restart the application.
A kernel crash leads to undefined behaviour on the ring 0 level. You don't want that, it's where root exploits live.
Furthermore, we have a lot of really, really strong kernel-level security extensions, like SELinux, whose only two vulnerable spots are kernel-level exploits and weak security policies. If you can remove one of them, you've done a lot to improve security.
Re: (Score:2)
If your filesystem task running on top of a proven kernel has a bug, it can still corrupt your disk.
Knuth on proven correct: (Score:5, Insightful)
"Beware of bugs in the above code. I have only proven it correct, not tested it."
Who proved the proof-checker? (Score:4, Funny)
Re: (Score:3, Insightful)
If he were being honest, he would say that recursion is a just convoluted, unnecessarily confusing method of doing iteration
Some would say that iteration is just a convoluted, unnecessarily confusing method of doing recursion.
For example, try iterating over all the nodes in a tree without using recursion. It's doable, but more complicated and error-prone than the recursive method.
Provable? (Score:2, Interesting)
I thought any sufficiently complex system was impossible to prove correct.
Re: (Score:2)
Well, one thing you can do is cut and paste your code into the specification. Now your code perfectly matches the specification---and is coded as specified.
They seem to be doing the same thing, except going about it some backwards way.
Re: (Score:2)
Well, one thing you can do is cut and paste your code into the specification. Now your code perfectly matches the specification---and is coded as specified.
That would be doing it backwards...
They seem to be doing the same thing, except going about it some backwards way.
...and doing a backwards thing backwards would be the right way again.
Re:Provable? (Score:5, Insightful)
I thought any sufficiently complex system was impossible to prove correct.
Then obviously this OS is not sufficiently complex.
Re: (Score:2, Informative)
only if you want to prove it automatically. this proof is constructed by hand, with some automatical steps in between, and then *verified* automatically. to manage the complexity of the proof, the proof is done in a more abstract formal specification language , then refined two times (haskel, C) . the correctness of the refinements are formally proven by the Isabelle system.
Re: (Score:2)
Well, there are some theoretical problems with this idea. The halting problem is trivial to prove insolvable, and it turns out that it's possible to generalise this proof and demonstrate that it's not possible to prove any complex properties of arbitrary programs. The key word here is arbitrary. You can, for example, trivially (algorithmically; the space / time requirements can be very large) solve the halting problem for any program that can be represented as a finite automaton. This includes any progr
Then a driver blows it all up.. (Score:5, Funny)
Suddenly after that, the proven kernel will be brought to its knees when someone adds a driver for an old graphics card.
But... (Score:2, Funny)
Proven? (Score:5, Insightful)
Wish I had mod points (Score:3, Insightful)
This is something that people who bang on about formal proofs conveniently forget - all it does is move the bugs from the source code to the formal specification. And if the spec is detailed enough to be useful it effectively becomes code anyway so you might just as well write the actual code and debug *that* instead.
Re: (Score:2)
Re: (Score:3, Insightful)
That this moves the bugs to the formal specification is true, but that therefore you might just as well write the actual code is an invalid derivation. Formal specification languages are designed with the idea that one should be able to reason about them in mind (be it manually or with the help of automatic/interactive theorem proving, model checking). This typically leads to a language in which systems can be expressed on a higher level, because performance issues are not important: the specification doe
Re: (Score:3, Insightful)
I don't thinks that's fair: the spec. just says *what* properties the system should have; the implementation says *how* those properties are provided. Where you can do it, denotational semantics (the spec.) let you say a lot more than you can with operational semantics (the code).
Of course, your argument also suffers from circularity: to debug code you have to have a spec. in the first place to tell you when the implementation is doing the wrong thing.
what if you made a kernel so perfect (Score:2)
Re: (Score:2)
the kernel was so perfect that it thought it was god and it condemned the rest of the OS to hell
Windows is a good example of an OS that _thinks_ it is perfect. Fortunately Microsoft's idea of hell is my idea of heaven :)
World's First Formally-Proven OS Kernel - NOT (Score:4, Informative)
Honywell SCOMP Early 1980s Was intended to me a secure front-end to Multics.
Verified by NSA et all as part of the first Orange-book A1 level certification.
For the time it was a magnificent bit of work.
Re: (Score:3, Insightful)
Re: (Score:2)
excellent news (Score:2)
This should once and for all silence the people who claim that it's impossible to formally verify any non-trivial code.
Oh, what am I dreaming. They won't shut up, but maybe now they'll die out.
Re: (Score:2)
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...
Re: (Score:3, Informative)
Microkernels provde:
L4 checks these boxes. Nanokernel and picokernel are poorly defined, emotive terms. Not reasonable criticism.
Not very useful... (Score:2, Insightful)
In addition to what's already been pointed out about formal vs. informal specifications,
1. Running Linux on top of this is no more safe than running Linux directly on the hardware--it's Linux that crashes (though not very often!)
2. Running this on a CPU that has not been formally proven is nearly useless because only part of the system has been proven, which results in an overall system that is unproven.
Re: (Score:2)
Good News and Bad News (Score:5, Insightful)
First off, as an Australian and a nerd, I am very proud.
Now.
Good news: there is now a formally verified microkernel. 8,700 lines of C and 600 odd lines of ARM assembly. Awesome.
Bad news: it took 200,000 lines of manually-generated proof and approximately 25 person-years by PhDs to verify the aforementioned microkernel.
Conclusion: formal verification of software is not going to take off any time soon.
Re: (Score:2)
At the speed commercial IT moves right now? No.
Eventually? I think it would be in the best interest of everyone to work toward making this the normal operation in CS.
If Donald Knuth wrote it... (Score:2)
he would probably say:
"Please be aware of bugs. I just proven this kernel to be correct, didn't actually run it" ;)
Great work, but... (Score:3, Informative)
...there are two caveats. One is that "executable specification in Haskell" is a bit of a dodge. It means that they have effectively verified the translation from Haskell to C, but if there are bugs in the Haskell then there will be bugs in the C as well (in fact this is part of what they've proven). They admit as much at the very top of http://ertos.nicta.com.au/research/l4.verified/proof.pml [nicta.com.au], but it still leaves the question of why this is any better than simply rewriting the microkernel in Haskell. If the benefit of a concise and abstract specification is lost, what's left?
The second major caveat is that they had to leave out some features that they couldn't verify. Most significant is that they didn't verify multi-core - by which it seems they mean multi-processor, but "multi-core" is the much hipper word. Since even laptops are multi-processor now, this limits applicability until they take the next step. With all of these shortcuts, though, if you look at the list of what they did manage to verify - mostly pointer errors and overflows - it's not clear that it couldn't have been done with a more real-code-oriented tool such as the Stanford Checker or sparse.
congratulations! (Score:2)
The kernel has now been proven to implement buggy specifications precisely!
You mean they aren't all tested like this? (Score:5, Insightful)
As someone who does not work in IT, count me as surprised that not all OSes are tested this rigorously.
Re: (Score:3, Insightful)
Linux has more than ten million lines of code. Given that they needed 5 years for 12 persons to verify ten thousand lines of code, this means verifying the Linux kernel would give an estimated cost of 60,000 man-years. So even if they got a thousand people doing nothing else but verifying the Linux kernel, it would take then 60 years to finish.
Re: (Score:3, Insightful)
That more like "not only doesn't work in IT, but doesn't know of or understand the theory". No slam, just the facts.
Seriously, the reason all OSes aren't tested this vigorously is that the time/amount of work needed to do so rises exponentially with the size/complexity of the OS. Not only does that imply the OS would take years to bring to market, but also that said OS would incredibly expensive. Worse yet, after all that time and expense, all you've actually proven is that your running code matc
Halting Problem? (Score:2)
I'm not a computer scientist, so this may be obvious, but how does the halting problem come into this? I mean, the summary suggests that you know this OS won't crash, but wouldn't a general method for proving that be solving the halting problem? I'm guessing that the answer is that they've just proved it meets the spec, and the spec cannot be proved not to crash. Or perhaps it's that they've proved that this program won't crash by a method that's not generally applicable to all problems, so they would
A truly marvelous (Score:5, Funny)
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
Re:Yeah right (Score:5, Funny)
Re:Godel's Incompleteness Theorem? (Score:5, Insightful)
Godel's Incompleteness Theorem just say(In this context) that there exists infinite many kernels that are correct but which can not be proven correct. It does not say that no kernel can be proven correct.
So they just happen to write one of the kernels that could be proven.
Re: (Score:2)
Hm I thought they proved the mapping (Score:2)
Hm I thought they proved the mapping from Haskell to C was correct, as well. At lest, so far, for the ARM version.
Re: (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 provabl
Re: (Score:2)
Re: (Score:2)
Goedel's theorem simply states that you cannot prove a system in itself, for any sufficiently interesting system.. not repeating the definition of /that/ one here. In any case, this kernel qualifies.
But that doesn't at all prevent you from proving it in a higher-level system, such as the theorem prover they used. Um, though it would cause trouble if you want to prove the /prover/ correct...
Re: (Score:2)
I think the relevant word is "can", not "has". It has the potential to do the same thing but doesn't seem to have made it that far. Provable but not proven?
And besides that, from the very article you linked to, I can spot a number of problems - such that isn't just written in one language and translated to a final, provable "one language + assembly" like the main article, but several (and a lot more than the bare minimum necessary to boot a kernel, it seems). It's kind of mid-way to what the main article
Re: (Score:2)
CmdrTaco just takes any warm body that can hit CTRL-C and CTRL-V in quick succession. FTFY.
CmdrTaco just takes any warm body. FTFYA.
Re:Sounds like automated unit test generation to m (Score:3, Informative)
Formal proofs are not unit tests. Unit tests test that certain values work correctly. Formal proofs show that the code works to the specification in all cases (modulo errors in the proof, of course). They of course cannot find bugs in the specification (which unit tests might, if they test what you thought the specification said, instead of what the specification really said).
Re:Empty promises... (Score:5, Insightful)
Most faults on most platforms are caused by hardware faults
bullshit.
Re:Empty promises... (Score:4, Insightful)
The context of your full original post does not change the fact that you claim most faults are caused by hardware, which is the specific point he was disputing.
If you have something to strengthen your claim (from your original "context" or otherwise), present it. Otherwise, complaining about being quoted "out of context" is just rhetorical posturing.
Re: (Score:2)
The article does not claim that software faults have caused plane crashes.
The article merely states: "Or, much scarier, you might be on a plane and there's a problem with the board computer."
Thus, I have proven that you have failed to understand simply English.
Re: (Score:2)
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 kern