使用ESBMC验证Arm(R)机密计算架构组件
Verifying components of Arm(R) Confidential Computing Architecture with ESBMC
AI总结：
本文应用基于SMT的软件模型检查器ESBMC对Arm机密计算架构中的RMM固件进行验证，展示其在合理时间内发现规范失败的能力，并提出改进建议以更好满足工业验证需求。
摘要：
Realm Management Monitor（RMM）是近期Arm机密计算架构（Arm CCA）中至关重要的固件组件。先前的工作应用形式化技术来验证RMM的规范及原型参考实现。然而，仅依赖单一验证工具可能导致某些缺陷或漏洞被忽视。本文讨论了ESBMC——一种基于可满足性模理论（SMT）的最先进软件模型检查器——的应用，以进一步增强RMM验证。我们展示了ESBMC在合理时间范围内精确解析源代码并识别规范失败的能力。此外，我们提出了对ESBMC的潜在改进，以提升其对工业工程师的效率。这项工作有助于探索形式化验证技术在真实场景中的能力，并为进一步改进以更好地满足工业验证需求提出了途径。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
