Thanks for your reply. On Wed, Feb 10, 2016 at 7:00 PM Peter Gutmann <[email protected]> wrote:
> Sean Lynch <[email protected]> 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.
