"Which, just to nitpick, it is neither for seL4" -- a fine nit to pick
and I don't think seL4 should be over-sold... But I do think there is great
benefit to formal verification beyond just the certificate at the end.
Although various ports might have introduced subtle flaws that
have not been shaken out by formal verification (yet?), at least large
portions of the code base have been through the verification process.
And that process has removed bugs from that code. The lack of
memory corruption issues, integer overflows, undefined C behaviors,
etc. in that code should benefit even the unproven ports.
On Wed, Mar 18, 2015 at 8:59 AM, Marcus Hähnel
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
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com