Use verified L4 kernel instead of Xen

[GWeck]

Qubes OS version:

Far in the Future

Affected component(s):

mainly dom0

---

Steps to reproduce the behavior:

Expected behavior:

Actual behavior:

General notes:

The security of Qubes critically depends on strong isolation provided by Xen. Bugs in Xen endanger the security of Qubes significantly. Possibly the security kernel of L4 (os.inf.tu-dresden.de/L4/) might be used instead of Xen, if vchan and qrexec could be implemented in L4 without too much effort. As L4 is used in very security critical projects, e.g. a filter gateway connecting NATO secret systems to the outside world (https://www.infodas.de/wp-content/uploads/2016/11/SDoT_6.0i_eng_170530.pdf), it is to be expected that using L4 would significantly reduce the risks posed in Xen by bugs.

I think it would be worth while to contact the Technical University of Dresden on this issue. As far as I know, they are currently looking at Qubes and should be interested in a cooperation with the Qubes team. If interested, please contact Prof. Härtig (haertig@os.inf.tu-dresden.de).

---

Related issues:

[wom-bat]

You should probably look at seL4 https://seL4.systems/ if you want a proven secure foundation.

[marmarek]

See https://www.qubes-os.org/faq/#what-about-this-othernew-microkernelhypervisor

[GWeck]

The L4 development team answered the questionnaire as to which features necessary for porting Qubes to another microkernel als follows:
From: Adam Lackorzynski adam@os.inf.tu-dresden.de
Subject: Re: Fwd: [QubesOS/qubes-issues] Use verified L4 kernel instead of Xen (#3894)
Date: 26. September 2018 at 18:33:51 CEST
To: Hermann Härtig haertig@os.inf.tu-dresden.de
On Wed Sep 26, 2018 at 17:25:57 +0200, Hermann Haertig wrote:

1. What kinds of containers does it use for isolation? Processes? PV VMs? Fully virtualized VMs (HVMs)? And what underlying h/w technology is used (ring0/3, VT-x)?
   Fully virtualized VMs (VT-x, AMD-v). Or PV (ring0/3)

2. Does it require specially written/built applications (e.g. patched Firefox)?
   Runs unmodified usermode apps (binaries).

3. Does it require custom drivers, or can it use Linux/Windows ones?
   Does not require custom drivers, but can be added for special
   functionality.

4. Does it support VT-d, and does it allow for the creation of untrusted driver domains?
   Yes, and yes.

5. Does it support S3 sleep?
   Yes.

6. Does it work on multiple CPUs/Chipsets?
   Yes

7. What are the performance costs, more or less? (e.g. “XYZ prevents concurrent execution of two domains/processes on shared cores of a single processor”, etc.)
   Typical performance costs due to virtualization.

8. Other special features? E.g. eliminates cooperative covert channels between VMs?

• Microhypervisor based on capability-system
• Built on OS framework, allows for hypervisor/microkernel applications
• real-time capable
• Supports x86, ARM and MIPS
• ...

Adam

From this, it seems that porting should be possible, even without too much effort.
Supporting the L4 kernel might help in building Qubes-based systems in German government projects.

[GWeck]

I just provided the answers to the questionnaire as a comment in the github issue #3894 The L4 team is quite interested, but - like so many of us, lacks decent time. _____________________________________________________________________ Dr. Gerhard Weck Franz-Rüth-Str. 2d 50374 Erftstadt Tel. 02235/44747 E-Mail: GerhardWeck@onlinehome.de

…

_____________________________________________________________________ Am 18.09.2018 um 00:12 schrieb Marek Marczykowski-Górecki: See https://www.qubes-os.org/faq/#what-about-this-othernew-microkernelhypervisor — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[cfcs]

@GWeck
if vchan and qrexec could be implemented in L4 without too much effort

It seems to me that if no one can be bothered to do it, it is actually "too much effort."

You could also argue that Genode or Muen would be better than Xen, or that GNU/Herd would be, or that we should retarget to run in QNX. So far nobody but the Qubes team has actually come up with a practical implementation.

If you want to see HAL or Qubes on other platforms than Xen, you should dedicate the time to implement the required feature set (namely shared memory and a stream/message-based primitive), or find funding or people to do that.

As this is an L4 issue, and not a Qubes issue, I believe this issue here should be closed so it doesn't clutter the issue tracker.

[andrewdavidwong]

As this is an L4 issue, and not a Qubes issue, I believe this issue here should be closed so it doesn't clutter the issue tracker.

Leaving it open for now to give the Qubes devs time to consider and decide what to do with it.

[DemiMarie]

seL4 does have a vchan implementation, at least.

[cfcs]

We couldn’t find any code matching 'vchan' in seL4/seL4
@DemiMarie please post a source.

[DemiMarie]

@cfcs https://github.com/seL4/seL4_libs/blob/c7e4a85edc3048979fbc962ace2dbe657e8d0b3c/libsel4vmm/include/vmm/libvchan.h

Based on the original QubesOS code, too.