可信执行环境（Trusted Execution Environment, TE）应用程序接口的正式规范制定以及可信应用程序的模型检测

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

　　

摘要AI摘要

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

了解更多登录

摘要

摘要

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

AI摘要

AI生成摘要（实验性）

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

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

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