Hi all,
I'm new to this mailing list but I've done a little study of the source code, history, and other things surrounding Pistachio and L4-Hurd. My knowledge of L4 is very limited.
I have a goal of a drop-in Linux replacer built on much better technology, such as L4 or the kind of work being done at VPRI. I have a rough design for such a thing but a lot of major pieces are missing.
On the other hand, a totally new (to me) system with enough apps to get me through the day would be good too. The system I'm currently looking at is Coyotos, which is based on EROS and KeyKOS. These systems feature capability security, and I read somewhere that L4 was designed with this in mind. I can't find much info about that.
I'd appreciate any information about any of this that seems relevant, even if it has nothing to do with any specific thing I've mentioned. If this list wouldn't be interested in what you have to say, you can email me privately at mikejolley@sbcglobal.net.
Thanks a lot,
Mike Jolley
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
l4-hackers@os.inf.tu-dresden.de