I'm new to seL4 (and L4 generally). I'd like to initially run my application functionality in Linux on top of seL4 (x86) and then over time migrate pieces of its functionality to run directly on seL4 to achieve finer-grained confinement.
I'm having trouble finding any instructions on how to run a Linux environment on top of seL4. Either paravirtualized or hardware virtualized would be ok. So far I found pointers to L4Linux but it appears to need L4Re. Can anyone point me in the right direction?
Thanks, Rob
On 15 Oct 2014, at 14:34 , Robert Brewer <rwb123@gmail.commailto:rwb123@gmail.com> wrote:
I'm new to seL4 (and L4 generally). I'd like to initially run my application functionality in Linux on top of seL4 (x86) and then over time migrate pieces of its functionality to run directly on seL4 to achieve finer-grained confinement.
I'm having trouble finding any instructions on how to run a Linux environment on top of seL4. Either paravirtualized or hardware virtualized would be ok. So far I found pointers to L4Linux but it appears to need L4Re. Can anyone point me in the right direction?
The instructions are sparse, we should add at least a README.
We no longer support para-virtualized Linux (as in L4Linux), too much work and no longer justified with hardware support widely available. We support hardware-supported virtualisation on x86 and soon on ARM.
On x86, the kernel runs in Ring-0 root mode, and virtualization events are reflected to a virtual-machine monitor (VMM) running in Ring-3 root mode. On http://sel4.systems/Download/ there is a rerference to a CAmkES-based VMM at https://github.com/seL4/camkes-vm-manifest.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
x86 support is actually becoming more critical for us (and I suspect for a lot of other research groups too) since we are looking at replacing the VM layer in private clouds for financial and other secure applications with sel4. Only issue is IA64 support which I believe is still not stable in seL4 ?
With stable IA64 support, seL4 becomes an excellent candidate for Secure Enterprise Virtualization.
On Thu, Oct 16, 2014 at 11:21 AM, Gernot Heiser gernot@nicta.com.au wrote:
On 15 Oct 2014, at 14:34 , Robert Brewer <rwb123@gmail.commailto: rwb123@gmail.com> wrote:
I'm new to seL4 (and L4 generally). I'd like to initially run my application functionality in Linux on top of seL4 (x86) and then over time migrate pieces of its functionality to run directly on seL4 to achieve finer-grained confinement.
I'm having trouble finding any instructions on how to run a Linux environment on top of seL4. Either paravirtualized or hardware virtualized would be ok. So far I found pointers to L4Linux but it appears to need L4Re. Can anyone point me in the right direction?
The instructions are sparse, we should add at least a README.
We no longer support para-virtualized Linux (as in L4Linux), too much work and no longer justified with hardware support widely available. We support hardware-supported virtualisation on x86 and soon on ARM.
On x86, the kernel runs in Ring-0 root mode, and virtualization events are reflected to a virtual-machine monitor (VMM) running in Ring-3 root mode. On http://sel4.systems/Download/ there is a rerference to a CAmkES-based VMM at https://github.com/seL4/camkes-vm-manifest.
Gernot
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 16 Oct 2014, at 17:38 , S Madhu <smadhu2048@gmail.commailto:smadhu2048@gmail.com> wrote:
x86 support is actually becoming more critical for us (and I suspect for a lot of other research groups too) since we are looking at replacing the VM layer in private clouds for financial and other secure applications with sel4. Only issue is IA64 support which I believe is still not stable in seL4 ?
With stable IA64 support, seL4 becomes an excellent candidate for Secure Enterprise Virtualization.
I assume when you say “IA64” you mean what Intel marketing this week cunfuslingly calls “Intel 64”, otherwise known as x86-64, or simply x86. (“IA-64” is Itanium, a completely different, and, unfortunately, almost completely dead architecture.)
x64 support is sort-of working but not yet releasable. It also isn’t a particularly high priority for us ATM. This can change if someone wants to inject some cash. Failing that we are not prepared to commit to a release anytime soon.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-
Gernot Heiser -
Robert Brewer -
S Madhu