Muen and Qubes Odyssey

[Alfonso De Gregorio]

Hello,

Does anybody have explored the possibility of using Muen Separation
Kernel [1] as yet another isolation backend for Qubes?

Muen is a GPL licensed micro kernel written in SPARK [2, 3]. It aims
at preventing/mitigating possible covert channels (e.g., implementing
cache coloring mechanism) and to prove the absence of some types of
runtime errors. In Muen guest software is isolated using Intel VT
(VT-{x,EPT,d}).

A Muen driver for libvirt should give to Qubes HAL the means to
provide a different security/hardware-compatibility tradeoff.

How many of you would prefer Muen to Xen as the underlying VMM to Qubes?

[1] Muen Separation Kernel, http://www.muen.sk/
[2] Reto Buerki and Adrian-Ken Rueegsegger, Muen - An x86/64
Separation Kernel for High Assurance, project report,
http://muen.codelabs.ch/muen-report.pdf
[3] Reto Buerki and Adrian-Ken Rueegsegger, Muen - An x86/64
Separation Kernel for High Assurance, slides,
http://muen.codelabs.ch/muen-slides.pdf

-- alfonso

@secYOUre

[Joanna Rutkowska]

Whenever introducing some new kernel/hypervisor discussion, I strongly
suggest to include answers to the following questions first:

0) What kind 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)?

1) Does it require specially written/build applications (e.g. patched
Fierfox)?

2) Does it require custom drivers or can use Linux/Windows ones?

3) Does it support VT-d and does it allow to create untrusted driver
domains?

4) Does it support S3 sleep?

5) Does it work on multiple CPUs/Chipstes?

6) 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)

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

Here are the answers for Xen 4.1 that we use:

0) PV and HVM Virtual Machines (ring0/3 for PV domains, VT-x/AMD-v for HVMs)
1) Runs unmodified usermode apps (binaries)
2) Runs unmodified Linux drivers (dom0 and driver domains) PV VMs
require special written pvdrivers.
3) Full VT-d support including untrusted driver domains
4) S3 sleep supported well
5) Works on most modern CPUs/Chipsets
6) Biggest performance hit on disk operations (especially in Qubes when
complex 2-layer mapping used for Linux AppVMs), no GPU virtualization
7) Mostly Works (TM) :)

Perhaps we could have a wiki page with a table summarizing various
hypervisor, kernel and other isolation technologies (e.g. Linux kernel
w/ LXC)?

joanna.

[7v5w7go9ub0o]

Heh....ISTM that your reply, under the title "What about other
hypervisors?", already constitutes that wiki page.

Perhaps replace your first sentence ( "Whenever introducing some new
kernel/hypervisor.......")

with

"We want Qubes to be as good as it can be and welcome your suggestions.
Below summarized is our overview of Xen; please submit any suggestions
for a better hypervisor along with a similar overview - responding to
the specific questions:"

[Alfonso De Gregorio]

Muen is an experimental technology. At the current stage it lacks most
of the features provided by Xen -- it will suffice to say that:
1. The Linux kernel cannot run as a Muen subject, yet (*).
2. While some resources can be accessed using port an memory-mapped
I/O, there is no PCIe virtualization.
Hence, trying to assess the suitability of Muen as an isolation
backend solely on the basis of its current maturity would be a losing
proposition. We should look at what Muen might become in the future.

That is to say that the reason for asking to Qubes developers about
their potential interest in supporting Muen ensues from the desire to
understand if a contribution to this new microkernel might bring a new
hypervisor to Qubes in the first place.

*) As far as the memory management goes, in Muen it is possible to run
unmodified guest OS. However there are still unresolved issues related
to the Linux boot process.

-- alfonso

@secYOUre

[Adrian-Ken Rueegsegger]

Hello,

[ Disclaimer: I am one of the developers of the Muen kernel ]

On 04/28/2014 04:09 PM, Alfonso De Gregorio wrote:
> Muen is an experimental technology. At the current stage it lacks most
> of the features provided by Xen -- it will suffice to say that:
> 1. The Linux kernel cannot run as a Muen subject, yet (*).

Muen is actually able to run Linux as a subject, see [1].

> 2. While some resources can be accessed using port an memory-mapped
> I/O, there is no PCIe virtualization.

We have experimental branches which implement PCI-Passthrough and VT-d
support. Coincidentally, integration of these features into the main
development branch is next up on our todo list.

