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.
Genode OS: A tool kit for highly secure special-purpose operating systems
11–20 of 34 posts
Re: Genode OS: A tool kit for highly secure special-purpose operating systems
#12https://genode.org/download/sculpt
And some eye candy:
Re: Genode OS: A tool kit for highly secure special-purpose operating systems
#13I 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:
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
#14It'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
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
#15An 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.
Re: Genode OS: A tool kit for highly secure special-purpose operating systems
#16An 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.
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
#17An 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
#18An 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
#19https://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:
Re: Genode OS: A tool kit for highly secure special-purpose operating systems
#20It'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