Genode OS: A tool kit for highly secure special-purpose operating systems | Hacker News Reader

Genode OS: A tool kit for highly secure special-purpose operating systems

genode.org

205 pointsdoener31 comments

I've been following the Genode project for quite some time, and first got the chance to meet the Genode team when they presented their work at FOSDEM in 2012. I've since been amazed, both at the pace of development they've kept up while keeping to their principles of a small trusted code base that is kept clean by refactoring when common concepts are outlined.

My friend Daniel and I were invited to join their Hack n' Hike event a few years back, and it was just the loveliest! We hiked together during the days, sharing a barbecue around the camp fire in the evenings and hacking together at night. The people on the Genode team are among the friendliest I've come across in the open source community.

I wish you all the best of futures, both with the Genode project and in life in general.

Cheerful regards, Robin

Edit: the slides from FOSDEM 2012 introducing Genode (in the state of the project back then): https://genode-labs.com/publications/nfeske-genode-fosdem-20...

The fine people on the Genode project did yeoman's work for constructing something sufficiently complex atop seL4. Without their exploring, mailing-list cajoling, implementation, and write-ups our seL4 work would be significantly more painful, and it's already unpleasantly painful as-is.

sel4.systems appears to be down currently

Now it's up again: http://sel4.systems/

It's worth to note they now have a downloadable USB image, which is notably dogfed (dogfooded? dogfeeded?) by the Genode developers:

https://genode.org/download/sculpt

And some eye candy:

https://genode.org/about/screenshots

It’s a verb (to dogfood) so it would be dogfooded. More intuitive if you use it in continuous tense: “I am/have been dogfooding Foobar on my dog.”

Also they really need to put a README on that live CD.

Distrowatch did a review of it (which I would bet inspired someone to submit genode to hackernews) https://distrowatch.com/weekly.php?issue=20190121#sculpt

> It's worth to note they now have a downloadable USB image, which is notably dogfed (dogfooded? dogfeeded?) by the Genode developers: https://genode.org/download/sculpt

I fetched their `sculpt-vc.img` and create qcow out of it to directly boot in qemu.

$ qemu-img convert -f raw -O qcow2 sculpt-vc.img /var/lib/libvirt/images/sculpt-vc.qcow2

The resulting image is not bootable. It fails on boot showing Genode logo and goes into a reboot cycle.

$ file sc*

sculpt-vc.img: DOS/MBR boot sector, extended partition table (last)

sculpt-vc.qcow2: QEMU QCOW2 Image (v3), 24375296 bytes

Genode uses PCI MMCONFIG, so you have to use 'qemu -machine q35' not 'pc'.

Nice. This got me going

$ qemu-system-x86_64 -name guest=humbug,debug-threads=on -drive file=/var/lib/libvirt/images/sculpt-vc.qcow2 -machine q35 ....

They implement a Nizza-like architecture to let you choose how much risk you want for each part of your stack:

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

It's also designed to allow separation kernels to be used in foundation. There's been quite a few of them:

https://arxiv.org/pdf/1701.01535

Do you think it is feasible, for a poweruser who can setup and debug linux installations, to setup and use GenodeOS or sel4 as of today as a main workstation with X applications on the level of Xfce, Firefox? (days, or months, or not at all?)

I haven't used the recent version. Try it out. Tell us how well it works or doesnt. Preferably on hardware you know is supported.

> Do you think it is feasible, for a poweruser who can setup and debug linux installations, to setup and use GenodeOS or sel4 as of today as a main workstation with X applications on the level of Xfce, Firefox? (days, or months, or not at all?)

Coming from UNIX, used sculpt on QeMU just yesterday. Let me just say this - the exploration was pretty much just `meh`. But also - the devil is in the detail. I bet, if I read the documentation and then go back, I'll stop flaffing around too much and use it to do awesome things.

I loved the ViM though ;)

