A Verification Methodology for the Arm® Confidential Computing Architecture: Fr...
summary
The project verifies Arm CCA’s Realm Management Monitor by combining CBMC model checking, interactive theorem proving, and concurrency-aware testing against a ~100-page machine-readable specification and ~10K lines of C, replacing small assembly fragments. Automation generates CBMC harnesses from pre/post conditions; manual stubs implement informal predicates. Results include 25% of tracked specification issues found early, memory-safety checks passing, and tooling to explore non‑atomic concurrency and lock-ordering.
AI-written summary · about
chapters (9)
- 0:00Introduction to Arm Confidential Computing
- 1:03Arm CCA and RME
- 2:30Verification goals and challenges
- 3:54Spec verification with ImProver
- 7:29Isolation and security proofs
- 9:38C verification with CBMC
- 12:51Concurrency in verification
- 15:17Industry verification approach
- 16:19Conclusion and Q&A
related talks
39mFormal specification of attestation mechanisms in Confidential Computing
19mIntroduction of CCA on Arm
32mWhen Confidential Containers Meet Arm CCA
46mAdding Arm RME/CCA Support in Confidential Containers
38mUnveiling Arm Confidential Computing Architecture Software Stack
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
23mMorello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…)
01h 05mKeynote: Can we reason about the security of concurrent systems code?