New list member Mike Jolley

Gernot Heiser gernot at
Sat May 31 09:54:06 CEST 2008

>>>>> On Fri, 30 May 2008 21:58:41 -0500, Mike Jolley <mikejolley at> said:
MJ> [...]

MJ> On the other hand, a totally new (to me) system with enough apps to get me 
MJ> through the day would be good too.  The system I'm currently looking at is 
MJ> Coyotos, which is based on EROS and KeyKOS.  These systems feature capability 
MJ> security, and I read somewhere that L4 was designed with this in mind.  I 
MJ> can't find much info about that.  

MJ> I'd appreciate any information about any of this that seems relevant, even if 
MJ> it has nothing to do with any specific thing I've mentioned.

Generally, a good starting point for such info is .

Re your specific questions: OKL4 supports capabilities as of the 2.1
release (see It is evolving towards the
high-security seL4 API, which includes user-level control over all
kernel resources (see

The present (unreleased) seL4 prototype is fully functional, to the
degree that it can run a para-virtualized Linux system on top. It also
has formal (machine-checked) proofs of security properties, and a
formal verification of it's high-level and low-level designs (see


More information about the l4-hackers mailing list