Genode OS: A tool kit for highly secure special-purpose operating systems • Hacker News Board

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

#31

Post by lsofzz » Tue, Jan 22, 2019, 1:12 PM UTC

chelmuth wrote: post #25

lsofzz wrote: post #24

Earlier quoted context omitted.

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

Nice. This got me going

$ qemu-system-x86_64 -name guest=humbug,debug-threads=on -drive file=/var/lib/libvirt/images/sculpt-vc.qcow2 -machine q35 ....

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

#32

Post by nickpsecurity » Tue, Jan 22, 2019, 11:08 PM UTC

posix_me_less wrote: post #27

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

I haven't used the recent version. Try it out. Tell us how well it works or doesnt. Preferably on hardware you know is supported.

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

#33

Post by nickpsecurity » Tue, Jan 22, 2019, 11:13 PM UTC

Koshkin wrote: post #21

jcelerier wrote: post #16

Earlier quoted context omitted.

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

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.

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

#34

Post by lsofzz » Wed, Jan 23, 2019, 8:15 AM UTC

posix_me_less wrote: post #27

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

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

I loved the ViM though ;)