On Fri, 30 May 2008 21:58:41 -0500, Mike Jolley mikejolley@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