ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2018, Vol. 55 ›› Issue (8): 1809-1825.doi: 10.7544/issn1000-1239.2018.20170250

• 信息安全 • 上一篇    

位置约束的访问控制模型及验证方法

曹彦1,黄志球1,2,3,阚双龙1,彭焕峰1,柯昌博1,4   

  1. 1(南京航空航天大学计算机科学与技术学院 南京 211106);2(高安全系统的软件开发与验证技术工业和信息化部重点实验室(南京航空航天大学) 南京 211106);3(软件新技术与产业化协同创新中心 南京 210093);4(南京邮电大学计算机学院 南京 210023) (caoyan926@nuaa.edu.cn)
  • 出版日期: 2018-08-01
  • 基金资助: 
    国家“八六三”高技术研究发展计划基金项目(2015AA015303);国家自然科学基金项目(61772270,61602262,61602237);江苏省自然科学基金青年项目(BK20150865,BK20170809) This work was supported by the National High Technology Research and Development Program of China (863 Program) (2015AA015303), the National Natural Science Foundation of China (61772270, 61602262, 61602237), and Jiangsu Natural Science Foundation of China (BK20150865, BK20170809).

Location-Constrained Access Control Model and Verification Methods

Cao Yan1, Huang Zhiqiu1,2,3, Kan Shuanglong1, Peng Huanfeng1,Ke Changbo1,4   

  1. 1(School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106);2(Key Laboratory of Safety-Critical Software(Nanjing University of Aeronautics and Astronautics), Ministry of Industry and Information Technology, Nanjing 211106);3(Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 210093);4(School of Computer Science, Nanjing University of Posts and Telecommunications, Nanjing 210023)
  • Online: 2018-08-01

摘要: 随着物联网和信息物理融合系统等新一代信息技术的发展,位置约束的访问控制系统的安全性需求不仅体现在虚拟的信息空间,还体现在现实的物理空间.如何在这种新需求下制定位置约束的访问控制模型与验证方法成为保证访问控制系统安全的关键所在.首先提出位置约束访问控制模型,包括LCRBAC模型和EM模型,实现对信息空间和物理空间的静态结构以及两空间中实体动态行为的刻画;其次利用偶图和偶图反应系统建模位置约束访问控制模型,生成访问控制策略标注转移边的标号变迁系统;然后根据标号变迁系统验证结果,提出针对死锁状态、违反状态和不可达状态的策略修改方案;最后通过银行访问控制系统实例分析说明所提方法能够对信息空间和物理空间以及两空间交互行为的访问控制策略进行建模和验证.

关键词: 位置约束访问控制系统, 模型检测, 偶图, 反应规则, 验证

Abstract: With the advent of Internet of things and cyber-physical systems, location-constrained access control systems need to consider security requirements of cyber spaces and physical spaces simultaneously, because the boundary between the physical and the cyber world becomes unclear in these new paradigms. However, the most existing access control models consider physical and cyber security separately, and they are oblivious to cyber-physical interactions. Authorization models are needed to help the security policy design and express higher-level organizational security rules. Firstly, the environment model (EM) and location-constrained role-based access control (LCRBAC) model are proposed. The environment model is presented for describing the static topology configuration of cyber space and physical space. The LCRBAC model is used to describe dynamic behaviors of cyber entities and physical entities. Secondly, given the bigraphs and bigraphs reactive systems that describe the environment configuration and entities behaviors respectively, a labeled transition system is obtained by applying reaction rules to the environment configuration. Thirdly, policy modification proposals are proposed for deadlock states, violation states, and unreachable states based on the verification results on the labeled transition system. Finally, a case study concerned with a bank building automation access control system is conducted to evaluate the effectiveness of the proposed approach.

Key words: location-constrained access control system, model checking, bigraphs, reaction rules, verification

中图分类号: