The first formal review of a prototype Arm CCA firmware

As our personal data is increasingly used in many applications from advertising to finance to healthcare, the protection of sensitive information has become an essential feature of computer architectures.

Arm CCA

Applications that process such data must trust the system software they rely on, such as operating systems and hypervisors, but such system software is complex and often has vulnerabilities that can compromise data confidentiality and integrity.

For the past two years, Columbia Engineering researchers have been working with Arm, a semiconductor IP and software design company, to address these vulnerabilities. The team has now unveiled key verification technologies for the Arm Confidential Compute Architecture (Arm CCA), a new feature of the Armv9-A architecture. The paper, presented at the 16th USENIX Symposium on Operating Systems Design and Implementation, demonstrates the first formal verification of a prototype Arm CCA firmware.

Arm CCA relies on firmware to manage hardware and enforce its security guarantees, so it is important that firmware is accurate and secure. While many previous systems depended on firmware, none of them can guarantee that the firmware is bug-free.

Formal verification is a relatively new method now used to guarantee software/hardware correctness. Instead of testing, formal verification uses mathematical models to prove that the software and hardware are absolutely correct, offering the highest guarantee of correctness.

“We proved for the first time that the firmware is correct and secure, leading to the first demonstration of confidential computer architecture backed by formally verified firmware,” said the study’s lead author Xupeng Li, a graduate student of Ronghui Gu. Tang family assistant professor of computer science, and Jason Nieh, professor of computer science and co-director of the Software Systems Laboratory.

While there are many approaches to verifying the correctness of simple programs, they are not amenable to something as complex as CCA firmware, so researchers had to develop new verification techniques to enable verification of Arm CCA firmware. For example, the CCA firmware is designed for scalability and performance, enabling highly concurrent operation and mixing C and assembly code. Concurrent operation is made possible through the use of fine-grain synchronization methods and code with data races.

It is an Arm CCA design principle that untrusted software must remain in control of the management of hardware resources. Therefore, a key challenge is to prove that the system is still secure even though untrusted software can take away hardware resources at will. Previous approaches could not verify programs with such properties. This new verification technique is powerful enough to verify concurrent firmware with both C and assembly code.

“Bugs are really hard to find using classic software testing techniques,” said Xuheng Li, the co-author of the paper. “In this way, we demonstrated the importance and value of our formal verification techniques, with the end result being the first demonstration of a confidential computer architecture supported by verified firmware.”

The team is very excited about the new verification technologies that can be used to prove the correctness of implementations of the firmware underlying Arm CCA. ARM CPUs are already used in billions of devices around the world. As Arm CCA is increasingly used to protect users’ private data – particularly in cloud services and beyond – the verification techniques presented in this white paper will provide a significant improvement in privacy and security.

One of the challenges with formal methods applied to software is the need to adjust proofs when software is updated. Researchers are working on new technologies that will help them verify Arm CCA firmware updates incrementally and quickly, ensuring they are always verifying the latest available firmware.

Gu and Nieh added, “We recognize the power and potential of formal verification through our work and believe that formal verification is an essential technique that will replace the currently used software testing in the near future.”

Leave a Comment

%d bloggers like this: