可信执行环境访问控制建模与安全性分析
作者:
作者单位:

作者简介:

通讯作者:

常瑞,E-mail:crix1021@zju.edu.cn

中图分类号:

TP301

基金项目:

国家自然科学基金(61872016, 62132014)


Modeling and Security Analysis of Access Control in Trusted Execution Environment
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    可信执行环境的安全问题一直受到国内外学者的关注.利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制, 但已有方案往往依赖于测试或者经验分析表明其有效性, 缺乏严格的正确性和安全性保证.本文针对内存标签实现的访问控制提出了通用的形式化模型框架, 并提出了一种基于模型检测的访问控制安全性分析方法.首先, 利用形式化方法构建了基于内存标签的可信执行环境访问控制通用模型框架, 给出访问控制实体的形式化定义, 定义的规则包括访问控制规则和标签更新规则; 然后利用形式化语言B以递增的方式设计并实现了该框架的抽象机模型, 通过不变式约束形式化描述了模型的基本性质; 再次以可信执行环境的一个具体实现TIMBER-V为应用实例, 通过实例化抽象机模型构建TIMBER-V访问控制模型, 添加安全性质规约并运用模型检测验证了模型的功能正确性和安全性; 最后模拟了具体攻击场景并实现攻击检测, 评估结果表明了本文提出的安全性分析方法的有效性.

    Abstract:

    The security issues of Trusted Execution Environment (TEE) have always been concerned by the domestic and foreign researchers. Memory tag technology utilized in TEE helps to achieve finer-grained memory isolation and access control mechanisms. Neverthless, prior works often rely on testing or empirical analysis to show their effectiveness, which lacks strong assurance of functional correctness and security properties. This paper proposes a general formal model framework for memory tag based access control, and presents a security analysis method in access control based on model checking. First, a general framework for access control model of TEE based on memory tag are constructed utilizing formal method, and those access control entities are formally defined. The defined rules include access control rules and tag update rules. Then the abstract machines of the framework is incrementally designed and implemented with formal language B. These abstract machines formalize the basic properties through invariant constraints. Next, a TEE implementation called TIMBER-V is used as an application case. The TIMBER-V access control model is constructed by instantiating these abstract machines, and the security properties are formally specified. The functional correctness and security of the instantiated model is verified based on model checking. Finally, this paper simulates the specific attack scenarios and these attacks are successfully detected. The evaluation results show the effectiveness of the security analysis method.

    参考文献
    相似文献
    引证文献
引用本文

苗新亮,常瑞,潘少平,赵永望,蒋烈辉.可信执行环境访问控制建模与安全性分析.软件学报,,():0

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-08-30
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号