Dan Connolly's tinkering lab notebook

Toward capabilities all the way down with Genode on a Thinkpad

In this year's holiday lull, I got closer to a "capabilities all the way down" workstation using Genode, an OS framework with capability-based security.

Sculpt is a Genode-based general-purpose OS.

Sculpt system overview

Genode has a choice of low level microkernels at the bottom. Sculpt uses the NOVA microhypervisor:

... the NOVA microhypervisor uses a capability-based authorization model and provides only basic mechanisms for virtualization, spatial and temporal separation, scheduling, communication, and management of platform resources.

NOVA isn't formally verified like seL4, but it's tiny (9,000 LOC):

figure 1
Figure 1: Comparison of the TCB size of virtual environments. -- Steinberg 2010

... not to mention mature: that peer-reviewed release was in 2010 and the spec last changed in 2014. It's clearly trustworthy enough for my hobby usage.

For reference, genode sculpt-22.10 ports/nova.port points to NOVA a34076e, modified Sep 29. So they do continue to make the occasional tweak here and there to the C++ code... prompted by Sculpt usage, I suspect.

The Sculpt release notes include a tutorial on how to boot it from a USB drive and play around with it; I managed to get that far back in 2018. This time, I got a more clear understanding of how persistent configuration on a partition of the USB drive works. A big clue is that the built-in "inspect" view is plenty for command-line file manipulation; there's no need to install and configure all the components of a shell.

I wanted to reproduce Schlatow's results from Starting an existing Linux installation from Sculpt. I managed to

  1. partition the hard drive
    • considered nix declarative disk partitioning with disko a la McGee's notes
      • learned a bit more about nix flakes
      • tried to make my own flake; re-discovered my problem with nix: unlike apt where if you get an option wrong, some C code tells you that you got an option wrong, nix just passes the wrong option down into interpreted code where you eventually get “string found where integer expected” or some such. As Phil Karlton would say, "yet another interpreted language without a debugger."
  2. install linux on the internal SDD
  3. install genode on another partition
    • though I couldn't get the grub config to work automatically

and I downloaded the components to run a VM, but when I tried to start it up, it couldn't find /machine.vbox6:

[runtime] child "vbox6"
[runtime]   RAM quota:  4402952K
[runtime]   cap quota:  7966
[runtime -> vbox6 -> vbox] main     Executable:  /virtualbox6
[runtime -> vbox6 -> vbox] Error: failed to init machine from settings
[runtime -> vbox6 -> vbox] Runtime error opening '/machine.vbox6' for reading: -102 (File not found.).
[runtime -> vbox6 -> vbox] /data/depot/genodelabs/src/vbox6/2022-10-11/src/virtualbox6/src/VBox/Main/src-server/MachineImpl.cpp[499] (nsresult Machine::initFromSettings(VirtualBox*, const com::Utf8Str&, const com::Guid*))
[core] attempted exec at non-executable memory (EXEC pf_addr=0x271dd78 pf_ip=0x271dd78 from pager_object: pd='init -> runtime -> vbox6 -> vbox' thread='ep') 
[core] page fault, pd='init -> runtime -> vbox6 -> vbox' thread='ep' cpu=0 ip=0x271dd78 address=0x271dd78 stack pointer=0x403fe6b8 qualifiers=0x15 IrUwP reason=3
[core] no RM attachment (READ pf_addr=0x0 pf_ip=0x16bb302 from pager_object: pd='init -> runtime -> vbox6 -> vbox' thread='Watcher') 
[core] page fault, pd='init -> runtime -> vbox6 -> vbox' thread='Watcher' cpu=0 ip=0x16bb302 address=0x0 stack pointer=0x409feb00 qualifiers=0x4 irUwp reason=1

After a a bit of diigoing, I came to the conclusion that there's a significant gap in my education around using VirtualBox in general, never mind in Genode.