位置约束的访问控制模型及验证方法
|
摘要
随着物联网和信息物理融合系统等新一代信息技术的发展,位置约束的访问控制系统的安全性需求不仅体现在虚拟的信息空间,还体现在现实的物理空间.如何在这种新需求下制定位置约束的访问控制模型与验证方法成为保证访问控制系统安全的关键所在.首先提出位置约束访问控制模型,包括LCRBAC模型和EM模型,实现对信息空间和物理空间的静态结构以及两空间中实体动态行为的刻画;其次利用偶图和偶图反应系统建模位置约束访问控制模型,生成访问控制策略标注转移边的标号变迁系统;然后根据标号变迁系统验证结果,提出针对死锁状态、违反状态和不可达状态的策略修改方案;最后通过银行访问控制系统实例分析说明所提方法能够对信息空间和物理空间以及两空间交互行为的访问控制策略进行建模和验证.
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.
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.
引文
[1]Dey A,Hightower J,Lara E D,et al.Location-based services[J].IEEE Pervasive Computing,2017,9(1):11-12
[2]Wang Senzhang,He Lifang,Stenneth L,et al.Estimating urban traffic congestions with multi-sourced data[C]//Proc of the 17th IEEE Int Conf on Mobile Data Management.Piscataway,NJ:IEEE,2016:82-91
[3]Wang Senzhang,Zhang Xiaoming,Cao Jianping,et al.Computing urban traffic congestions by incorporating sparse GPS probe data and social media data[J].ACM Trans on Information System,2017,35(4):1-30
[4]Chen Weihe,Ju Shiguang,Xue Anrong.Survey on the novel access control model of location-based serveice based on the spatial location of mobile user[J].Computer Science,2008,35(10):19-24(in Chinese)(陈伟鹤,鞠时光,薛安荣.基于移动用户位置的信息服务中的访问控制模型研究综述[J].计算机科学,2008,35(10):19-24)
[5]Rajkumar R R,Lee I,Sha L,et al.Cyber-physical systems:The next computing revolution[C]//Proc of the 47th Design Automation Conf.New York:ACM,2010:731-736
[6]Hu V C,Kuhn R.Access control policy verification[J].Computer,2016,49(12):80-83
[7]Sandhu R,Ferraiolo D,Kuhn R.The NIST model for rolebased access control:Towards a unified standard[C]//Proc of the 5th ACM Workshop on Role-Based Access Control.New York:ACM,2000:47-63
[8]Unal D,Akar O,Caglayan M U.Model checking of location and mobility related security policy specifications in ambient calculus[C]//Proc of the 5th Int Conf on Mathematical Methods,Models,and Architectures for Computer Network Security.Berlin:Springer,2010:155-168
[9]Cardelli L,Gordon A D.Mobile ambients[C]//Proc of the1st Int Conf on Foundations of Software Science and Computation Structure.Berlin:Springer,1998:140-155
[10]Milner R.Pure bigraphs:Structure and dynamics[J].Information and Computation,2006,204(1):60-122
[11]Damiani M L,Bertino E,Catania B,et al.GEO-RBAC:A spatially aware RBAC[J].ACM Trans on Information and System Security,2007,10(1):1-42
[12]Ray I,Kumar M,Yu Lijun.LRBAC:A location-aware rolebased access control model[C]//Proc of the 2nd Int Conf on Information Systems Security.Berlin:Springer,2006:147-161
[13]Zhang Hong,He Yeping,Shi Zhiguo.A formal model for access control with supporting spatial context[J].SCIENTIA SINICA Informationis,2007,37(2):254-271(in Chinese)(张宏,贺也平,石志国.一个支持空间上下文的访问控制形式模型[J].中国科学:信息科学,2007,37(2):254-271)
[14]Chandran S M,Joshi J B D.LoT-RBAC:A location and time-based RBAC model[C]//Proc of the 6th Int Conf on Web Information Systems Engineering.Berlin:Springer,2005:361-375
[15]Ray I,Toahchoodee M.A spatio-temporal role-based access control model[C]//Proc of the 21st IFIP Annual Conf on Data and Applications Security.Berlin:Springer,2007:211-226
[16]Abdunabi R,Al-Lail M,Ray I,et al.Specification,validation,and enforcement of a generalized spatio-temporal role-based access control model[J].IEEE Systems Journal,2013,7(3):501-515
[17]Abdunabi R,Ray I,France R.Specification and analysis of access control policies for mobile applications[C]//Proc of the 18th ACM Symp on Access Control Models and Technologies.New York:ACM,2013:173-184
[18]Fadhel A B,Bianculli D,Briand L.A comprehensive modeling framework for role-based access control policies[J].Journal of Systems and Software,2015,107:110-126
[19]Toahchoodee M,Ray I.On the formalization and analysis of a spatio-temporal role-based access control model[J].Journal of Computer Security,2011,19(3):399-452
[20]Toahchoodee M,Ray I,Anastasakis K,et al.Ensuring spatio-temporal access control for real-world applications[C]//Proc of the 14th ACM Symp on Access Control Models and Technologies.New York:ACM,2009:13-22
[21]Geepalla E,Bordbar B,Du X.Spatio-temporal role based access control for physical access control systems[C]//Proc of the 4th IEEE Int Conf on Emerging Security Technologies.Piscataway,NJ:IEEE,2013:39-42
[22]nal D,a4layan M U.A formal role-based access control model for security policies in multi-domain mobile networks[J].Computer Networks,2015,57(1):330-350
[23]nal D,a4layan M U.Spatiotemporal model checking of location and mobility related security policy specifications[J].Turkish Journal of Electrical Engineering &Computer Sciences,2013,21(1):144-173
[24]Tsigkanos C,Pasquale L,Ghezzi C,et al.On the interplay between cyber and physical spaces for adaptive security[J].IEEE Trans on Dependable and Secure Computing,2016(99):1-14
[25]Milner R.The Space and Motion of Communicating Agents[M].Cambridge,UK:Cambridge University Press,2009
[26]Clarke E M,Grumberg O,Peled D.Model Checking[M].Cambridge,MA:MIT Press,1999
[27]Li Ruixuan,Lu Jianfeng,Li Tianyi,et al.An approach for resolving inconsistency confilcts in access control policies[J].Chinese Journal of Computers,2013,36(6):1210-1223(in Chinese)(李瑞轩,鲁剑锋,李添翼,等.一种访问控制策略非一致性冲突消解方法[J].计算机学报,2013,36(6):1210-1223)
[28]Hu Hongxin,Ahn G J,Jorgensen J.Multiparty access control for online social networks:Model and mechanisms[J].IEEE Trans on Knowledge and Data Engineering,2013,25(7):1614-1627
[29]Bacci G,Grohmann D,Miculan M.DBtk:A toolkit for directed bigraphs[C]//Proc of the 3rd Int Conf on Algebra and Coalgebra in Computer Science.Berlin:Springer,2009:413-422
[30]Faithfull A J,Perrone G,Hildebrandt T T.Big red:A development environment for bigraphs[J].Electronic Communications of the Easst,2013,61:1-10
[31]Perrone G,Debois S,Hildebrandt T T.A verification environment for bigraphs[J].Innovations in Systems and Software Engineering,2013,9(2):95-104
[2]Wang Senzhang,He Lifang,Stenneth L,et al.Estimating urban traffic congestions with multi-sourced data[C]//Proc of the 17th IEEE Int Conf on Mobile Data Management.Piscataway,NJ:IEEE,2016:82-91
[3]Wang Senzhang,Zhang Xiaoming,Cao Jianping,et al.Computing urban traffic congestions by incorporating sparse GPS probe data and social media data[J].ACM Trans on Information System,2017,35(4):1-30
[4]Chen Weihe,Ju Shiguang,Xue Anrong.Survey on the novel access control model of location-based serveice based on the spatial location of mobile user[J].Computer Science,2008,35(10):19-24(in Chinese)(陈伟鹤,鞠时光,薛安荣.基于移动用户位置的信息服务中的访问控制模型研究综述[J].计算机科学,2008,35(10):19-24)
[5]Rajkumar R R,Lee I,Sha L,et al.Cyber-physical systems:The next computing revolution[C]//Proc of the 47th Design Automation Conf.New York:ACM,2010:731-736
[6]Hu V C,Kuhn R.Access control policy verification[J].Computer,2016,49(12):80-83
[7]Sandhu R,Ferraiolo D,Kuhn R.The NIST model for rolebased access control:Towards a unified standard[C]//Proc of the 5th ACM Workshop on Role-Based Access Control.New York:ACM,2000:47-63
[8]Unal D,Akar O,Caglayan M U.Model checking of location and mobility related security policy specifications in ambient calculus[C]//Proc of the 5th Int Conf on Mathematical Methods,Models,and Architectures for Computer Network Security.Berlin:Springer,2010:155-168
[9]Cardelli L,Gordon A D.Mobile ambients[C]//Proc of the1st Int Conf on Foundations of Software Science and Computation Structure.Berlin:Springer,1998:140-155
[10]Milner R.Pure bigraphs:Structure and dynamics[J].Information and Computation,2006,204(1):60-122
[11]Damiani M L,Bertino E,Catania B,et al.GEO-RBAC:A spatially aware RBAC[J].ACM Trans on Information and System Security,2007,10(1):1-42
[12]Ray I,Kumar M,Yu Lijun.LRBAC:A location-aware rolebased access control model[C]//Proc of the 2nd Int Conf on Information Systems Security.Berlin:Springer,2006:147-161
[13]Zhang Hong,He Yeping,Shi Zhiguo.A formal model for access control with supporting spatial context[J].SCIENTIA SINICA Informationis,2007,37(2):254-271(in Chinese)(张宏,贺也平,石志国.一个支持空间上下文的访问控制形式模型[J].中国科学:信息科学,2007,37(2):254-271)
[14]Chandran S M,Joshi J B D.LoT-RBAC:A location and time-based RBAC model[C]//Proc of the 6th Int Conf on Web Information Systems Engineering.Berlin:Springer,2005:361-375
[15]Ray I,Toahchoodee M.A spatio-temporal role-based access control model[C]//Proc of the 21st IFIP Annual Conf on Data and Applications Security.Berlin:Springer,2007:211-226
[16]Abdunabi R,Al-Lail M,Ray I,et al.Specification,validation,and enforcement of a generalized spatio-temporal role-based access control model[J].IEEE Systems Journal,2013,7(3):501-515
[17]Abdunabi R,Ray I,France R.Specification and analysis of access control policies for mobile applications[C]//Proc of the 18th ACM Symp on Access Control Models and Technologies.New York:ACM,2013:173-184
[18]Fadhel A B,Bianculli D,Briand L.A comprehensive modeling framework for role-based access control policies[J].Journal of Systems and Software,2015,107:110-126
[19]Toahchoodee M,Ray I.On the formalization and analysis of a spatio-temporal role-based access control model[J].Journal of Computer Security,2011,19(3):399-452
[20]Toahchoodee M,Ray I,Anastasakis K,et al.Ensuring spatio-temporal access control for real-world applications[C]//Proc of the 14th ACM Symp on Access Control Models and Technologies.New York:ACM,2009:13-22
[21]Geepalla E,Bordbar B,Du X.Spatio-temporal role based access control for physical access control systems[C]//Proc of the 4th IEEE Int Conf on Emerging Security Technologies.Piscataway,NJ:IEEE,2013:39-42
[22]nal D,a4layan M U.A formal role-based access control model for security policies in multi-domain mobile networks[J].Computer Networks,2015,57(1):330-350
[23]nal D,a4layan M U.Spatiotemporal model checking of location and mobility related security policy specifications[J].Turkish Journal of Electrical Engineering &Computer Sciences,2013,21(1):144-173
[24]Tsigkanos C,Pasquale L,Ghezzi C,et al.On the interplay between cyber and physical spaces for adaptive security[J].IEEE Trans on Dependable and Secure Computing,2016(99):1-14
[25]Milner R.The Space and Motion of Communicating Agents[M].Cambridge,UK:Cambridge University Press,2009
[26]Clarke E M,Grumberg O,Peled D.Model Checking[M].Cambridge,MA:MIT Press,1999
[27]Li Ruixuan,Lu Jianfeng,Li Tianyi,et al.An approach for resolving inconsistency confilcts in access control policies[J].Chinese Journal of Computers,2013,36(6):1210-1223(in Chinese)(李瑞轩,鲁剑锋,李添翼,等.一种访问控制策略非一致性冲突消解方法[J].计算机学报,2013,36(6):1210-1223)
[28]Hu Hongxin,Ahn G J,Jorgensen J.Multiparty access control for online social networks:Model and mechanisms[J].IEEE Trans on Knowledge and Data Engineering,2013,25(7):1614-1627
[29]Bacci G,Grohmann D,Miculan M.DBtk:A toolkit for directed bigraphs[C]//Proc of the 3rd Int Conf on Algebra and Coalgebra in Computer Science.Berlin:Springer,2009:413-422
[30]Faithfull A J,Perrone G,Hildebrandt T T.Big red:A development environment for bigraphs[J].Electronic Communications of the Easst,2013,61:1-10
[31]Perrone G,Debois S,Hildebrandt T T.A verification environment for bigraphs[J].Innovations in Systems and Software Engineering,2013,9(2):95-104