There is good information on the web now about seL4 (too). There is a chronological list of papers at the bottom of this page. “Documentation”. Here are a few insightful remarks on the system. Here are my notes on the “seL4 Reference Manual API version 7.0.0”. This is actually an introduction to a Haskel model that was used in some sort of formal proof. This is another document from 2015 by the same title that does not speak much of Haskell. To be analyzed: Running the Manual relates kernel semantics to a particular Haskell program. Formality video & voice
seL4 is like Keykos in that the native language (by which users define object behavior) is machine code; bring your own compiler. (e.g. Rust or C).
In some seL4 papers programs talk to the kernel about CNodes whereas in Keykos they talk to the node. seL4 speaks of a CNode as being a kernel object, but not something to be invoked. Once Keykos (Gnosis) spoke that way too. I think this is a distinction without a difference. Keykos largely unifies kernel objects and objects defined by user code as seen by the user of those objects. (Section 2.2 of “The Manual” uses Keykos terminology where you can invoke either a kernel object or another ‘thread’ much as one Keykos domain invokes another. I suspect that they can indeed virtualize kernel objects.) I think that in some seL4 literature all objects are kernel objects. Using this manner of speaking we call upon services of another thread by invoking an endpoint (a kernel object) to which the other thread is listening. N.B. In these papers “TCB” refers to not “Trusted Computer Base”, but “task control block”, rather like the Keykos domain. Reading further makes me think seL4 is not so much different than Keykos in this regard.
As they describe seL4_Reply() they say that the invoked key is the reply capability generated by the seL4_Call(). It is the cap found in the special slot of the TCB which is normally the reply cap. Keykos invokes kernel and non kernel objects by composing a message and sending it using a key as an address. Code can copy from the reply slot of its own TCB.
seL4 slots may not hold a capability but Keykos slots always hold a key. Keykos number keys designate nothing unless you want to say that they designate a number; a slot with a number key is merely a convenient place to keep some information. That convenience is very substantial as the alternative would often seem to be a page to hold a small integer. Perhaps seL4’s page analog is cheaper.
The formal proof may be important. What is important about it is not the proof but the nature of what was proven! Those ‘specifications’ were about capabilities. The same project for Linux would fail. While bugs in the Linux code are often vulnerabilities, gradually fixing them is feasible. There are vulnerabilities in the Linux specifications which remain. Large bodies of code rely on the nature of these flaws.
Wikipedia speaks of seL4 “exporting the management of kernel resources to user level and subjects them to the same capability-based access control as user resources”.
The nature of the proof.