From mboxrd@z Thu Jan 1 00:00:00 1970 From: David Craven Subject: Microkernel & guix Date: Wed, 21 Dec 2016 13:26:42 +0100 Message-ID: Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:49099) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1cJfyr-00079Q-4s for help-guix@gnu.org; Wed, 21 Dec 2016 07:26:50 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1cJfyn-0002SQ-8K for help-guix@gnu.org; Wed, 21 Dec 2016 07:26:49 -0500 Received: from mail-qk0-x235.google.com ([2607:f8b0:400d:c09::235]:34205) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1cJfyn-0002Ro-3k for help-guix@gnu.org; Wed, 21 Dec 2016 07:26:45 -0500 Received: by mail-qk0-x235.google.com with SMTP id q68so79829121qki.1 for ; Wed, 21 Dec 2016 04:26:43 -0800 (PST) List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-guix-bounces+gcggh-help-guix=m.gmane.org@gnu.org Sender: "Help-Guix" To: help-guix@gnu.org Hi, So I assume that many have already heard of the SEL4 microkernel that contains a (~full) correctness proof (equivalence to the Haskell functional model) and proof of various interesting properties including confidentiality and integrity of the IPC communication and worst case execution time for hard real time guarantees. [0] Some other interesting developments in the OS scene is the Genode operating system [1]. Genode is an implementation of the user-space part of a microkernel based OS. It supports various microkernels including the SEL4 and a handful of other microkernel implementations. It has a driver execution environment for repurposing Linux drivers, iPXE drivers and NetBSD drivers and provides a POSIX interface to existing applications. I think at some point it would be nice to start thinking about how guix and genode could complement each other. Work is being done on exploring how nix can help genode with it's "package management problems" [2]. I suggest waiting to see what develops from that first. Just thought I'd share in case someone is interested :) And make sure that Guix devs stay on top of current developements =P [0] https://github.com/seL4/seL4 [1] https://github.com/genodelabs/genode [2] https://github.com/ehmry/genode-nix