A high assurance virtualization platform for ARMv8
(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)
- author
- Baumann, Christoph ; Naslund, Mats ; Gehrmann, Christian LU ; Schwarz, Oliver and Thorsen, Hans
- publishing date
- 2016-09-06
- 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-07-09 00:24:32
@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}}, }