一句话：提出结合交互式定理证明、模型检测与并发测试的方法，验证 Arm CCA 中 RMM 的规约与原型实现。
本文介绍 Arm 在验证 Realm Management Monitor（RMM）规约与原型参考实现方面的工作。RMM 是 Arm 机密计算架构（Arm CCA）的关键固件组件，其威胁模型严苛、安全攸关。作者组合交互式定理证明、模型检测和并发感知测试，对 RMM 的规约与原型实现的安全（security）与安全性质（safety）进行验证。这些验证工作与规约和实现的开发同步进行并持续迭代，且已被 Arm 产品团队采用。论文报告了形式化技术带来的主要成果，以及未来工作仍面临的挑战，并认为这是当前商用机密计算实现中最彻底的形式化技术应用之一。
We present Arm's efforts in verifying the specification and prototype reference implementation of the Realm Management Monitor (RMM), an essential firmware component of Arm Confidential Computing Architecture (Arm CCA), the recently-announced Confidential Computing technologies incorporated in the Armv9-A architecture. Arm CCA introduced the Realm Management Extension (RME), an architectural extension for Armv9-A, and a technology that will eventually be deployed in hundreds of millions of devices. Given the security-critical nature of the RMM, and its taxing threat model, we use a combination of interactive theorem proving, model checking, and concurrency-aware testing to validate and verify security and safety properties of both the specification and a prototype implementation of the RMM. Crucially, our verification efforts were, and are still being, developed and refined contemporaneously with active development of both specification and implementation, and have been adopted by Arm's product teams. We describe our major achievements, realized through the application of formal techniques, as well as challenges that remain for future work. We believe that the work reported in this paper is the most thorough application of formal techniques to the design and implementation of any current commercially-viable Confidential Computing implementation, setting a new high-water mark for work in this area.
@article{paperbot2034,
title = {A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations},
author = {Anthony C. J. Fox and Gareth Stockwell and Shale Xiong and Hanno Becker and Dominic P. Mulligan and Gustavo Petri and Nathan Chong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586040}
}