Comment by boricj | Hacker News Reader

Comment by boricj | Hacker News Reader

Parent Full thread

Former MINIX3 contributor here, I'd like to share my perspective.

While others have noted that grant money has run out, for me MINIX3 is only as good as its weakest link: its microkernel has a really dated design. Imagine taking 1980s Unix and gutting it until you have a microkernel: it has a fork() primitive oddly enough, it's not SMP-safe, it's 32 bit only, processes only have one thread... It's the one area of the OS that hasn't changed that much since 1987.

So while there has been some very good research done on it (https://wiki.minix3.org/doku.php?id=publications, especially of note reliability in face of drivers and services misbehaving or crashing as well as live update of almost all drivers and services without interruption of service), it cannot take advantage of modern 64 bit, multi-core processors.

Furthermore, the second weakest link is driver support. Running on bare metal is possible but vintage hardware is best suited for it because of the limited hardware support. Especially problematic is the lack of USB support on x86. NetBSD's rumpkernel would have been a potential in-tree solution to fix this, but sadly it has never been done.

Anyways, these days the Zircon microkernel seems extremely promising. The design seems well thought-out, the object/handle/IPC mechanisms are especially interesting because it's rather unlike everything else done at this point that I'm aware of and processes can only interact with the rest of the system through handles, so it's trivial to sandbox things.

As for me on OS development, right now I'm having fun hacking on SerenityOS. It's a sin for a micro-kernel guy like me, but who's to say I can't have a little bit of fun on the side?

Wasn't that kind of thing an intentional part of its design?

My understanding was that Tanenbaum made it as a teaching tool and always resisted attempts to modernize it too much, lest it becomes too complicated for students to understand. The lack of SMP support may well be one of those things.

It's part of the legacy of an educational operating system from 1987 that initially targeted 8086 systems with 640 KiB memory and two 360 KiB floppy drives. The teaching focus was deemphasized after the release of MINIX 3.1.0, so the system did gain features like VFS and paged virtual memory after that. There was an early version in the 3.1.x era that had experimental SMP support in the form of a BKL, but it has bit-rotten a long time ago. Alas, the microkernel never received the rewrite it needed to bring it into the 21st century.

That is not to say that MINIX ever was just a toy OS, it was self-hosted from the first publicly released version if I'm not mistaken. But it takes much, much more than that to be a daily use OS nowadays.

In my opinion, the problem with MINIX3 is that as a product it lacked focus. MINIX2 was excellent for education. MINIX3 led to great research. But if you want to maintain a software product with a small team, you have to have a clear idea of what features are essential for your product and then make sure those have excellent support.

I'm very much in agreement with this comment, it is a fair assessment of Minix' weaknesses.

Zircon... Another Google-product... No thanks!

What's your opinion on Genode (on seL4)?

(redox-os seems to be heading the way of the dodo as well...)

I'll admit I've never played with or looked into Genode, so I can't meaningfully comment on it.

Regarding seL4, I haven't played with it but I did read their whitepaper. I believe they are setting the gold standard for microkernels in reliability and correctness. Not many systems can claim to have a formally-verified trusted computing base of not only their source code, but the binary artefacts too. This is the closest kernel project I know of that can potentially mitigate against attacks as described in the paper "Reflections on Trusting Trust" by Ken Thomson.

That is not to say that their approach is fool-proof. Like any proof, they make assumptions, which in this case is that the base hardware (CPU, MMU, memory...) does and only does what their specification claims, which the long list of erratas in Intel CPUs as well as Spectre, Meltdown, rowhammer, the Intel Management Engine debacle and others showed that they definitely don't. Not that other hardware vendors are immune too, by the way.

Their formally-verified proof is also limited to the microkernel. So while they claim to guarantee that userland processes can't compromise the microkernel nor compromise other userland processes through the microkernel (which does have its uses in embedded systems requiring high reliability), it has no bearing on what the userland does. Heartbleed wouldn't have been stopped by seL4 for example, not to mention social engineering, evil maid attacks, DMA attacks, attacks on packaging system (I lost count of the number of NPM modules that were compromised over the years), not to mention plain user stupidity.

In a way, "Reflections on Trusting Trust" by Ken Thomson has never been more relevant than today. On a typical Linux desktop operating system, we effectively blindly assume that hundreds of millions of lines of code, taken from tens of thousands of code repositories from the Internet, written in mostly unsafe languages (or languages whose interpreters/VMs are written in unsafe languages), running on a monolithic kernel with tens of millions of code written in C, running on hardware that is effectively a big black box, does what they're supposed to do and nothing more.

Even if you do audit stuff, a human can't possibly audit everything from the LLVM compiler to your web browser, not to mention we are effectively emotionally-driven, tribal-minded, chemically-influenced, prejudiced, illogical and error-prone ape brains and anyone pretending to be a perfect Vulcan is either delusional or lying.

Not to mention, I just read their whitepaper and thought to myself "yeah, sounds good". I haven't actually audited seL4, their methodology and their proof, so... As the meme says: everything is fine?

Before I trigger panic attacks, I do have to note that humans abstract away reality until we can handle it, whether it's in engineering, manufacturing, physics, food supply chains, sociology or anything else. This is effectively how our society operates: mostly that problems we don't deal with directly are taken care of by somebody else in good faith. That is not to say we can't mitigate reality if we're willing to put in the price, but except in mathematics we are never building on first principles.

> but except in mathematics we are never building on first principles

In practice, mathematicians also assume "that problems we don't deal with directly are taken care of by somebody else in good faith". We use theorems that others proved, and we trust that the authors and the reviewers did their job, without inspecting the proofs ourselves. Sometimes mistakes slip through, but they are usually caught fairly quickly, and can be fixed locally. In other words, we are less strict than we like to think we are, but we get away with it perfectly well.

Reply on news.ycombinator.com