Thanks for your reply.
   On Wed, Feb 10, 2016 at 7:00 PM Peter Gutmann
   <[1]pgut001@cs.auckland.ac.nz> wrote:

     Sean Lynch <[2]seanl@literati.org> writes:
     >And of course both Nova and seL4 have had a lot of trouble gaining
     any kind
     >of foothold in the market.
     That's because you need to add way too much other stuff to them to
     make them
     generally useful.  My favourite quote on this, attributed to Nick
     Foster, is:
       You know, when you have a program that does something really cool,
     and you
       wrote it from scratch, and it took a significant part of your
     life, you
       grow fond of it. When it's finished, it feels like some kind of
     amorphous
       sculpture that you've created. It has an abstract shape in your
     head
       that's completely independent of its actual purpose. Elegant,
     simple,
       beautiful. Then, only a year later, after making dozens of
     pragmatic
       alterations to suit the people who use it, not only has your
     Venus-de-
       Milo lost both arms, she also has a giraffe's head sticking out of
     her
       chest and a cherubic penis that squirts colored water into a
     plastic
       bucket. The romance has become so painful that each day you
     struggle with
       an overwhelming urge to smash the fucking thing to pieces with a
     hammer.

   This is my general experience with programming, yes, though it is
   somewhat orthogonal to security.

     You can write pretty good, minimal, very high-assurance code if you
     follow
     something like DO-178B and get people who are a fair way down the
     ASD
     spectrum to work on it, but then you've got something that's
     hardcoded to
     do one thing really well in a tightly-controlled environment, and
     nothing
     else.  A lot of the crap out there exists because it has to interact
     with
     a bazillion buggy pieces of hardware and software and support unique
     absolutely mission-critical customer requirements that no-one else
     on
     earth has.  seL4 makes all of this someone else's problem, while
     Linux
     and Windows and whatnot make it their problem.

   It makes it someone else's problem *in userspace*. Linux supports all
   that stuff, but it does so *in kernel space*. And while seL4 and Nova
   don't address device drivers, Genode does, by reimplementing the Linux
   (and NetBSD, and OpenBSD, and FreeBSD) kernel interfaces (yes, I know
   in the Linux case this is a moving target, but Linux has a LOT of
   drivers, so even if you're stuck to a narrow range of versions, you can
   still get a lot of mileage out of this approach) and then running each
   driver as a separate server process.
   I'm not talking about raw size or complexity here; obviously having
   lots of features and support for lots of devices means high complexity,
   but it doesn't require that all that complexity run with full system
   privileges.

References

   1. mailto:pgut001@cs.auckland.ac.nz
   2. mailto:seanl@literati.org