Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

genode.org

Post reply on HN
Print view View original

21–30 of 34 posts

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

#21

Post by Koshkin »

jcelerier wrote: post #16
AnaniasAnanas wrote: post #2

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

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

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

#22

Post by yellowapple »

DyslexicAtheist wrote: post #13
Timothycquinn wrote: post #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."

> 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://twitt…

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

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

#24

Post by lsofzz »

akavel wrote: 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 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

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

#25

Post by chelmuth »

lsofzz wrote: post #24
akavel wrote: 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 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…

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

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

#26

Post by doener »

mey wrote: post #7
im_down_w_otp wrote: post #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.

sel4.systems appears to be down currently

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

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

#27

Post by posix_me_less »

nickpsecurity wrote: post #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

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?)

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

#28

Post by doener »

Timothycquinn wrote: post #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."

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

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

#29

Post by heavenlyhash »

DyslexicAtheist wrote: post #13
Timothycquinn wrote: post #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."

> 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://twitt…

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

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

#30

Post by renox »

casual_slacker wrote: post #17
martin1975 wrote: post #15

Earlier quoted context omitted.

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

Post reply on HN