Arm's Confidential Computing Architecture, Built for Privacy and Security, Gains Formal Verification

Computer scientists from Columbia University and Arm have announced successful verification of the company's Confidential Compute Architecture, a new feature of the Armv9-A chip architecture that aims to protect users' data even as it's processed, proving that the firmware on which it relies can be trusted.

"We've proved, for the first time, that the firmware is correct and secure," explains lead author Xupeng Li of the team's work, "resulting in the first demonstration of a confidential computing architecture backed by formally verified firmware."

Introduced with the Armv9-A architecture, the high-performance application-processor profile of the Armv9 architecture the company launched last year, Arm's Confidential Compute Architecture (CCA) aims to remove the risk of trusting kernels and hypervisors to keep data confidential — protecting both data and code from even the highest levels of the underlying operating system.

"Arm CCA extends workload isolation to enable a provider to shift from a position where service providers will not access customer data, to one where they cannot access customer data," claimed Arm's Richard Grisenthwaite at the launch, "thereby reducing the volume of software that must be trusted, the attack surface for hackers, and the potential for customer data or algorithm breaches."

History is littered with claims of "unhackable" protection systems, however, and few have stood the test of time — which is why the formal verification of the firmware underpinning CCA is being positioned by Arm as a major milestone even as the team behind said verification seems rather more excited about the novel approach to verification it developed for the project, which it says can be applied to all implementations of Arm's CCA.

"Bugs are really hard to find via classic software testing techniques," explains co-author Xuheng Li. "So we showed the importance and value of our formal verification techniques with the end result being the first demonstration of a confidential computing architecture backed by verified firmware."

The team presented its work at the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI '22) earlier this week, with an open-access copy of the paper available on the USENIX website.