seL4 Microkernel: How small can the shim be?

Liam,

The reason I keep coming back to this is the complexity of modern OS
threats and requirements and the desire to spend less of my time here.

The core drivers of the seL4 API are (from
https://microkerneldude.wordpress.com/ ; good reads here BTW):

Verification
------------
-Minimality  [* Small _IS_ beautiful ! *]
-Policy freedom
-Performance
-Security
-Don’t pay for what you don’t use

Then there are a few non-goals:
------------------------------
-Stopping you from shooting yourself in the foot [*systems programmers
have to aim through their heads;^]
-Ease of use  [*we can help here*]
-Hardware abstraction [*we should be able to help here*]

So starting with a minimalist open source microkernel running drivers,
servers, apps as hot swapable Smqlltalk runtime components in separate
user-land address spaces with _fast_ IPC makes sense to me as a
strategy.

If the systems architecture is right and there is enough interest, we
can drill down to the bottom level, but in the mean time we can devise
and experiment without getting bogged down learning the details of tying
our shoelaces before the big race.

My thought is to have a copy-on-write core (I am thinking again or
something like the Bee DMR binary core here) with a system naming
service that is used to intern all selectors, so IPC uses common
selector keys.  Capabilities map to Smalltalk objects in their home
address spaces (note
http://mumble.net/~jar/pubs/secureos/secureos.html).

So code+component(s) = driver or service with core just copy-on-write
(with resilient live update).

I would think that all of this maps into (perhaps grad level) student
projects as well, so [a] we can get a bit of "free labor" boost plus [b]
more beginning and advanced students get exposed to Smalltalk and the
ideas of the community.

$0.02,
-KenD

On Wed, 24 Feb 2021 at 17:40, <[hidden email]> wrote:
>
> Liam,
>
> The reason I keep coming back to this is the complexity of modern OS
> threats and requirements and the desire to spend less of my time here.
>
> The core drivers of the seL4 API are (from
> https://microkerneldude.wordpress.com/ ; good reads here BTW):
[...]
> I would think that all of this maps into (perhaps grad level) student
> projects as well, so [a] we can get a bit of "free labor" boost plus [b]
> more beginning and advanced students get exposed to Smalltalk and the
> ideas of the community.

:-D

Some excellent points there.

I was and am slightly aware of the seL4 µkernel, but I did not
seriously consider it.

I want to stress that I am not really an expert in this stuff, merely
an interested dilettante! But few people seem to be considering new OS
designs these days, so I thought that maybe this amateur could make
some interesting points.

So, my reasoning for suggesting Oberon and specifically A2:

• I really wanted a total and clean break from C and C-based designs;
something really different.

• I was hoping for a type-safe, memory-managed compiler suitable for
low-level and kernel work – and I found one in Oberon.

• A2 is a complete OS, with multicore support, TCP/IP stack, working
USB drivers, things like that, not just a kernel. It also provides a
compiler and rudimentary sort of IDE suitable for writing new drivers
in. L4 is just a microkernel and needs an OS building around it, as I
understand it.

• I do not know much about the whole L4 family but what little I know
some of the existing OSes based upon them were very vaguely Unix-ish.
That's precisely what I'm trying to move away from.

• I do not know if SEL4 has working multiprocessor support. I know
that QNX does, which demonstrates that a Unix-like true microkernel
can do this; but I also believe that Minix 3 so far lacks one, and
lacks some APIs needed for POSIX and xNix compatibility. This is not
an easy thing to do.

• This is wild supposition on my part, but I wonder if the traditional
C language's design and features, and the design philosophy of xNix,
its design of separate isolated execution environments which mainly
exchange data through the filesystem or IPC mechanisms, make things
like microkernels seem like a desirable design: to extend this
compartmentalisation right down into the kernel itself.

Plan 9's developers originally intended to replace C with Aleph, but
in the end abandoned that approach but applied much stricter standards
to Plan 9 C than ordinary xNix/Linux C. I have read 1 isolated comment
lacking more context that the design of Plan 9 makes considerations of
microkernels largely irrelevant, but I do not know how or why that
might be. I would very much like to know.


--
Liam Proven – Profile: https://about.me/liamproven
Email: [hidden email] – gMail/gTalk/gHangouts: [hidden email]
Twitter/Facebook/LinkedIn/Flickr: lproven – Skype: liamproven
UK: +44 7939-087884 – ČR (+ WhatsApp/Telegram/Signal): +420 702 829 053