Securing the Arm
Confidential Computing Architecture
23 additional property violations identified in the Realm Management Monitor — the privileged firmware at the root of trust of the Armv9 Confidential Computing Architecture — on top of those already detected by CBMC.
23
Additional property violations only ESBMC detected on Arm's RMM firmware
Armv9
CCA is rolling out across the Armv9 ecosystem
SAS 2024
Published at the Static Analysis Symposium (Wu et al., 451–462)
Arm CoE
Co-funded via the Arm Centre of Excellence at the University of Manchester
Challenge
Arm's Confidential Computing Architecture (CCA) provides hardware-enforced memory isolation, and is rolling out across the Armv9 ecosystem. The Realm Management Monitor (RMM) is the privileged firmware component at its core — it enforces isolation between the Realm, Secure, Root, and Non-secure memory worlds, and is the root of trust for the entire CCA.
Any property violation in the RMM could undermine the confidentiality guarantees of cloud workloads running on CCA-enabled hardware. Arm engineers had auto-generated verification harnesses from the RMM's machine-readable specification and were already deploying CBMC (the C Bounded Model Checker by Daniel Kroening and Michael Tautschnig) against those harnesses in their CI/CD — confirming and fixing several violations along the way. The open question Arm collaborators wanted to answer was whether a different state-of-the-art model checker could uncover further violations on the same code.
Approach
Working with Arm engineers — including co-authors Shale Xiong and Gareth Stockwell — we applied ESBMC to the RMM verification harnesses against the safety and security properties defined in the RMM specification. We first reproduced the violations CBMC had previously reported (and that Arm engineers had already confirmed), then ran ESBMC against the same codebase to look for additional findings.
During the comparison, we also identified a small number of cases where CBMC and ESBMC produced inconsistent verdicts. We reported these to the CBMC team, who confirmed an underlying memory-model bug (diffblue/cbmc#8161). The work was published at SAS 2024 and the verification artefacts deposited on Zenodo for reproducibility.
Results
23 additional property violations identified in the RMM implementation that ESBMC was able to detect on top of those already reported by CBMC on the same codebase.
Inconsistent verdicts between CBMC and ESBMC were documented and reported upstream, leading to a confirmed memory-model fix in CBMC.
Arm's co-authorship of the published work, together with co-funding via the Arm Centre of Excellence at the University of Manchester, confirms this was a real-world collaboration on production-track firmware rather than a synthetic benchmark study.
The findings strengthened the assurance baseline of the RMM implementation as published.
References
- Tong Wu, Shale Xiong, Edoardo Manino, Gareth Stockwell, Lucas C. Cordeiro. Verifying Components of Arm® Confidential Computing Architecture with ESBMC. SAS 2024: 451–462. ssvlab.github.io/lucasccordeiro/papers/sas2024.pdf
Note. The collaboration described on this page is a published academic research engagement (SAS 2024) co-authored with engineers from Arm and partially funded via the Arm Centre of Excellence at the University of Manchester. CBMC is an independent third-party tool authored by Daniel Kroening and Michael Tautschnig; the inconsistency described above was reported upstream and confirmed by the CBMC maintainers. Findings reported as "property violations" are assertion or specification violations identified by the model checker on the published RMM code; the paper does not characterise them as exploitable security vulnerabilities.