Re: [seL4] seL4 + Qubes OS Project

On 19 Mar 2015, at 2:01 am, Toby Murray wrote:

On 19/03/15 02:59, Marcus Hähnel wrote:

...

On 2015-03-18 16:32, Tim Newsham wrote:

...

Though thats still a bit different than what qubes gives you, and although the TCB is smaller, none of it is proven.

Which, just to nitpick, it is neither for seL4. Unless you plan to run your code on an "imx31 platform, arm1136jf-s CPU, ARMv6 architecture" [0]. I'm not sure that this is feasible for any serious workload.

I should point out that while the current proofs for seL4 hold only for this platform, that "porting" them to similar platforms we know will be relatively straightforward.

Gerwin Klein can elaborate if needed, but I think we can say with confidence that moving the proofs over to e.g. the SABRE Lite (imx6, ARMv7 platform) would require relatively little effort -- it's just not a high priority for us at the moment.

In fact, we expect to be able to release the proof for imx6 later this year. Cheers, Gerwin ________________________________ 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.