Re: [MirageOS-devel] Qns about Unikernels/hypervisors/baremetal/security

[Hannes Mehnert <hannes@xxxxxxxxxxx>]

On 04/02/2017 17:29, Michael Bright wrote:
> [deleted stuff covered in mort's reply]
>
> How can we be sure about the Hypervisor security.

well, we can't. ;)  while I don't run any verified hypervisor, there's
at least some academic work:
 - L4 http://sel4.systems/
 - "A Formally Verified Static Hypervisor with Hardware Support for a
Many-Core Chip" (Euro-PAR 2013)
 - "Combining Mechanized Proofs and Model-Based Testing in the Formal
Analysis of a Hypervisor" FM 2016
 - "Machine code verification of a tiny ARM hypervisor" TrustED 2013

> Are there any comparisons of security between Xen, kvm, hyper-v, esxi ?

Xen was a pioneer, and includes hardware emulation code which is
nowadays done by hardware (e.g. EPT, VT-d).  Newer hypervisors (kvm I
suspect, FreeBSD bhyve (I use this to run MirageOS), OpenBSD vmm, etc.)
require these hardware features, and thus have less code. :)

> I see we talk about "potential" security improvements - due to less LOC,
> due to easier to understand code (because of less LOC).
> Are there any studies/figures to support this position?

It is less code, and all written in a sane programming language with
compile time guarantees, expressed as types.  If you restrict yourself
to a certain coding style (to explicitly express all effects via types),
you can get to code which is easier to understand locally -- my point of
view is that Mirage3 is here a good step forward.

You might want to read our usenix security paper on nqsb-tls
(https://usenix15.nqsb.io) - hosted as a MirageOS unikernel - which
covers some security and programming style features, and contains some
empirical data to give some evidence.


hannes

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel