Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

A high assurance virtualization platform for ARMv8

Baumann, Christoph ; Naslund, Mats ; Gehrmann, Christian LU ; Schwarz, Oliver and Thorsen, Hans (2016) 2016 European Conference on Networks and Communications, EUCNC 2016 p.210-214
Abstract

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)... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; ; ; and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
keywords
ARMv8, assurance, Common Criteria, formal verification, hypervisor, isolation
host publication
2016 European Conference on Networks and Communications (EuCNC)
article number
7561034
pages
5 pages
publisher
IEEE - Institute of Electrical and Electronics Engineers Inc.
conference name
2016 European Conference on Networks and Communications, EUCNC 2016
conference location
Athens, Greece
conference dates
2016-06-27 - 2016-06-30
external identifiers
  • scopus:84988950416
ISBN
9781509028931
9781509028948
DOI
10.1109/EuCNC.2016.7561034
language
English
LU publication?
no
id
5f0a8e3e-53c8-4776-a367-d630876211af
date added to LUP
2018-11-21 16:42:14
date last changed
2024-02-14 11:17:14
@inproceedings{5f0a8e3e-53c8-4776-a367-d630876211af,
  abstract     = {{<p>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.</p>}},
  author       = {{Baumann, Christoph and Naslund, Mats and Gehrmann, Christian and Schwarz, Oliver and Thorsen, Hans}},
  booktitle    = {{2016 European Conference on Networks and Communications (EuCNC)}},
  isbn         = {{9781509028931}},
  keywords     = {{ARMv8; assurance; Common Criteria; formal verification; hypervisor; isolation}},
  language     = {{eng}},
  month        = {{09}},
  pages        = {{210--214}},
  publisher    = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
  title        = {{A high assurance virtualization platform for ARMv8}},
  url          = {{http://dx.doi.org/10.1109/EuCNC.2016.7561034}},
  doi          = {{10.1109/EuCNC.2016.7561034}},
  year         = {{2016}},
}