Security News > 2022 > July > The first formal verification of a prototype of Arm CCA firmware

The 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 to enforce its security guarantees, so it is essential that the firmware is correct and secure.

"We've proved, for the first time, that the firmware is correct and secure, resulting in the first demonstration of a confidential computing architecture backed by formally verified firmware," said the study's lead author Xupeng Li, a PhD 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 suitable for something as complex as CCA firmware, so the researchers had to develop new verification techniques to make verifying Arm CCA firmware possible.

The team is very excited about the new verification technologies that can be used to prove the correctness of implementations of firmware underlying Arm CCA. Arm CPUs are already deployed across billions of devices around the world.

The researchers are working on new technologies to help them incrementally and quickly verify updates to Arm CCA firmware and ensure that the latest firmware available is always verified.

News URL

https://www.helpnetsecurity.com/2022/07/18/arm-cca-firmware/