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.
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.
> 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.
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?)
> 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.
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. 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 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).
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."
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:
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.
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").
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...