> Hence, trying to assess the suitability of Muen as an isolation
> backend solely on the basis of its current maturity would be a losing
> proposition. We should look at what Muen might become in the future.

Muen is a young project and is currently under very active development.

The main difference to Xen is that the Muen Separation Kernel is
designed to be a special purpose Microkernel targeting high assurance
use cases.

The objective of an SK is to enforce strict component isolation.
Information flow between components is only permitted if specified by a
system policy. All functionality not absolutely necessary to implement
the separation of components (i.e. virtual machines) is not part of the
kernel.

Muen is much more static since a system has to be completely specified
in a policy at integration time. The policy makes resource allocation
explicit and allowed us to omit complicated resource management
functionality from the kernel.

Advanced Intel virtualization features such as Extended Page Tables
(EPT) greatly simplified the kernel implementation. In contrast to other
hypervisors Muen requires these hardware features since it was designed
with their availability in mind. This greatly contributed to a clean
design and spared us from the complexities and problems of emulating
such mechanisms in software.

As a consequence of this design, the code size of the Muen kernel is
orders of magnitudes smaller than Xen (we consider Dom0 part of the
TCB). Currently the kernel is composed of ~2'600 SLOC of SPARK and ~200
SLOC of assembly (system boot only).

SPARK is a precisely defined high-level programming language designed
for implementing high integrity systems. It is based on Ada, which is
itself a programming language with a strong focus on security and
safety. The use of SPARK allowed us to formally prove that the kernel
contains no runtime errors at the source code level.

[...]

> *) As far as the memory management goes, in Muen it is possible to run
> unmodified guest OS. However there are still unresolved issues related
> to the Linux boot process.

We are not aware of any Linux boot issues. Could you please elaborate?

Regards,
Adrian

[1] - https://groups.google.com/forum/#!topic/muen-dev/TFPsXHfV2zU

[Alfonso De Gregorio]

On Mon, Apr 28, 2014 at 4:10 PM, Adrian-Ken Rueegsegger <k...@codelabs.ch> wrote:
...
>> *) As far as the memory management goes, in Muen it is possible to run
>> unmodified guest OS. However there are still unresolved issues related
>> to the Linux boot process.
>
> We are not aware of any Linux boot issues. Could you please elaborate?

Absolutely. This contrasts with what reported in section 6.2.2 of the
thesis published at http://muen.codelabs.ch/muen-report.pdf

6.2.2. Linux Subjects
Porting the Linux kernel to run as a subject on the Muen
separation kernel would enable the execution of a large
number of Linux user-space applications. This would
drastically increase the number of real world use-cases,
that a system using the Muen kernel could be applied to.
Leveraging the VM profile, which allows a subject to perform
memory management via EPT (see section 2.3.1.2), reduces
the porting effort. Changes to the Linux boot process are needed,
since it is quite involved. The Linux kernel implements an
architecture-dependent boot protocol that is explained as part
of the kernel documentation .

Am I missing something here?

> Regards,
> Adrian
>
> [1] - https://groups.google.com/forum/#!topic/muen-dev/TFPsXHfV2zU

-- alfonso

@secYOUre

[Adrian-Ken Rueegsegger]

Hi,

The report is dated August 29, 2013. Development has continued at a
steady pace since then so there have been many improvements over past
seven months. The previously mentioned announcement [1] to the muen-dev
mailing list sent out this February lists the newly implemented features
among which is Linux support.

[Alfonso De Gregorio]

On Mon, Apr 28, 2014 at 4:58 PM, Adrian-Ken Rueegsegger <k...@codelabs.ch> wrote:
...

> The report is dated August 29, 2013. Development has continued at a
> steady pace since then so there have been many improvements over past
> seven months. The previously mentioned announcement [1] to the muen-dev
> mailing list sent out this February lists the newly implemented features
> among which is Linux support.

I am glad to be proven wrong regarding the Linux VM support, I
congratulate with the Muen team for the work done so far, and I
welcome any improvement that makes us closer to the integration of
Muen and Qubes.

> Regards,
> Adrian
>
> [1] - https://groups.google.com/forum/#!topic/muen-dev/TFPsXHfV2zU

-- alfonso

@secYOUre

[Joanna Rutkowska]

On 04/28/14 18:10, Adrian-Ken Rueegsegger wrote:
> Hello,
>
> [ Disclaimer: I am one of the developers of the Muen kernel ]
>

