A High Assurance Virtualization Platform for ARMv8

Baumann, Christoph and Näslund, Mats and Gehrmann, Christian and Schwarz, Oliver and Thorsen, Hans (2016) A High Assurance Virtualization Platform for ARMv8. In: European Conference on Networks and Communications (EuCNC) 2016.

PDF (author version) - Accepted Version

Official URL:


This paper presents the first results from the ongoing research project HASPOC, developing a high assurance virtualization platform for the ARMv8 CPU architecture. Formal verification at machine code level guarantees information isolation between different guest systems (e.g.~OSs) running on the platform. To use the platform in networking scenarios, we allow guest systems to securely communicate with each other via platform-provided communication channels and to take exclusive control of peripherals for communication with the outside world. The isolation is shown to be formally equivalent to that of guests executing on physically separate platforms with dedicated communication channels crossing the air-gap. Common Criteria (CC) assurance methodology is applied by preparing the CC documentation required for an EAL6 evaluation of products using the platform. Besides the hypervisor, a secure boot component is included and verified to ensure system integrity.

Item Type:Conference or Workshop Item (Paper)
Additional Information:This is the author version of the corresponding paper published in the 2016 European Conference on Networks and Communications (EuCNC). The publisher is IEEE. The final publication (DOI: 10.1109/EuCNC.2016.7561034) is available at IEEE Xplore via © © 2016 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Uncontrolled Keywords:hypervisor, isolation, assurance, formal verification, Common Criteria, ARMv8
ID Code:6062
Deposited By:Oliver Schwarz
Deposited On:16 Sep 2016 11:02
Last Modified:16 Sep 2016 11:02

Repository Staff Only: item control page