软件学报

作者：靳翠珍，张倩颖，马雨薇，李希萌，王国辉，施智平，关永

单位：靳翠珍，首都师范大学 信息工程学院, 北京 10004811,张倩颖，首都师范大学 信息工程学院, 北京 100048;高可靠嵌入式系统北京市工程研究中心(首都师范大学), 北京 100048;计算机体系结构国家重点实验室(中国科学院 计算技术研究所), 北京 10019002,马雨薇，首都师范大学 信息工程学院, 北京 10004803,李希萌，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004804,王国辉，首都师范大学 信息工程学院, 北京 100048;高可靠嵌入式系统北京市工程研究中心(首都师范大学), 北京 10004805,施智平，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004806,关永，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学), 北京 10004807

关键词：TEE;内存隔离机制;形式化验证;精化关系;信息流安全性

基金：国家自然科学基金(61802375,61602325,61876111,61877040,62002246);北京市教委科技计划(KM201910028005,KM202010028010);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920);中央支持地方建设-“双一流”建设项目(20531120005)

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

来源：2022年第6期

《软件学报》期刊编辑部

查看软件学报杂志2022年第6期