Hi Christian, we did of course do a lot of digging in that direction, there is at least a 30-year history of attempted OS verification, and quite a few success stories (PSOS, KSOS, EROS, KIT etc).
Specifically, the claim for seL4 is machine-checked code-level verification. As far as we are aware, only [1] has done something comparable before seL4, and it is very much a demo toy system only, orders of magnitude smaller. Everything else we’re aware of is not machine-checked verification (i.e. pen-and-paper) or is model-level verification, where not the code is verified, but a manually constructed model of what the code does. Cheers, Gerwin > On 11 Mar 2016, at 11:33, Christian Stroetmann <[email protected]> wrote: > > On the 10th of March 2016 at 23:21, Wolfgang Keller wrote >>> Interesting statement on the Muen kernel section: "The world’s first Open >>> Source microkernel that has been formally proven to contain no runtime >>> errors at the source code level. “ >>> >>> We proved full functional correctness (which is a superset of absence of >>> runtime errors) for seL4 in 2009. I must be missing something. >> I believe how it is meant is the following: "The first kernel to both >> reach being open source and being proven to contain no runtime errors >> is Muen." (of course among the kernels that are *now* open source, >> seL4 is the first one for which the absence of runtime errors was >> proven) >> >> Wolfgang >> > > Indeed, I also found this statement a little confusing at first. > > But nevertheless, I am still very critical with this claim by NICTA as well, > because I am virtually for 100% sure, that on the one hand the NASA verified > an RTOS for a spacecraft, the USArmy (DARPA, AFRL, etc.) verified an RTOS for > a cruise missile or another critical equipement, and one of the largest > aircraft manufacturers (e.g. Boeing, Lockheed Martin, Tupolev, or > Mikoyan-Gurevich) verified some kind of a small operating system. > On the other hand there were always attempts to do such a work, as it could > be seen for example with [1], and it is hardly not convincing that in the > following 22 years nobody else tried and eventually achieved it. > > In the case of the NASA and the USArmy I am still waiting for a disclosure of > historical informations, which in the case of the army most potentially is > still confidential. > > What makes a judgement even more difficult or even impossible is the problem > to draw the exact limits in relation with what is understood as a > microkernel, a general purpose operating system kernel and so on for being > able to make such a statement "The first verified ... system" at all. > > > > Regards > Christian Stroetmann > > [1] William R. Bevier: "A Verified Operating System Kernel", Technical Report > 11, October, 1987 > >> >> >> On Thu, Mar 10, 2016 at 10:33 PM, Gernot Heiser<[email protected]> wrote: >>> Interesting statement on the Muen kernel section: "The world’s first Open >>> Source microkernel that has been formally proven to contain no runtime >>> errors at the source code level. “ >>> >>> We proved full functional correctness (which is a superset of absence of >>> runtime errors) for seL4 in 2009. I must be missing something. >>> >>> Gernot >>> >>>> On 11 Mar 2016, at 6:50 , Jakub Jermář<[email protected]> wrote: >>>> >>>> Hello, >>>> >>>> just FYI, I have set up a simple web page[1] to promote the wider >>>> microkernel community and its goals. So far, the page comes with a brief >>>> description of the microkernel concept and an incomplete list of >>>> microkernel projects with links to each project's web. The description >>>> is made out of the first two sentences I found in the "What is XYZ" >>>> section or elsewhere on the web of the respective project. I also took >>>> the freedom to use the respective project's logo (or what I believed was >>>> the project's logo) for promoting it. >>>> >>>> I hope you will find this small web a good idea. It was inspired by a >>>> similar (though a little bit more informative) site set up by the >>>> unikernel community [2]. The sources of the [1] web are hosted on Github >>>> [3], so feel free to submit issues or PR to make the site better. >>>> >>>> Please send me a PM if there are any issues pertaining your project's >>>> cartouche that cannot be dealt with using Github. >>>> >>>> Thanks, >>>> Jakub >>>> >>>> [1] http://microkernel.info >>>> [2] http://unikernel.org/projects/ >>>> [3] https://github.com/jermar/microkernel.info >>>> >>>> _______________________________________________ >>>> Devel mailing list >>>> [email protected] >>>> https://sel4.systems/lists/listinfo/devel >>> >>> ________________________________ >>> >>> 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 >> _______________________________________________ >> Devel mailing list >> [email protected] >> https://sel4.systems/lists/listinfo/devel > > > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
