"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 marcus@mh-development.info 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'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