Keynote Talk: Hardware-based Confidential Computing: verifying Arm-V9 CCA

Abstract:

Gustavo will present emergent technologies for hardware-assisted confidential computing in the Cloud. he will then focus on the case of the Arm Confidential Computing Architecture (CCA), an architectural extension of Arm-V9. Gustavo will show also how Arm applies a number of formal methods to guarantee security properties of Arm CCA.
This tutorial is aimed at presenting confidential computing at a high-level, and demonstrating how we apply formal methods in industry to validate security critical components.