Thanks for dropping by :)

> On 04/28/2014 04:09 PM, Alfonso De Gregorio wrote:
>> Muen is an experimental technology. At the current stage it lacks most
>> of the features provided by Xen -- it will suffice to say that:
>> 1. The Linux kernel cannot run as a Muen subject, yet (*).
>
> Muen is actually able to run Linux as a subject, see [1].
>
>> 2. While some resources can be accessed using port an memory-mapped
>> I/O, there is no PCIe virtualization.
>
> We have experimental branches which implement PCI-Passthrough and VT-d
> support. Coincidentally, integration of these features into the main
> development branch is next up on our todo list.
>
>> Hence, trying to assess the suitability of Muen as an isolation
>> backend solely on the basis of its current maturity would be a losing
>> proposition. We should look at what Muen might become in the future.
>
> Muen is a young project and is currently under very active development.
>

Would you mind providing short answers to the 6 basic questions I wrote
earlier in this thread?

> The main difference to Xen is that the Muen Separation Kernel is
> designed to be a special purpose Microkernel targeting high assurance
> use cases.
>
> The objective of an SK is to enforce strict component isolation.
> Information flow between components is only permitted if specified by a
> system policy. All functionality not absolutely necessary to implement
> the separation of components (i.e. virtual machines) is not part of the
> kernel.
>
> Muen is much more static since a system has to be completely specified
> in a policy at integration time. The policy makes resource allocation
> explicit and allowed us to omit complicated resource management
> functionality from the kernel.
>
> Advanced Intel virtualization features such as Extended Page Tables
> (EPT) greatly simplified the kernel implementation. In contrast to other
> hypervisors Muen requires these hardware features since it was designed
> with their availability in mind. This greatly contributed to a clean
> design and spared us from the complexities and problems of emulating
> such mechanisms in software.
>
> As a consequence of this design, the code size of the Muen kernel is
> orders of magnitudes smaller than Xen (we consider Dom0 part of the
> TCB). Currently the kernel is composed of ~2'600 SLOC of SPARK and ~200
> SLOC of assembly (system boot only).
>

I would argue that this is a wrong and unfair comparison, unless you
claim that one can build a desktop system based on Muen where:

1) The GUI subsystem (screen output, user input) would *not* be part of
the TCB,

2) Disk drivers and filesystem stacks would *not* be part of the TCB.

Unless you can do that (which you can't on x86, I'm pretty sure ;P) then
it is not fair to claim you are so damn slim and then compare yourself
with a complete desktop system's TCB (which includes the GUI subsystem,
disk backends, and power management)...

> SPARK is a precisely defined high-level programming language designed
> for implementing high integrity systems. It is based on Ada, which is
> itself a programming language with a strong focus on security and
> safety. The use of SPARK allowed us to formally prove that the kernel
> contains no runtime errors at the source code level.
>

Beware not to get too excited with formal proofs:

http://theinvisiblethings.blogspot.com/2010/05/on-formally-verified-microkernels-and.html

> [...]
>
>> *) As far as the memory management goes, in Muen it is possible to run
>> unmodified guest OS. However there are still unresolved issues related
>> to the Linux boot process.
>
> We are not aware of any Linux boot issues. Could you please elaborate?
>
> Regards,
> Adrian
>
> [1] - https://groups.google.com/forum/#!topic/muen-dev/TFPsXHfV2zU
>

Cheers,
joanna.

[senier.a...@gmail.com]

Hi Joanna,

On Monday, April 28, 2014 7:30:02 PM UTC+2, joanna wrote:

Would you mind providing short answers to the 6 basic questions I wrote
earlier in this thread?

I'll answer them if you don't mind (I'm involved closely with the design and implementation of Muen).

> 0) What kind 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)?

0) Everything — including native applications — are Intel VT-x VMs, the kernel runs in root mode/ring 0. VM Exits are mostly handled in applications outside the kernel.

> 1) Does it require specially written/build applications (e.g. patched
> Fierfox)?

1) Linux binaries run unmodified.

> 2) Does it require custom drivers or can use Linux/Windows ones?

2) Experimental PCI passthrough and VT-d exist and are on the roadmap for mainline. Once available, you can use stock Linux drivers. Some Linux drivers (like the console) are paravirtualized, though. There is no Windows support right now.

> 3) Does it support VT-d and does it allow to create untrusted driver
> domains?

3. See #2. Untrusted (PCI) driver domains are possible once VT-d and interrupt remapping are implemented (well, at least under certain assumptions, e.g. that your untrusted device cannot forge PCI cycles on behalf of a different device or your VT-d IO access rights are tight enough and all the other driver domains are careful when accessing their IO memory regions).

> 4) Does it support S3 sleep?

4. No. We have not looked into Power Management, yet.

> 5) Does it work on multiple CPUs/Chipstes?

5. Yes, I tested the demo on various Sandy Bridge, Ivy Bridge and Haswell systems. To be fair, there is not much chipset-dependent stuff in there, yet.

> 6) 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)

6. It has a static fixed-cyclic scheduler, which comes with the cost of wasting cycles even when the application/VM is idle. You can switch between different scheduling plans to adapt to different workloads, but you will still waste CPU time. OTHO this might be beneficial for power management (only a wild guess, see #4).

> 7) Other special features? E.g. eliminates cooperative covert channels
> between VMs?

7. Given the right configuration, it does limit certain covert channels (and side channels). The fixed cyclic scheduler mitigates those channels where a rogue application observes another applications behaviour and derives e.g. key material (like here [1]). Some other channels might be mitigated by a suitable system configuration (e.g. a virtual memory layout that partitions shared caches). As for other special features: The architecture allows for deprivileged full-virtualization, where all virtualization events are handled in a designated per-VM subject monitor. We do that for FV Linux.

The point this questionnaire (which I'm happy to answer ;-) is ignoring — Muen is not meant to support dynamic workloads like the ones Qubes has. It may or may not evolve into something more dynamic in the future. Muen is good for scenarios where you do security critical functions like network encryption, key management etc. in small, and rather static native applications and all the nasty stuff in VMs that interact with them.

Also note, that Muen deliberately has all its resources defined statically (e.g. there is no resource detection and allocation at boot time). We consider this a feature, not a bug. However, that requires a more embedded system-style development where you know your hardware very well at integration time. You cannot take an arbitrary PC (even when it has the right feature set) and expect your system to run on it without at least minor adjustments.

From that perspective we are really comparing apples and oranges here…

All the best
Alex

[1] http://eprint.iacr.org/2010/594.pdf

[Joanna Rutkowska]

So, just out of curiosity -- how do you see your kernel adopted in
practice? I.e. in what kind of products? Embedded, single-purpose,
crypt-related devices only? Anything else?

Also, how do you estimate the bandwidth of the _cooperative_ covert
channels that are/will still be possible with your kernel? How would you
relate those to the bandwidth for covert channels possible in a
hypervisor like Xen [*]?

joanna.

[*] Assuming we can disable the trivial channels via legal (or
quasi-legal) APIs, such as two VMs creating a shared memory by guessing
grant references, as was discussed in some other thread recently.

[Adrian-Ken Rueegsegger]

Hello Joanna,

On 04/28/2014 07:30 PM, Joanna Rutkowska wrote:
> On 04/28/14 18:10, Adrian-Ken Rueegsegger wrote:

[...]

>> As a consequence of this design, the code size of the Muen kernel
>> is orders of magnitudes smaller than Xen (we consider Dom0 part
>> of the TCB). Currently the kernel is composed of ~2'600 SLOC of
>> SPARK and ~200 SLOC of assembly (system boot only).
>
> I would argue that this is a wrong and unfair comparison, unless
> you claim that one can build a desktop system based on Muen where:
>
> 1) The GUI subsystem (screen output, user input) would *not* be
> part of the TCB,
>
> 2) Disk drivers and filesystem stacks would *not* be part of the
> TCB.
>
> Unless you can do that (which you can't on x86, I'm pretty sure ;P)
> then it is not fair to claim you are so damn slim and then compare
> yourself with a complete desktop system's TCB (which includes the
> GUI subsystem, disk backends, and power management)...

Xen provides much more functionality and contrary to Muen it is a
general purpose hypervisor which can support all sorts of use cases.
However it is my understanding that Dom0 is an integral part of any
system built with Xen. That is to say that all the code running in
Dom0 including the Dom0 kernel is always part of any TCB. This is
problematic in certain use cases, see e.g. OpenMirage Unikernel [2]
(section 5.3). But as Alex mentioned in his reply it is kind of an
apples and oranges comparison.

>> SPARK is a precisely defined high-level programming language
>> designed for implementing high integrity systems. It is based on
>> Ada, which is itself a programming language with a strong focus
>> on security and safety. The use of SPARK allowed us to formally
>> prove that the kernel contains no runtime errors at the source
>> code level.
>
> Beware not to get too excited with formal proofs:
>
> http://theinvisiblethings.blogspot.com/2010/05/on-formally-verified-microkernels-and.html

We
>
have been careful with the wording and the use of the term 'formal
verification'. I am convinced that our project has benefited from the
employed methods and programming language. I agree with what you say
in your blog post that formal verification is *not* a silver bullet
(since there is none). At the same time I also agree with the comment
Gerwin made [2] that there is an actual gain from employing formal
methods even if it means we have to invest additional effort.

Regards,
Adrian

[1] - http://nymote.org/docs/2013-asplos-mirage.pdf
[2] -
http://theinvisiblethings.blogspot.ch/2010/05/on-formally-verified-microkernels-and.html?showComment=1273787941706#c5663920830714525309

[Joanna Rutkowska]

On 04/30/14 00:02, Alexander Senier wrote:

> On Tue, 29 Apr 2014 01:15:17 +0200
> Joanna Rutkowska <joa...@invisiblethingslab.com> wrote:
>
>> So, just out of curiosity -- how do you see your kernel adopted in
>> practice? I.e. in what kind of products? Embedded, single-purpose,
>> crypt-related devices only? Anything else?
>

> We currently build it with security appliances (secure thin-clients,
> VPN gateways) in mind. I would not exclude other use cases, but this
> out of scope for us at the moment.
>

Sure, make sense.

>> Also, how do you estimate the bandwidth of the _cooperative_ covert
>> channels that are/will still be possible with your kernel? How would
>> you relate those to the bandwidth for covert channels possible in a
>> hypervisor like Xen [*]?
>

> I have no good answer to that question, as we have not quantified those
> channels (yet). Some covert channels (e.g. those relying on an influence
> of the application/VM on the scheduler) may vanish completely, others
> are probably hard to mitigate at all (e.g. branch prediction cache).
> It would be an interesting analysis, though.
>

It surely would.

joanna.

[Alexander Senier]

On Tue, 29 Apr 2014 01:15:17 +0200
Joanna Rutkowska <joa...@invisiblethingslab.com> wrote:

> So, just out of curiosity -- how do you see your kernel adopted in
> practice? I.e. in what kind of products? Embedded, single-purpose,
> crypt-related devices only? Anything else?

We currently build it with security appliances (secure thin-clients,
VPN gateways) in mind. I would not exclude other use cases, but this
out of scope for us at the moment.

> Also, how do you estimate the bandwidth of the _cooperative_ covert
> channels that are/will still be possible with your kernel? How would
> you relate those to the bandwidth for covert channels possible in a
> hypervisor like Xen [*]?

I have no good answer to that question, as we have not quantified those
channels (yet). Some covert channels (e.g. those relying on an influence
of the application/VM on the scheduler) may vanish completely, others
are probably hard to mitigate at all (e.g. branch prediction cache).
It would be an interesting analysis, though.

Regards
Alex

[Noah Vesely]

Just to give an update on this, it seems Muen has now integrated PCI passthrough w/ Intel VT-d. Although, they still say it is not ready for production use.

I am very interested to see where Qubes and Muen will be 2 years from now. It would be great if it were possible to offer Qubes with Muen, despite the lesser functionality it will probably still have vis-a-vis Xen (and also increased difficulty and hardware-specificity of set-up). I refer specifically to Alex's post earlier:

"Muen is not meant to support dynamic workloads like the ones Qubes has. It may or may not evolve into something more dynamic in the future. Muen is good for scenarios where you do security critical functions like network encryption, key management etc. in small, and rather static native applications and all the nasty stuff in VMs that interact with them.

Also note, that Muen deliberately has all its resources defined statically (e.g. there is no resource detection and allocation at boot time). We consider this a feature, not a bug. However, that requires a more embedded system-style development where you know your hardware very well at integration time. You cannot take an arbitrary PC (even when it has the right feature set) and expect your system to run on it without at least minor adjustments."

I'll keep an eye out on this project.

[Noah Vesely]

In case anyone is interested, they have their own Google Group muen-dev https://groups.google.com/forum/#!forum/muen-dev