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.

翻译：领域管理监视器（RMM）是近期Arm机密计算架构（Arm CCA）中的一个关键固件组件。先前的研究已应用形式化技术来验证RMM的规范及原型参考实现。然而，仅依赖单一验证工具可能导致某些缺陷或漏洞被忽视。本文讨论了应用ESBMC（一种先进的基于可满足性模理论（SMT）的软件模型检查器）来进一步增强RMM验证。我们展示了ESBMC在合理时间内精确解析源代码并识别规范违规的能力。此外，我们提出了ESBMC的潜在改进方向，以提升其在工业工程师使用中的效率。本工作有助于探索形式化验证技术在实际场景中的应用能力，并为更好地满足工业验证需求提出了进一步的改进途径。