Re: L4.sec
"Jonathan S. Shapiro" <[email protected]>
| Newsgroups | gmane.os.hurd.l4 |
|---|---|
| Message-ID | <[email protected]> |
On Fri, 2007-06-08 at 00:12 +0200, Marcus Brinkmann wrote: > At Wed, 6 Jun 2007 18:24:33 +1200, > "Shams" <[email protected]> wrote: > > > > Hi, > > > > Has anyone reviewed OKL4 for usage with Hurd? > > http://www.ok-labs.com/technology/ > > As far as I know this project is based on the seL4 work from NICTA[1]. > seL4 is a cross-over between EROS and the previous L4 generations: The > mapping paradigm of L4 is preserved, while kernel object semantics > resemble EROS in some details. I believe that seL4 and L4.sec are independent projects. Both have borrowed elements from EROS and (of course) from previous L4 generations. shap > > [1] http://ertos.nicta.com.au/research/sel4/ > > It's an interesting mix, with some things good and some things > uncertain. Definitely a relevant project, but practical value of the > implementation to us is unclear to me. The focus is also very > different (formal verification, embedded systems). Yes. seL4 is very focused on embedded systems. It is also very disturbing that they have borrowed greatly from the open community, but the majority of their results are proprietary. shap