Guix on a microkernel

[mikadoZero]

# Appreciation

I appreciate:

* many of Guix's design decisions.  The one that is relevant to this
  discussion is the kernel.  I like that Guix uses the linux-libre (no
  binary blobs) instead of the linux kernel.

* that work is underway to get Guix to work with GNU Hurd.  I like that
  a microkernel is a potential kernel option. 

  http://lists.gnu.org/archive/html/guix-devel/2016-12/msg00857.html

* the effort that has been put into GNU Hurd to get it to where it is.

* the bootsrapping initiative.

  https://bootstrappable.org/
  https://fosdem.org/2019/schedule/event/gnumes/

# Intent

* I would like to understand why GNU Hurd is being focused
  on (my perception) given other microkernel options. 
* I want to share what I have found after doing some looking into
  microkernels.
* I am curious what others think of microkernels.

I mention the appreciations above because I am aiming for a tone of
appreciation and curiosity and not a critical one.  The tone can be a
challenge for written communication. 

# My microkernel experience

Currently I do not have any practical experience using any microkernel.
I have just spent time looking into the topic as it is interesting to
me.

# Why microkernels?

I think Andrew Tanenbaum explains benefits of microkernel entertainingly
in this talk:
http://www.youtube.com/watch?v=bx3KuE7UjGA

The talks has a focus on Minix but I think the benefits are transferable
to other microkernels.

# GNU Hurd

## Perceived focus

I looks to me like there is a effort (which I appreciate) to get Guix
working on Hurd.  I get this perception from:

http://lists.gnu.org/archive/html/guix-devel/2016-12/msg00857.html

These comments from this thread:

https://lists.gnu.org/archive/html/help-guix/2019-03/msg00158.html

Ricardo Wurmus:  "Let’s work on the Hurd, people!  It’s beautiful!"

Jan Nieuwenhuizen: "FWIW the Mes port to the Hurd is ongoing and mes now
runs, next thing up is fork which we need for running mescc."

## Critiques of Hurd

I would be curious what people think about these third party critiques
(not mine) of Hurd.

### From X15

https://www.sceen.net/x15/

"Although the design of the Hurd is promising and attractive, its
implementation has a number of severe issues. X15 takes the approach of
the complete rewrite to make sure that key ideas are kept in mind at all
times during development. Since it’s not meant to be compatible with the
Hurd, critical interfaces such as IPC and signals can be re-implemented
completely differently. There is a lot of emphasis on code quality and
ease of maintenance, obtained from disciplined application of best
practices."

### From HelenOS

http://www.helenos.org/wiki/FAQ#HowisHelenOSdifferentfromGNUHurd

### Why Hurd?

Why the focus on Hurd given other microkernel options?  I ask this
question out of curiosity and a lack of practical experience with
microkernels.

# Microkernel wish list

These are things that I see as desirable in a microkernel.

## Free software

It should be completely free software.  No binary blobs included.  It
looks like all of the microkernel listed here are:
http://www.microkernel.info/

## RISC-V

RISC-V a free and open instruction set architecture is a nice complement
to a free operating system.  It is nice if a mircokernel already has
plans to run on RISC-V. 

Intel security issues:
https://libreboot.org/faq.html#intel

ARM security issues:
https://libreboot.org/faq.html#amd

### Entirely free RISC-V computers

These two initiatives are entirely free hardware based on RISC-V.

* HiFive Unleashed
  https://www.sifive.com/boards/hifive-unleashed

* lowRISC
  https://www.lowrisc.org

## Formal verification

An application of the minimality principle in the design of microkernel
leads to smaller code bases which are amenable to formal verification. 

https://en.wikipedia.org/wiki/Microkernel#Essential_components_and_minimality

I see the extra security assurance that formal verification provide as
desirable.

# Alternative microkernels

I used http://www.microkernel.info/ as the starting point when I began
looking into microkernels. 

## Summary of interesting microkernels

This is a high level summary based on the "Microkernel wish list" above.
All of these are free software.  I am likely missing some other
interesting microkernel projects.

| projects     | RISC-V efforts | Formal verification |
|--------------+----------------+---------------------|
| sel4.systems | Yes            | Yes                 |
| genode.org   | Yes            | Yes                 |
| helenos.org  | Yes            | No                  |
| muen.sk      | ?/No           | Yes                 |
| minix3.org   | ?/No           | No                  |
| hurd.gnu.org | ?/No           | No                  |

Note:

* ?/No is where (to me without asking) there does not look like there
  have been efforts to make the project work with RISC-V. 

* Genode is different than the others as it is not just a microkernel.
  I have given Genode Yes for both RISC-V and Formal verification
  because it can use the seL4 microkernel.  It can also use other
  microkernels beyond just seL4.

## Other interesting projects

robigalia.org:  based on seL4 microkernel which is formally verified and
has RISC-V efforts underway.  It is using Rust to build the parts that
would normally be part of a monolithic kernel in user space.  It looks
like a young project.

redox-os.org:  Rust based microkernel project.  It looks like a young
project. 

## Projects I have not looked into

I have not looked at the following projects which were also listed on
http://www.microkernel.info/ 

* github.com/Nils-TUD/Escape
* github.com/f9micro
* l4re.org
* github.com/TUD-OS/M3
* hypervisor.org