A high assurance virtualization platform for ARMv8

Christoph Baumann; Mats Naslund; Christian Gehrmann; Oliver Schwarz; Hans Thorsen

doi:10.1109/EuCNC.2016.7561034

A high assurance virtualization platform for ARMv8

Christoph Baumann, Mats Naslund, Christian Gehrmann, Oliver Schwarz, Hans Thorsen

Research output: Chapter in Book/Report/Conference proceeding › Paper in conference proceeding › peer-review

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

Original language	English
Title of host publication	2016 European Conference on Networks and Communications (EuCNC)
Publisher	IEEE - Institute of Electrical and Electronics Engineers Inc.
Pages	210-214
Number of pages	5
ISBN (Electronic)	9781509028931
ISBN (Print)	9781509028948
DOIs	https://doi.org/10.1109/EuCNC.2016.7561034
Publication status	Published - 2016 Sept 6
Externally published	Yes
Event	2016 European Conference on Networks and Communications, EUCNC 2016 - Athens, Greece Duration: 2016 Jun 27 → 2016 Jun 30

Conference

Conference	2016 European Conference on Networks and Communications, EUCNC 2016
Country/Territory	Greece
City	Athens
Period	2016/06/27 → 2016/06/30

Free keywords

ARMv8
assurance
Common Criteria
formal verification
hypervisor
isolation

Access to Document

10.1109/EuCNC.2016.7561034

Cite this

@inproceedings{5f0a8e3e53c84776a367d630876211af,

title = "A high assurance virtualization platform for ARMv8",

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) 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.",

keywords = "ARMv8, assurance, Common Criteria, formal verification, hypervisor, isolation",

author = "Christoph Baumann and Mats Naslund and Christian Gehrmann and Oliver Schwarz and Hans Thorsen",

year = "2016",

month = sep,

day = "6",

doi = "10.1109/EuCNC.2016.7561034",

language = "English",

isbn = "9781509028948",

pages = "210--214",

booktitle = "2016 European Conference on Networks and Communications (EuCNC)",

publisher = "IEEE - Institute of Electrical and Electronics Engineers Inc.",

address = "United States",

note = "2016 European Conference on Networks and Communications, EUCNC 2016 ; Conference date: 27-06-2016 Through 30-06-2016",

}

Baumann, C, Naslund, M, Gehrmann, C, Schwarz, O & Thorsen, H 2016, A high assurance virtualization platform for ARMv8. in 2016 European Conference on Networks and Communications (EuCNC)., 7561034, IEEE - Institute of Electrical and Electronics Engineers Inc., pp. 210-214, 2016 European Conference on Networks and Communications, EUCNC 2016, Athens, Greece, 2016/06/27. https://doi.org/10.1109/EuCNC.2016.7561034

A high assurance virtualization platform for ARMv8. / Baumann, Christoph; Naslund, Mats; Gehrmann, Christian et al.
2016 European Conference on Networks and Communications (EuCNC). IEEE - Institute of Electrical and Electronics Engineers Inc., 2016. p. 210-214 7561034.

Research output: Chapter in Book/Report/Conference proceeding › Paper in conference proceeding › peer-review

TY - GEN

T1 - A high assurance virtualization platform for ARMv8

AU - Baumann, Christoph

AU - Naslund, Mats

AU - Gehrmann, Christian

AU - Schwarz, Oliver

AU - Thorsen, Hans

PY - 2016/9/6

Y1 - 2016/9/6

N2 - 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.

AB - 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.

KW - ARMv8

KW - assurance

KW - Common Criteria

KW - formal verification

KW - hypervisor

KW - isolation

U2 - 10.1109/EuCNC.2016.7561034

DO - 10.1109/EuCNC.2016.7561034

M3 - Paper in conference proceeding

AN - SCOPUS:84988950416

SN - 9781509028948

SP - 210

EP - 214

BT - 2016 European Conference on Networks and Communications (EuCNC)

PB - IEEE - Institute of Electrical and Electronics Engineers Inc.

T2 - 2016 European Conference on Networks and Communications, EUCNC 2016

Y2 - 27 June 2016 through 30 June 2016

ER -

A high assurance virtualization platform for ARMv8

Abstract

Conference

Free keywords

Access to Document

Fingerprint

Cite this