今天为大家推荐的论文来自浙江大学网络空间安全学院赵永望研究组投稿并发表在IEEE TDSC期刊上的最新工作 ProveriT: A Parameterized, Composable, and Verified Model of TEE Protection Profile 。该工作提出了组合验证框架并对可信执行环境的安全规范文档进行了形式化建模。通过形式化验证确保其正确性并且发现了漏洞。 在现代计算机系统中,可信执行环境(TEE)扮演着至关重要的角色。TEE通过提供隔离执行环境,确保电子设备中敏感数据的安全。然而,一旦TEE被攻破,可能会导致巨大的损失。尽管已经有许多TEE产品,但大多数缺乏强有力的安全保障。为了解决这一问题,GlobalPlatform(GP)定义了TEE的保护轮廓标准GPTEE PP: GlobalPlatform Technology TEE Protection Profile。 其中,GlobalPlatform(GP)是一个致力于确保数字设备安全的国际性组织。该组织制定了许多安全标准和规范,以
………………………………