New list member Mike Jolley

[Gernot Heiser]

>>>>> On Fri, 30 May 2008 21:58:41 -0500, Mike Jolley <mikejolley at sbcglobal.net> 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 http://l4hq.org .

Re your specific questions: OKL4 supports capabilities as of the 2.1
release (see http://wiki.ok-labs.com/). It is evolving towards the
high-security seL4 API, which includes user-level control over all
kernel resources (see http://ertos.nicta.com.au/research/sel4/).

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
http://ertos.nicta.com.au/research/l4.verified/).

Gernot