Hello everyone, I would just like to ask about the current status or some roadmap for L4.sec? Is it actively being worked on? Reason is: I need to choose a microkernel to start working on an experimental operating system within this year I need some facts for decision-making - and I would prefer a capability-based one like L4.sec. Thank you, Ernst Rohlicek jun.
Hi, Ernst Rohlicek jun. wrote:
Hello everyone,
I would just like to ask about the current status or some roadmap for L4.sec? Is it actively being worked on?
L4.sec is (and probably will be for quite some time) an experiment that is still worked on in our group. Mainly due to maintenance and support issues the sources have not been officially released yet. Our roadmap regarding L4.sec is to continue experimenting with capabilities and user controlled kernel memory management. Some of the results we already integrated into the Fiasco kernel, which is our mainstream kernel as for now. These include kernel memory quotas, security monitor style IPC permissions (though no local names yet). Others are likely to be integrated in some form in the Nova microhypervisor, which we are currently developing in the course of the Robin project.
Reason is: I need to choose a microkernel to start working on an experimental operating system within this year I need some facts for decision-making - and I would prefer a capability-based one like L4.sec.
Can you elaborate a little on what you plan to do? Possibly, we can give you more advice on which kernel to use once we know what your plans are. The L4 related stuff that is out there is: Fiasco (TU-Dresden mainstream kernel) + L4Env which is small multiserver OS Pistachio (Uni Karlsruhe, UNSW / NICTA mainstream kernel) L4.Sec (TUD, experimental) Nova (TUD, under development) seL4 (UNSW / NICTA, Haskel implementation of an interface with similar features to L4.sec, i.e., capabilities, kernel memory management, etc.) + some commercial versions P4 (Sysgo) OKL4 (Open Kernel Labs) Best regards Marcus -- Marcus Völp Technische Universität Dresden Department of Computer Science Institute for System Architecture Tel: +49 (351) 463 38350 Fax: +49 (351) 463 38284 Email: voelp@os.inf.tu-dresden.de Web: http://os.inf.tu-dresden.de/~voelp
Marcus, At Thu, 02 Aug 2007 10:34:41 +0200, Marcus Voelp wrote:
Some of the results we already integrated into the Fiasco kernel, which is our mainstream kernel as for now. These include kernel memory quotas, security monitor style IPC permissions (though no local names yet). Others are likely to be integrated in some form in the Nova microhypervisor, which we are currently developing in the course of the Robin project.
Are these extensions documented anywhere other than in the source? Thanks, Neal
Hi, I fin interesting Nova L4, What is it about? Many thanks, Jorge On 8/2/07, Marcus Voelp <voelp@os.inf.tu-dresden.de> wrote:
Hi,
Ernst Rohlicek jun. wrote:
Hello everyone,
I would just like to ask about the current status or some roadmap for L4.sec? Is it actively being worked on?
L4.sec is (and probably will be for quite some time) an experiment that is still worked on in our group. Mainly due to maintenance and support issues the sources have not been officially released yet. Our roadmap regarding L4.sec is to continue experimenting with capabilities and user controlled kernel memory management. Some of the results we already integrated into the Fiasco kernel, which is our mainstream kernel as for now. These include kernel memory quotas, security monitor style IPC permissions (though no local names yet). Others are likely to be integrated in some form in the Nova microhypervisor, which we are currently developing in the course of the Robin project.
Reason is: I need to choose a microkernel to start working on an experimental operating system within this year I need some facts for decision-making - and I would prefer a capability-based one like L4.sec.
Can you elaborate a little on what you plan to do? Possibly, we can give you more advice on which kernel to use once we know what your plans are. The L4 related stuff that is out there is:
Fiasco (TU-Dresden mainstream kernel) + L4Env which is small multiserver OS Pistachio (Uni Karlsruhe, UNSW / NICTA mainstream kernel)
L4.Sec (TUD, experimental) Nova (TUD, under development)
seL4 (UNSW / NICTA, Haskel implementation of an interface with similar features to L4.sec, i.e., capabilities, kernel memory management, etc.)
+ some commercial versions P4 (Sysgo) OKL4 (Open Kernel Labs)
Best regards
Marcus
-- Marcus Völp
Technische Universität Dresden Department of Computer Science Institute for System Architecture
Tel: +49 (351) 463 38350 Fax: +49 (351) 463 38284
Email: voelp@os.inf.tu-dresden.de Web: http://os.inf.tu-dresden.de/~voelp
_______________________________________________ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
Hi,
Hi Marcus,
L4.sec is (and probably will be for quite some time) an experiment that is still worked on in our group. Mainly due to maintenance and support issues the sources have not been officially released yet. Our roadmap regarding L4.sec is to continue experimenting with capabilities and user controlled kernel memory management. Some of the results we already integrated into the Fiasco kernel, which is our mainstream kernel as for now. These include kernel memory quotas, security monitor style IPC permissions (though no local names yet). Others are likely to be integrated in some form in the Nova microhypervisor, which we are currently developing in the course of the Robin project.
User-controlled memory management sounds interesting -
Reason is: I need to choose a microkernel to start working on an experimental operating system within this year I need some facts for decision-making - and I would prefer a capability-based one like L4.sec.
Can you elaborate a little on what you plan to do? Possibly, we can give you more advice on which kernel to use once we know what your plans are.
Sure. I'm glad you asked - there are quite a few new microkernels out there, and even the various L4 variants are still a bit obscure to me. Generally, the goal of the experiment is to take a micro-kernel, which interacts with the hardware and provides basic abstractions for it (threads, memory, scheduling, interrupts, etc.) and get a high-level runtime environment running as directly on top of it as possible. This would be a pervasively OO, multi-language-capable, extremely dynamic one (like combining .NET and the powers of Ruby/Smalltalk/Lisp), which, yet, compiles to machine-code, so presumably is quite fast - and is already in development. The advantage would be that the system would be programmable from the bottom up in a high-level (ie. not C/C++) programming language, which is known to developers from other platforms, since any syntactic conventions would be defineable, "We write an operating system in JavaScript - or Python if you like to - or ..." (If you're interested, see http://www.piumarta.com/papers/ .) On the security side, according to my research, capability security is close to "the insurmountable security paradigm" there is - in order to protect the objects of each process properly from each other, especially since much of the OS services would be inside the same runtime. And I'd like to start this year sometime :-)
Best regards
Marcus
Thanks in advance, Ernst Rohlicek jun. <ernst.rohlicek@inode.at>
Hi, On 8/2/07, Marcus Voelp <voelp@os.inf.tu-dresden.de> wrote:
L4.sec is (and probably will be for quite some time) an experiment that is still worked on in our group. Mainly due to maintenance and support issues the sources have not been officially released yet. Our roadmap regarding L4.sec is to continue experimenting with capabilities and user controlled kernel memory management. Some of the results we already integrated into the Fiasco kernel, which is our mainstream kernel as for now. These include kernel memory quotas, security monitor style IPC permissions (though no local names yet).
What does "security monitor style IPC permissions" mean? Can it be found in current Fiasco release? Others are likely to be integrated in some form in the Nova microhypervisor,
which we are currently developing in the course of the Robin project.
Where can I find information about Nova and Robin? Are there any English documentation? Regards, Wei Shen
Wei Shen wrote:
Hi,
On 8/2/07, *Marcus Voelp* <voelp@os.inf.tu-dresden.de <mailto:voelp@os.inf.tu-dresden.de>> wrote:
L4.sec is (and probably will be for quite some time) an experiment that is still worked on in our group. Mainly due to maintenance and support issues the sources have not been officially released yet. Our roadmap regarding L4.sec is to continue experimenting with capabilities and user controlled kernel memory management. Some of the results we already integrated into the Fiasco kernel, which is our mainstream kernel as for now. These include kernel memory quotas, security monitor style IPC permissions (though no local names yet).
What does "security monitor style IPC permissions" mean? Can it be found in current Fiasco release? Yes, although documentation lacks behind a little bit. Check the IPCMon package in the OpenTC Snapshot for an example how to use it these kernel features. Primarily you can restrict the tasks to which a given task may send IPC.
Others are likely to be integrated in some form in the Nova microhypervisor, which we are currently developing in the course of the Robin project.
Where can I find information about Nova and Robin? Are there any English documentation? http://robin.tudos.org/
See the Executive summary for a progress report on Robin. A specification of Robin will be released latest in Mai 2008. Best regards Marcus -- Marcus Völp Technische Universität Dresden Department of Computer Science Institute for System Architecture Tel: +49 (351) 463 38350 Fax: +49 (351) 463 38284 Email: voelp@os.inf.tu-dresden.de Web: http://os.inf.tu-dresden.de/~voelp
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hi,
What does "security monitor style IPC permissions" mean? Can it be found in current Fiasco release?
Yes, it can be found in Fiasco. Tasks can be started in "monitored" mode which means that they only possess rights to communicate with themselves, their creators and the NIL thread. Every other IPC will raise a capability fault which is sent to a user-defined capability fault handler. The handler may then act upon this fault by mapping an IPC right to the faulting task, if it possesses this right itself. Whenever this right has been mapped, no more capabilty faults will occur until the right is revoked at a later point in time.
Where can I find information about Nova and Robin? Are there any English documentation?
Maybe start at http://robin.tudos.org/ . Regards, Bjoern - -- Dipl.-Inf. Björn Döbel doebel@os.inf.tu-dresden.de Technische Universität Dresden Tel: +49 351 463 38799 Dept. of Computer Science, OS Chair Fax: +49 351 463 38284 D-01062 Dresden, Germany -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFGuBhvP5ijxgQLUNkRAoRgAKCcc/8pDFTJf4qAcf61/D6VSMpTzwCgmn9p cTIr3gAxmG0UV+wy4ejiHQg= =fu56 -----END PGP SIGNATURE-----
Hi, Thanks for your reply. On 8/7/07, Bjoern Doebel <doebel@os.inf.tu-dresden.de> wrote:
What does "security monitor style IPC permissions" mean? Can it be found in current Fiasco release?
Yes, it can be found in Fiasco. Tasks can be started in "monitored" mode which means that they only possess rights to communicate with themselves, their creators and the NIL thread. Every other IPC will raise a capability fault which is sent to a user-defined capability fault handler. The handler may then act upon this fault by mapping an IPC right to the faulting task, if it possesses this right itself. Whenever this right has been mapped, no more capabilty faults will occur until the right is revoked at a later point in time.
Interesting, especially that I think IPC control is an obvious weakness of current L4 kernels. Is there any new l4 API specification release includes this feature? Where do IPC capabilties originally come from? Maybe there is a privileged task (roottask?) that has all capabilites? How about the performance of this mechanism - searching the communication peer from the cap list in every IPC ... Is this model only used in IPC contol or also to control other kernel resources, like memory pages, interrupts, task no ... Is task / thread creation controlled now in Fiasco? Why can I find news about changes to Fiasco? Regards, Wei Shen
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hello,
On 8/7/07, Bjoern Doebel <doebel@os.inf.tu-dresden.de> wrote:
What does "security monitor style IPC permissions" mean? Can it be found in current Fiasco release? Yes, it can be found in Fiasco. Tasks can be started in "monitored" mode which means that they only possess rights to communicate with themselves, their creators and the NIL thread. Every other IPC will raise a capability fault which is sent to a user-defined capability fault handler. The handler may then act upon this fault by mapping an IPC right to the faulting task, if it possesses this right itself. Whenever this right has been mapped, no more capabilty faults will occur until the right is revoked at a later point in time.
Interesting, especially that I think IPC control is an obvious weakness of current L4 kernels. Is there any new l4 API specification release includes this feature?
Not yet, but there will probably be one in the future.
Where do IPC capabilties originally come from? Maybe there is a privileged task (roottask?) that has all capabilites? How about the performance of this mechanism - searching the communication peer from the cap list in every IPC ...
Currently tasks that are started by roottask during system startup possess all capabilities and may map those to clients. A specific IPC Monitor works as the capability fault handler for the tasks started by our ELF loader and can be configured by the user. Performance isn't hurt that much. You only need to do the lookup once the first IPC is sent between from task A to B. Afterwards, task A possesses the communication capability and no more capfaults occur, therefore causing no more overhead.
Is this model only used in IPC contol or also to control other kernel resources, like memory pages, interrupts, task no ... Is task / thread creation controlled now in Fiasco?
Fiasco also includes a new mechanism to account in-kernel memory usage to specific tasks. What kind of control do you want for task/thread creation?
Why can I find news about changes to Fiasco?
Hopefully there will be a new Fiasco spec some day. ;) Bjoern -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD4DBQFGuJV5P5ijxgQLUNkRApdXAJ9n/aDj4a3VOLB8HjfCm9TbrGq2oQCVF+PP +6jU5jXVFnen8OnXAIX4BA== =CFkU -----END PGP SIGNATURE-----
On Wed, 01 Aug 2007 23:42:54 +0200, "Ernst Rohlicek jun." <ernst.rohlicek@inode.at> said: ERj> Hello everyone, ERj> I would just like to ask about the current status or some roadmap for ERj> L4.sec? Is it actively being worked on?
ERj> Reason is: I need to choose a microkernel to start working on an ERj> experimental operating system within this year I need some facts for ERj> decision-making - and I would prefer a capability-based one like L4.sec. If you are looking for a capability-based L4 kernel you should have a look at seL4: http://ertos.nicta.com.au/research/sel4/ Work on this is quite advanced, see for example http://ertos.nicta.com.au/publications/papers/Elphinstone_KDRH_07.pdf The API is quite stable by now and will be released shortly (the only reason it isn't released yet is that we have to deal with lawyers and no-one wants to spend their time on this ;-). There is also an executable model of the API (aka simulator) that supports running ARM binaries built with a standard GNU toolchain, so you can port software to it. That executable model should be released at the same time as the API. The commercial OKL4 microkernel is converging on the seL4 API, it presently contains simplified versions of IPC control and all kernel resource allocation is under control of a user-level policy server. It should implement a full seL4 API probably sometime next year. Gernot
If you are looking for a capability-based L4 kernel you should have a look at seL4: http://ertos.nicta.com.au/research/sel4/
Work on this is quite advanced, see for example http://ertos.nicta.com.au/publications/papers/Elphinstone_KDRH_07.pdf
The API is quite stable by now and will be released shortly (the only reason it isn't released yet is that we have to deal with lawyers and no-one wants to spend their time on this ;-). There is also an executable model of the API (aka simulator) that supports running ARM binaries built with a standard GNU toolchain, so you can port software to it. That executable model should be released at the same time as the API.
That is good to hear - I thought seL4 would take a longer time to a first (even if alpha/beta) release. I'm looking forward to it! In the paper, there is a mention of a "Coyotos" project by Mr. Shapiro, also striving to create a high-security microkernel. Where would you see seL4's strengths compared to Coyotos and vice versa?
The commercial OKL4 microkernel is converging on the seL4 API, it presently contains simplified versions of IPC control and all kernel resource allocation is under control of a user-level policy server. It should implement a full seL4 API probably sometime next year.
I've already come across OKL4 - I've always wondered what would happen when OKL4 has actually developed into an seL4 API implementation. Was OKL4 started as a second chance effort "should seL4 not work out" or "should it take longer than anticipated" or simply to allow clients using L4 to slowly migrate with each OKL4 realease toward seL4? Will they co-exist or will one be selected? Thanks for your time and the update on seL4; I really appreciate it. Greetings, Ernst Rohlicek jun. <ernst.rohlicek@inode.at>
On Fri, 03 Aug 2007 19:10:22 +0200, "Ernst Rohlicek jun." <ernst.rohlicek@inode.at> said:
ERj> [...] ERj> In the paper, there is a mention of a "Coyotos" project by Mr. Shapiro, ERj> also striving to create a high-security microkernel. Where would you see ERj> seL4's strengths compared to Coyotos and vice versa? seL4 is an OL4 kernel, so it provides an upgrade path for existing commercial deployments of L4. Also, seL4 will have a formal correctness proof, i.e., a mathematical proof that the security (and other) properties proved about the API will hold for the actual implementation. No such proof exists for any system out there, nor is likely to exist for any other system in the foreseeable future (see http://ertos.nicta.com.au/research/l4.verified/).
The commercial OKL4 microkernel is converging on the seL4 API, it presently contains simplified versions of IPC control and all kernel resource allocation is under control of a user-level policy server. It should implement a full seL4 API probably sometime next year.
ERj> I've already come across OKL4 - I've always wondered what would happen ERj> when OKL4 has actually developed into an seL4 API implementation. ERj> Was OKL4 started as a second chance effort "should seL4 not work out" or ERj> "should it take longer than anticipated" or simply to allow clients ERj> using L4 to slowly migrate with each OKL4 realease toward seL4? Will ERj> they co-exist or will one be selected? No, OKL4 is the commercially-supported version of what used to be called L4-embedded. It wasn't "started" in that sense, it was continued to provide commercial support for pre-existing and new commercial customers. It's out there in end-user products (see the recent announcement about the Toshiba phone). seL4 was done initially as a separate code base (forked from L4-embedded) to avoid hampering the research project with commercial realities, but while it is progressing, the OKL4 API is being successively adapted towards seL4. Having a large customer base (with many big multinationals) we need to be gentle with API changes. Most of it will be dealt with by migrating customers to a higher-level API that hides most changes. ERj> Thanks for your time and the update on seL4; I really appreciate it. Welcome, Gernot
Hi, On 8/3/07, Gernot Heiser <gernot@nicta.com.au> wrote:
The commercial OKL4 microkernel is converging on the seL4 API, it presently contains simplified versions of IPC control and all kernel resource allocation is under control of a user-level policy server. It should implement a full seL4 API probably sometime next year.
Gernot
I have several questions: 1)What does "simplified versions of IPC control" refer to? 2)"all kernel resource allocation is under control of a user-level policy server" - does the user-level policy server refer to Iguana? 3)Can these features you noted be found in current Pistachio-e and Iguana release? All they belong to close-source part of OKL4? Thanks! Wei Shen
On Tue, 7 Aug 2007 13:26:58 +0800, "Wei Shen" <cquark@gmail.com> said: WS> Hi, WS> On 8/3/07, Gernot Heiser <gernot@nicta.com.au> wrote:
WS> The commercial OKL4 microkernel is converging on the seL4 API, it WS> presently contains simplified versions of IPC control and all kernel WS> resource allocation is under control of a user-level policy server. It WS> should implement a full seL4 API probably sometime next year. WS> Gernot WS> I have several questions: WS> 1)What does "simplified versions of IPC control" refer to? There is a privileged IpcControl() syscall that allows you to set IPC restrictions on an address space (send anywhere, send anywhere except some, send only to some). WS> 2)"all kernel resource allocation is under control of a user-level policy WS> server" - does the user-level policy server refer to Iguana? As far as the kernel is concerned, it's the root task. In the OKL4 system the root task is Iguana. WS> 3)Can these features you noted be found in current Pistachio-e and Iguana WS> release? All they belong to close-source part of OKL4? They are in the released open-source OKL4l, and nicely documented in the very extensive (260 page) OKL4 Microkernel Programming Manual available at http://portal.ok-labs.com/ There is no closed-source part of OKL4, other than platform code that is specific to proprietary customer hardware. However, there is a release backlog (sorry). Nevertheless, what you are asking for is released, supported, deployed by commercial customers, and open source. Gernot
Hi, Shouldn't IPC restrictions and such be implemented on top of L4, in some OS personality? Thank you, Jorge On 8/7/07, Gernot Heiser <gernot@nicta.com.au> wrote:
On Tue, 7 Aug 2007 13:26:58 +0800, "Wei Shen" <cquark@gmail.com> said: WS> Hi, WS> On 8/3/07, Gernot Heiser <gernot@nicta.com.au> wrote:
WS> The commercial OKL4 microkernel is converging on the seL4 API, it WS> presently contains simplified versions of IPC control and all kernel WS> resource allocation is under control of a user-level policy server. It WS> should implement a full seL4 API probably sometime next year.
WS> Gernot
WS> I have several questions: WS> 1)What does "simplified versions of IPC control" refer to?
There is a privileged IpcControl() syscall that allows you to set IPC restrictions on an address space (send anywhere, send anywhere except some, send only to some).
WS> 2)"all kernel resource allocation is under control of a user-level policy WS> server" - does the user-level policy server refer to Iguana?
As far as the kernel is concerned, it's the root task. In the OKL4 system the root task is Iguana.
WS> 3)Can these features you noted be found in current Pistachio-e and Iguana WS> release? All they belong to close-source part of OKL4?
They are in the released open-source OKL4l, and nicely documented in the very extensive (260 page) OKL4 Microkernel Programming Manual available at http://portal.ok-labs.com/
There is no closed-source part of OKL4, other than platform code that is specific to proprietary customer hardware. However, there is a release backlog (sorry). Nevertheless, what you are asking for is released, supported, deployed by commercial customers, and open source.
Gernot
_______________________________________________ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
On Tue, 7 Aug 2007 17:18:31 -0400, "Jorge Torres" <jorge.torres.maldonado@gmail.com> said: JT> Hi, JT> Shouldn't IPC restrictions and such be implemented on top of L4, in some OS JT> personality?
The policy, yes. The mechanism must be provided by the kernel. This is exactly what OKL4 does. Gernot
participants (7)
-
Bjoern Doebel -
Ernst Rohlicek jun. -
Gernot Heiser -
Jorge Torres -
Marcus Voelp -
Neal H. Walfield -
Wei Shen