A High Assurance Virtualization Platform for ARMv8
2016 (English)In: Networks and Communications (EuCNC), 2016 European Conference on, IEEE conference proceedings, 2016Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
IEEE conference proceedings, 2016.
hypervisor, isolation, assurance, formal verification, Common Criteria, ARMv8
Research subject Computer Science
IdentifiersURN: urn:nbn:se:kth:diva-192598DOI: 10.1109/EuCNC.2016.7561034ISBN: 978-1-5090-2893-1ISBN: 978-1-5090-2894-8OAI: oai:DiVA.org:kth-192598DiVA: diva2:971284
European Conference on Networks and Communications (EuCNC), 27-30 June 2016
QC 201609202016-09-152016-09-152016-09-26Bibliographically approved