Design and Verification of the Arm Confidential Compute Architecture

Explore the design and verification of the Arm Confidential Compute Architecture in this 19-minute conference talk from OSDI '22. Delve into the innovative Realms abstraction, a new approach to confidential computing that protects data confidentiality and integrity of virtual machines. Learn how hardware creates and enforces the Realm world, a separate physical address space for Realms, while firmware secures them and manages requests from untrusted system software. Discover novel verification techniques used to prove the security and correctness of concurrent software with complex features such as hand-over-hand locking, dynamically allocated shared page tables, and data races in kernel code running on relaxed memory hardware. Gain insights into the integration of C and Arm assembly code, and how untrusted software maintains control of system resource allocation while being prevented from accessing Realm memory contents. Understand the significance of this technology as part of the Arm Confidential Compute Architecture and its potential impact on data privacy in computing.