Live data from Hacker News

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

genode.org

1–10 of 34 posts

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

#3

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-...

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

#4
post #3

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.

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

#6
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.

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

#7

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

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

#8
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."

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

#10
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...

Post reply on HN