An obligatory mention when we talk about secure operating systems is the seL4 microkernel (https://github.com/seL4/seL4) where they have formally verified every line of code using the proof assistant Isabelle/HOL.

Yes, I read about it in the German Wikipedia (https://de.wikipedia.org/wiki/L4_(Mikrokernel)), but the link provided there as a source does not work anymore: http://ertos.nicta.com.au/research/l4.verified

The other link provided is a press release in German: http://pressetext.de/news/090817022/sicherheits-beweis-fuer-...

PS: As always I recommend https://www.deepl.com/translator for translation.

Thanks for mentioning that site. Did not know about it, glad I do now.

Always made me curious why Google didn't decide to use seL4 as a base for Fuchsia and instead went with Zircon...

There might be license issues between AGPLv3 of GenodeOS and the Apache 2.0 or GPLv2 that Android components use.

? I know that this is a GenodeOS topic, but the GP wondered about seL4 which has some parts in GPLv2 and other BSD (2-clause).

IMHO the reason that few use seL4 is that it isn't ready: AFAIK seL4 isn't able to use efficiently multiple core with power savings, which is mandatory for usage in phones (and phones can use complex CPU with big and little cores).

synergy - Android's bootloader (fastboot mode, etc) uses LK, of which Zircon is a fork.

> where they have formally verified every line of code using the proof assistant Isabelle/HOL.

and it's interesting to note that even then, they still had a few bugs here and there due to incomplete / wrong formalisation

Also, I imagine, automatic theorem provers, too, can have bugs.

Yes. That's the reason the formal methodists started building verified or checkable tools with the checkers being tiny. Doing an solver might involve making it produce a log of each step it made with a simpler system checking them. The checking is also easy to parallelize with linear scaling. My current recommendation is checkable solvers done in a parallel language like Chapel with tiny, verified checkers. Run it logless first to see if it even passes at all. Once passes, run it in logging mode to get evidence to feed to checker. Use multiple, sequential processes to check that as concurrency in checker reduces confidence.

I was wondering what the fit with Qubes OS was. Found this entry on Genode challenges page:

"Genode as virtualization layer for Qubes OS - ...This exploration project pursues the goal of replacing Xen by Genode as virtualization layer for Qubes."

> I was wondering what the fit with Qubes OS was.

Rootkovska has been (imvho rightfully) criticized in the past for selling isolation but dismissing the attack surface in Xen. I think Genode can help here:

https://twitter.com/rootkovska/status/949297922998489088

Though I believe thegrugq / ioerror have a point when they say that hardware compartmentalization is superior than layers of SW virtualization:

https://twitter.com/thegrugq/status/515085244198703105

The threat model is relevant though: In that aspect QubesOS has some problem finding an audience. I personally like it (I'm an active user) ... but mostly because I have a fetish for privacy+security and I like to play with new stuff. However if you push a journalist or activist or anyone facing real risk to learn QubesOS (the learning curve is huge for the general user), it makes more sense to just invest in HW based compartmentalization instead. HW compartmentalization can easier be trained and there is less likely a chance of shooting yourself in the foot. It's not a tech that anybody whose life is under threat should be using. First rule here not to use tech in the first place, and for cases where the risk is marginal use HW based isolation ... then there is nothing for a long time followed by things like QubesOS, Signal etc. These things are just good enough to hide an affair but it's reckless selling them as serious solution to tech-illiterate folk who have something to loose.

Said attack surface is exactly why OpenBSD was so hesitant to buy into the virtualization trend up until they rolled their own hypervisor.

I think the linked Rootkovska tweet (or more specifically, her own thread/replies to it) actually gracefully acknowledges that Xen is not magically free of attack surfaces.

She's also written some fairly long-form articles about Xen security and the (sometimes significant) room for improvement, including, for example, this Black Hat talk (from 2008!) about breaking Xen: https://invisiblethingslab.com/resources/bh08/part3.pdf

I don't disagree with the rest of your comment :) I just have the impression that any discussion about Qubes+Xen is less "dismissal" and more that supporting a variety of hypervisors is "a small matter of programming" (where "small" is used to mean "absolutely not small").

Actually no, I stumbled upon Genode OS on this list: https://en.wikipedia.org/wiki/Category:Microkernel-based_ope...

I want to run this on qemu/kvm Linux. How?

Reply on news.ycombinator.com