Genode OS Framework 19.05 | Hacker News Reader

Genode OS Framework 19.05

genode.org

80 pointssnvzz20 comments

Love the updated C++17 support, Ada/SPARK improvements, Muen and OpenJDK integration.

Could someone give a short explanation? I browsed through home page but I couldn't get a good picture of what it is.

Is it a new OS, without using the Linux kernel but still using GNU tools (I saw a lot of references to GCC, GNU binutils, etc.).

It is a new research OS using micro-kernel design, built in a mix of C++ and Ada, with a pluggable layers.

It also has a POSIX compatibility layer, hence the references you saw.

The best way is to browse through https://genode.org/documentation/genode-foundations/19.05/in...

Interesting why they couldn't go with 100% Ada - because of technical limitations or they just wanted to reach more people...

It seems that Ada just relatively recently entered their field of vision.

Best described here: https://genode.org/documentation/genode-foundations/19.05/in...

Most projects depend on complex, vulnerable OS's like Linux that nobody knows how to secure. High-assurance security prefers minimalist foundations designed for security. Then, those foundations are leveraged by user-facing layers to inherit their properties. It's usually isolation of compromises to specific parts of memory with some support for blocking side channels between partitions. Genode follows that approach using an architecture similar to Nizza and Perseus:

https://os.inf.tu-dresden.de/papers_ps/nizza.pdf

http://www.perseus-os.org/content/pages/Architecture.htm

The NOVA microhypervisor, if compared to popular VMM's, is also illustrative of how high-assurance security applies minimalist, privilege-reducing design to the problem:

http://hypervisor.org/eurosys2010.pdf

Although I don't know Genode's assurances, most of the field also tries to make the assurance (confidence level) of the system as high as possible by using techniques that prove it has certain properties and/or rid it of as many vulnerabilities as possible. I have a list of historical and current methods here:

https://pastebin.com/uyNfvqcp

A discussion from 2015: https://news.ycombinator.com/item?id=10139224

The µkernel-agnostic abi for hypervisors is so cool.

I'm looking forward to them getting virtualbox working, too.

I think it does already perhaps,

http://genodians.org/alex-ab/2019-03-06-disposal-browser-vm discusses IIUC a disposable firefox instance, running in genode, which is run in either virtual box, or seoul vmm.

Similarly some other pages say the easiest way try it is by running genode in virtual box, so I think that covers all the bases no?

Yes, virtualbox works under genode and has for years.

What's not there yet is support for the cross-microkernel abi, as that only works with virtualbox on NOVA currently.

Can this be used to create a tiny specialized environment to run Docker containers?

It already offers much better mechanisms that the Linux ones docker uses for isolation and communication between containers.

I see it as a vastly superior competitor to Linux and Docker than a base for Docker.

Lot of superlative in there for a project I've never seen used anywhere.

But competition is good and you never know so I'll keep an eye on it.

If you want to know why it isn't used anywhere, try using it somewhere. Like most (all?) microkernel projects it seems to exist purely for academic purposes.

Yet another one that didn't realize that most high integrity systems, where human lives are at stake, mobile radio stacks, factory automation, run real time OSes with microkernel design.

Or that macOS, Windows and their derived implementations use an hybrid design.

Pure UNIX clones are the surviving monoliths.

Ok you got me there, I have literally no experience with such systems.

Counterpoints:

https://www.cs.vu.nl/%7East/reliable-os/

Especially QNX [1]. Green Hill's INTEGRITY, Sysgo's PikeOS, and Lynx's LynxOS-178B are other examples in safety-critical fields like aerospace. I think DDC-I's DEOS, which is in a bunch of aircraft systems, looked like a microkernel in its architectural diagrams. One of their main advantages, other than size, is that they let you evaluate systems piece by piece looking at components in isolation and then their specific, permitted interactions. Traditional monoliths might have control flow and state changes jumping all over the place.

[1] Look up demos of the Blackberry Playbook vs iPad to see how usable, fast, and stutter free QNX-based system was.

I have no idea why you would consider popularity a proxy for quality.

They were actually objectively-true statements. That person just didn't give you evidence supporting them. Here's a few things these alternative designs do:

1. Tiny amount of code in kernel mode with privilege services run with as much untrusted code as possible. Linux is already miles away from this. Even starting with Linux makes you automatically lose against a minimalist, security-focused design. There's even vendors that pre-supply folks with money vulnerabilities to use against Linux. A steady stream.

2. Built-in support at the very foundation for both strong process isolation, decomposing a system into components, and making them communicate easily. The security is almost always better if it's baked in rather than bolted on. At the least, there's fewer bad interactions or escape hatches that can happen when combining insecure and security-focused code.

3. For many L4-related projects, Camkes as a way to handle IPC for you. They usually have some kind of middleware for automatically generating code for components to communicate. They focus on correctness and security more than feature support. I don't know how Docker compares there.

https://ts.data61.csiro.au/software/TS/camkes/

4. Now, like Docker, Genode has some kind of build tooling to put it all together. I haven't read as much about recent changes. So, I'll just say they both do this kind of thing now. I'll also note that separation kernels are typically designed to be integrated with an application, OS, or whatever into a deployable image that contains just what they need. In most, the resources and scheduling policy are also done statically in the code to reduce attack surface.

If you're talking security and componentization, Genode-like designs have Docker beat with a foundation that has way less code, is actually designed for security, and makes achieving it easier by default. One still has to work on assuring anything they build on top. The GenodeOS might have vulnerabilities, too. Just by the numbers, Linux is going to have way more with higher impact on average. If you doubt that...

https://events.linuxfoundation.org/wp-content/uploads/2017/1...

Reply on news.ycombinator.com