Change search
ReferencesLink to record
Permanent link

Direct link
A High Assurance Virtualization Platform for ARMv8
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
Ericsson Research.
SICS Swedish ICT.ORCID iD: 0000-0001-8003-200X
SICS Swedish ICT.ORCID iD: 0000-0003-3434-5640
Show others and affiliations
2016 (English)In: Networks and Communications (EuCNC), 2016 European Conference on, IEEE conference proceedings, 2016Conference 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
IEEE conference proceedings, 2016.
Keyword [en]
hypervisor, isolation, assurance, formal verification, Common Criteria, ARMv8
National Category
Computer Science
Research subject
Computer Science
URN: urn:nbn:se:kth:diva-192598DOI: 10.1109/EuCNC.2016.7561034ISBN: 978-1-5090-2893-1ISBN: 978-1-5090-2894-8OAI: diva2:971284
European Conference on Networks and Communications (EuCNC), 27-30 June 2016

QC 20160920

Available from: 2016-09-15 Created: 2016-09-15 Last updated: 2016-09-26Bibliographically approved

Open Access in DiVA

author version(313 kB)4 downloads
File information
File name FULLTEXT01.pdfFile size 313 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textEntry in publisher's database

Search in DiVA

By author/editor
Baumann, ChristophNäslund, MatsGehrmann, ChristianSchwarz, Oliver
By organisation
Theoretical Computer Science, TCS
Computer 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: 83 hits
ReferencesLink to record
Permanent link

Direct link