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. We do expect to move the proofs to a newer ARM platform in the future. Moving to another architecture, like x86, is of course another matter altogether. Cheers Toby ________________________________ 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.