可信执行环境API的形式化规范与可信应用程序的模型检测

《Formal Aspects of Computing》：Formal Specification of Trusted Execution Environment APIs and Model Checking of Trusted Applications

　　

摘要AI 摘要

要查看此 AI 生成的摘要，您必须拥有高级访问权限。

了解更多登录

摘要

摘要

可信执行环境（TEEs）已成为网络安全中的关键技术，提供隔离环境，可在其中安全地执行敏感计算。在 TEE 中运行的可信应用程序是使用许多 TEE 硬件平台所遵循的标准化 API 开发的。然而，针对这些标准 TEE API 的正式可执行模型尚未得到充分发展。在本文中，我们使用 Maude 提出了 TEE API 的正式规范。我们重点关注可信存储 API 和密码操作 API，两者都是移动和物联网应用的基础。为了支持可信应用程序的正式分析，我们还对更广泛的 TEE 基础设施进行了建模。此外，我们应用了一种基于不可见转换的状态空间缩减技术，以缓解状态爆炸问题。我们通过开源物联网 TEE 应用程序 MQT-TZ 的正式分析展示了我们方法的有效性。我们的正式分析揭示了 MQT-TZ 实现中存在的安全漏洞。我们修补了该实现，并使用模型检查验证了其正确性。

AI 摘要

AI 生成摘要（实验性）

本摘要使用自动化工具生成，并非由文章作者撰写或审核。它旨在支持发现，帮助读者评估相关性，并协助相邻研究领域的读者理解该工作。它旨在补充作者提供的摘要，后者仍是论文的主要摘要。全文仍为权威记录版本。点击此处了解更多。

点击此处评论此摘要的准确性、清晰度和有用性。这样做将有助于改进和未来的重新生成版本。

要查看此 AI 生成的通俗语言摘要，您必须拥有高级访问权限。