"The First Formal Verification of a Prototype of Arm CCA Firmware"

Researchers at Columbia Engineering, working with Arm, a semiconductor IP and software design company, has revealed key verification technologies for the Arm Confidential Compute Architecture (Arm CCA), a new feature of the Armv9-A architecture. Their paper, presented at the 16th USENIX Symposium on Operating Systems Design and Implementation, demonstrates the first formal verification of a prototype of Arm CCA firmware. Arm CCA relies on firmware to manage the hardware and enforce its security guarantees, so the firmware must be correct and secure. While many previous systems relied on firmware, none could guarantee that the firmware was bug-free. Formal verification is a relatively new methodology for ensuring the correctness of software and hardware. Formal verification uses mathematical models to prove that the software and hardware are absolutely correct, providing the highest level of assurance of correctness. The team says they have proved, for the first time, that the firmware is correct and secure, thus resulting in the first demonstration of a confidential computing architecture backed by formally verified firmware. Although there are many approaches to verifying the correctness of simple programs, they are insufficient for something as complex as CCA firmware. Therefore, the researchers had to develop new verification techniques to make Arm CCA firmware verification possible. CCA firmware, for example, is designed for scalability and performance, so it supports highly concurrent operation and combines C and assembly code. Fine-grain synchronization methods and code with data races enable concurrent operation. It is an Arm CCA design principle that untrusted software must retain control of managing hardware resources. Proving that the system is still secure even though untrusted software can take away hardware resources as it pleases is a key challenge. Previous approaches were unable to validate programs with such properties. This new verification technique is capable of validating concurrent firmware written in both C and assembly code. This article continues to discuss the team's first formal verification of a prototype of Arm CCA firmware. 

Help Net Security reports "The First Formal Verification of a Prototype of Arm CCA Firmware"