典型文献
基于精化的可信执行环境内存隔离机制验证
文献摘要：
可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.
文献关键词：
TEE;内存隔离机制;形式化验证;精化关系;信息流安全性
中图分类号：
作者姓名：
靳翠珍;张倩颖;马雨薇;李希萌;王国辉;施智平;关永
作者机构：
首都师范大学 信息工程学院, 北京 100048;高可靠嵌入式系统北京市工程研究中心(首都师范大学), 北京 100048;计算机体系结构国家重点实验室(中国科学院 计算技术研究所), 北京 100190;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 100048;电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学), 北京 100048
文献出处：
引用格式：
[1]靳翠珍;张倩颖;马雨薇;李希萌;王国辉;施智平;关永-.基于精化的可信执行环境内存隔离机制验证)[J].软件学报,2022(06):2189-2207
A类：
内存隔离机制,精化关系,信息流安全,信息流安全性
B类：
可信执行环境,trusted,execution,environment,TEE,敏感数据,关键机制,访问控制,数据泄露,ARM,TrustZone,技术构建,制安,安全性验证,验证方法,抽象模型,明精,地址,MMU,monitor,定理证明,明器,Isabelle,HOL,无干扰,全属,形式化验证
AB值：
0.25963
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
