Skip to main content

Trusted <= trustworthy <= proof — position paper


Gernot Heiser

Open Kernel Labs




Virtualization, well established in enterprise, is finding its way into embedded systems. However, the use cases differ dramatically between the domains, and this results in significant differences in the requirements on the virtual-machine technology.

This paper examines a number of typical virtualization use cases from the CE domain, and the resulting requirements imposed on the hypervisor. We find that enterprise-style hypervisors are ill-matched to the requirements of the embedded domain, which are characterised by low-overhead communication, real-time capability, small memory footprint, small trusted computing base, and fine-grained control over security. We present the OKL4 hypervisor, a member of the L4 microkernel family, designed for embedded-systems use. We outline OKL4's relevant properties with an emphasis on its security mechanisms, and compare its performance to a version of Xen that has recently been promoted for CE use. We conclude that OKL4 is superior to enterprise-style hypervisors for use in CE devices.

BibTeX Entry

    author           = {Heiser, Gernot},
    month            = may,
    editor           = {{David Grawrock, Ahmad-Reza Sadeghi}},
    year             = {2009},
    keywords         = {operating systems, security, common criteria, implementation correctness, proof},
    title            = {Trusted <= Trustworthy <= Proof --- Position Paper},
    booktitle        = {Future of Trust in Computing},
    pages            = {55--59},
    address          = {Berlin}


Served by Apache on Linux on seL4.