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 wrote:

On 15 Oct 2014, at 14:34 , Robert Brewer > 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