Could someone with expertise in this area share what is really meant by "end-to-end proof of implementation correctness and security enforcement", and the practical implications of it? The words suggest that the kernel is 'proven' to be absolutely secure, which obviously is false (and I don't think the authors are trying to make that claim). So what are the precise implications for confidentiality, availability, and integrity?
Source: I have worked at NICTA, with the seL4 team, on the seL4 project, I've seen the seL4 source code and am (was?) a primary author of the user manual.
What they mean by this is that they have specified certain properties at a high level in a logical reasoning language they call HOL. These properties are things like the kernel will never reference a null pointer, or, the kernel will always run the next runable thread, or no application can access the memory of another application, or, a capability invocation will always terminate.
They then wrote a runable version of the kernel in Haskell (a purely functional language) and they have a mechanically checked mathematical proof that the Haskell code implements these features/properties. They then wrote a (nearly entirely) C implementation of the kernel and, under a relatively small set of preconditions, proved that the the C code exactly (no more, no less) implements the Haskell code, which implements these correctness and security properties.
A nasty side effect of this effort is that the C code is very strange, since it is more or less translated Haskell code, and the kernel code must necessarily be VERY small, about 10,000 lines of code, which is practically nothing for an operating system kerenl (it is a micro-kernel in the truest sense of the word). Another side effect is that the API bears almost no resemblance with "previous" versions such as OKL4.
I can't answer all of these questions authoritatively, as I have more of a systems focus than a formal methods focus, but I can hopefully point you in the right directions. The various published papers and final release will be the right places to find all the authoritative answers.
1) Why not use the Haskell version?
The Haskell version was (is?) "executable", but it ran only against a hardware simulator, never against real hardware. Haskell has a complex runtime which is not (easily) suitable to run directly on Hardware (although one student I worked with did port a subset of the Haskell runtime to work on top of seL4). Using Haskell directly would be slow, and would require the researchers to prove the correctness of the Haskell runtime implementation as well which would be a huge amount of work.
2) What did you use to check the haskell version? I was not directly involved in this. I believe the Haskell used to write the kernel was a subset of the language, they call "literate haskell" which was used to both implement and specify the kernel. This was somehow minimally translated into a dialect of Isabelle called HOL.
3) What did you use to check that C implements what haskell implements?
A similar process was used for checking that the C implementation was a refinement of the Haskell. Again, a restrictive subset of the C language a tool was written to translate the C code into HOL (I think). I remember the team lead arguing that the way the C implementation was checked, both the code itself and the translator could be checked for bugs.
AFAIK, The tooling was almost all custom except for relying on Haskell and the Isabel theorem prover. The group had a lot of experience for building and releasing the OKL4 kernel so a lot of the dirty work was already done as well as an excellent "Advanced Operating Systems Course" which whips and tortures undergraduates into systems engineers and ideally PhD students. :-)
I have already seen the approach "Lets design this in haskell and write production code in C" for http://cryptol.net/, but due to limited scope (mostly functions of several hundered bits input and output as customary in crypto-primitives), they were able to check that the implementation adheres to specification automatically. The aim was to allways know that the c code does what it is supposed to, so that programmer can focus on mitigating side-channel attacks :)
I wonder if something similar would be applicable to writing the micro-kernell.
