Long term plan for GuixSD security: microkernels, ocap, RISC-V support

[Christopher Lemmer Webber]

Hello... reading over a few articles this morning:

 - Researchers Blame ‘Monolithic’ Linux Code Base for Critical
   Vulnerabilities
   
https://threatpost.com/researchers-blame-monolithic-linux-code-base-for-critical-vulnerabilities/136785/
 - Its associated paper:
   "The Jury Is In: Monolithic OS Design Is Flawed"
   http://ts.data61.csiro.au/publications/csiro_full_text/Biggs_LH_18.pdf
 - Brains behind seL4 secure microkernel begin RISC-V chip port
   https://www.theregister.co.uk/2018/04/23/risc_v_sel4_port/

I'm bringing this up because I want to plant the seed for some thinking
and conversation:

 - It's getting hard to trust our computers as in terms of our physical
   hardware.  Companies like Purism are helping to build blobless
   systems, but even then the hardware is built on un-auditable and
   with growing apparent insecurity (Spectre, Meltdown) with little
   chance of fixing things.  RISC-V has a libre instruction set, and in
   the long term I think we want to support that.

 - In terms of software, currently we run on ACL-heavy systems, which
   are well known to be insecure designs:
     http://waterken.sourceforge.net/aclsdont/current.pdf
   If a computer program behaves badly, it shouldn't be able to do any
   more damage than the smallest amount of authority it should need to
   run.  Currently programs run with the full authority of the user.
   This means that a tiny code flaw in even the most trivial package
   can lead to complete user compromise.

   In the long run, we'll want to support object capability based OS
   designs which follow the principle of least authority, so a program's
   vulnerabilities will be limited in scope.

 - What paths do we have forward on that last one?

   - Well, GNU Hurd is a microkernel + ocap system (while also trying
     to be POSIX compatible).  Manolis has done much good work in
     helping to make that a more feasible option for Guix users.

   - There's also seL4 which has a verified security kernel, possibly
     even seL4 with Genode.  I'm not sure how hard it will be to run
     POSIX type things on Genode.

   - There's also Google's recent work with Magenta/Fuschia.  From what
     I've read, architecturally this looks right.  I think the reason
     for worry here is the same difficulty the community has had to
     build actual community and libre distributions on top of the
     Android ecosystem could apply here.

 - It's also worth noting that the most common class of serious
   application / library vulnerabilities that we have to deal with is C
   / C++ memory management issues.  I'm not saying we should embrace
   everything getting ported to Rust, but I do think it's important to
   note that we're finally seeing paths out of that nightmare.

As a side note, if we don't have both together (libre hardware + ocap)
and we just have microkernel + ocap systems on top of proprietary
hardware, especially heavily "vendor controlled" systems, we could end
up much more screwed than we are even in our current systems, which is
why I think it's critical that we engage these things.  In the book
Rainbow's End (minor spoilers here) it's hinted that all the users are
running computers which have object capaiblity security and are thus
much more resilient to attacks, except that the bottom most layer of the
system is intentionally government compromised so that all systems are
effectively backdoored.  So, your sustem is secure... except for the
backdoor.

Anyway... the goal of this email was mostly just to try to get people
thinking about the direction we want to go long term.  Hope that's
useful/interesting even if it isn't an actual contribution of code
towards it ;)