Design and Verification of the Arm Confidential Compute Architecture

Authors: 

Xupeng Li and Xuheng Li, Columbia University; Christoffer Dall, Arm Ltd; Ronghui Gu and Jason Nieh, Columbia University; Yousuf Sait and Gareth Stockwell, Arm Ltd

Abstract: 

The increasing use of sensitive private data in computing is matched by a growing concern regarding data privacy. System software such as hypervisors and operating systems are supposed to protect and isolate applications and their private data, but their large codebases contain many vulnerabilities that can risk data confidentiality and integrity. We introduce Realms, a new abstraction for confidential computing to protect the data confidentiality and integrity of virtual machines. Hardware creates and enforces Realm world, a new physical address space for Realms. Firmware controls the hardware to secure Realms and handles requests from untrusted system software to manage Realms, including creating and running them. Untrusted system software retains control of the dynamic allocation of memory to Realms, but cannot access Realm memory contents, even if run at a higher privileged level. To guarantee the security of Realms, we verified the firmware, introducing novel verification techniques that enable us to prove, for the first time, the security and correctness of concurrent software with hand-over-hand locking and dynamically allocated shared page tables, data races in kernel code running on relaxed memory hardware, integrated C and Arm assembly code calling one another, and untrusted software being in full control of allocating system resources. Realms are included in the Arm Confidential Compute Architecture.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {280904,
author = {Xupeng Li and Xuheng Li and Christoffer Dall and Ronghui Gu and Jason Nieh and Yousuf Sait and Gareth Stockwell},
title = {Design and Verification of the Arm Confidential Compute Architecture},
booktitle = {16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)},
year = {2022},
isbn = {978-1-939133-28-1},
address = {Carlsbad, CA},
pages = {465--484},
url = {https://www.usenix.org/conference/osdi22/presentation/li},
publisher = {USENIX Association},
month = jul,
}