19 Mar
2015
19 Mar
'15
2:59 a.m.
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'm just saying as people tend to forget that and expect the proof to hold for all platforms and all systems. This is not the case. - Marcus [0] http://sel4.org/FAQ/#whichcode