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

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

　　

摘要AI 摘要

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

了解更多登录

摘要

摘要

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

AI 摘要

AI 生成摘要（实验性）

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

点击 此处 对本文摘要的准确性、清晰度和有用性进行评论。这样做将有助于信息的完善和未来再生成版本。

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