Live data from Hacker News

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

genode.org

11–20 of 34 posts

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

#11
post #4
post #3

Earlier quoted context omitted.

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.

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

#13

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.

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

#14
post #12

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.

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

#15

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.

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

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

#16

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.

> 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

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

#17

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.

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.

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

#18

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.

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

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

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

#19
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

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

#20
post #12

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

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
Post reply on HN