Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

TL;DR

This paper explores using ESBMC, a formal verification tool, to verify the Realm Management Monitor in Arm's Confidential Computing Architecture, aiming to improve bug detection and verification efficiency in real-world scenarios.

Contribution

It demonstrates the application of ESBMC for verifying RMM, highlighting its effectiveness and proposing enhancements for industrial verification processes.

Findings

ESBMC can accurately parse source code and find specification failures.

The verification process is completed within a reasonable time frame.

Proposed improvements could make ESBMC more efficient for industry use.

Abstract

Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM. However, relying solely on a single verification tool may lead to the oversight of certain bugs or vulnerabilities. This paper discusses the application of ESBMC, a state-of-the-art Satisfiability Modulo Theories (SMT)-based software model checker, to further enhance RRM verification. We demonstrate ESBMC's ability to precisely parse the source code and identify specification failures within a reasonable time frame. Moreover, we propose potential improvements for ESBMC to enhance its efficiency for industry engineers. This work contributes to exploring the capabilities of formal verification techniques in real-world scenarios and suggests avenues for further improvements to better meet industrial verification needs.