Raising the level of abstraction of the discussion somewhat, I’d say that the traditional notion of a “shell” is really a command-line interface (aka primitive UI) to an OS’es syscall interface. This is certainly how the Unix shell started out (before it was turned into a full programming language and the kitchen sink).

Viewed that way, it’s clear that such a minimalist notion of a shell makes not much sense for a microkernel like seL4. Having a US to deal with raw caps doesn’t buy you much, and besides, you don’t even have the system services to implement that UI.

Hence, you need a layer of system services between the shell and the kernel. You’ll want at least a process concept, a concept of I/O (which in seL4 doesn’t exist at all) and communication that’s more than a few raw bytes and caps. In short, you need a minimal OS personality.

Matt has outlined one way to do it. Our Advanced OS course (https://www.cse.unsw.edu.au/~cs9242/19/project/) builds a simple OP personality on seL4, and a shell to drive it. That shell looks quite different from what Matt’s shell would look like.

Basic observation is then that a shell will be strongly tied to the OS personality on which it is based, and that OS personality will define a whole lot of policies on how the system and its resources are managed. In that sense, there cannot be a unique “seL4 shell”. But for any OS personality you build, you’d almost certainly want a shell.

Gernot

PS: This is probably one for our FAQ...