Change search
ReferencesLink to record
Permanent link

Direct link
A High Assurance Virtualization Platform for ARMv8
HASPOC.
HASPOC.
RISE, Swedish ICT, SICS. SEC.
RISE, Swedish ICT, SICS. SEC.
Show others and affiliations
Number of Authors: 5
2016 (English)Conference paper (Refereed)
Abstract [en]

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
2016, 9.
Keyword [en]
hypervisor, isolation, assurance, formal verification, Common Criteria, ARMv8
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-24570DOI: 10.1109/EuCNC.2016.7561034OAI: oai:DiVA.org:ri-24570DiVA: diva2:1043655
Conference
European Conference on Networks and Communications (EuCNC) 2016
Projects
HASPOC
Note
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 http://ieeexplore.ieee.org/document/7561034 © © 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.Available from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(238 kB)4 downloads
File information
File name FULLTEXT01.pdfFile size 238 kBChecksum SHA-512
9dfd0750e014b69f31131452c546466b03edbc7345375dcf4234667ada26807f56503da611371571ae724fc4ed0b087d8e5e2c12fbc758bea04f13c0211d6d06
Type fulltextMimetype application/pdf

Other links

Publisher's full texthttp
By organisation
SICS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 4 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 23 hits
ReferencesLink to record
Permanent link

Direct link