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

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

　　

摘要AI摘要

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

了解更多信息登录

摘要

摘要

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

AI摘要

AI生成摘要（实验性）

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

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

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