On 7 Sep 2019, at 13:32, Gergely Buday <[email protected]<mailto:[email protected]>> wrote:
how does Muen relate to seL4? https://muen.codelabs.ch/ e.g. it claims to be the first verified microkernel. That has always been pretty dodgy marketing. It claims to be the first *open source* verified microkernel. The first part of which is technically true, since seL4 became open source slightly later, but seL4 was of course verified much before Muen. The second part I would actually contest, because they themselves (correctly, as far as I can see ) call it a separation kernel in the rest of the docs, not a general-purpose microkernel. seL4 can be configured as a separation kernel, but that is just one of many ways of using it. Muen as far as I can tell doesn’t really compare in feature set or depth of verification. It shows absence runtime errors only, which 10 years ago would have been cool, but is a bit behind the times. seL4 had full functional correctness in 2009 already (which includes absence of runtime errors), and by now also binary correctness, security theorems, etc. Doesn’t mean it’s a bad project, It’s probably fine for the limited application area it is aimed at, but the verification is comparatively shallow. Cheers, Gerwin
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
