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.

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