> On 19 Mar 2015, at 2:01 am, Toby Murray <[email protected]> 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. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
