Specification and Verification of a Topology-Aware Access Control Model for Cyber-Physical Space
|
摘要
The cyber-physical space is a spatial environment that integrates the cyber and physical worlds to provide an intelligent environment for users to conduct their day-to-day activities. Mobile users and mobile objects are ubiquitous in this space, thereby exerting tremendous pressure on its security model. This model must ensure that both cyber and physical objects are always handled securely in this dynamic environment. In this paper,we propose a systematic solution to be able to specify security policies of the cyber-physical space and ensure that security requirements hold in these policies. We first formulate a topology configuration model to capture the topology characteristics of the cyber and physical worlds. Then, based on this model, a Topology-Aware CyberPhysical Access Control model(TA-CPAC) is proposed, which can ensure the security of the cyber and physical worlds at the same time by adjusting permission assignment dynamically. Then, the topology configuration and TA-CPAC models are formalized by bigraphs and Bigraph Reactive System(BRS), respectively, allowing us to use model checking to rationalize the consequences of the evolution of topological configurations on the satisfaction of security requirements. Finally, a case study on a building automation access control system is conducted to evaluate the effectiveness of the proposed approach.
The cyber-physical space is a spatial environment that integrates the cyber and physical worlds to provide an intelligent environment for users to conduct their day-to-day activities. Mobile users and mobile objects are ubiquitous in this space, thereby exerting tremendous pressure on its security model. This model must ensure that both cyber and physical objects are always handled securely in this dynamic environment. In this paper,we propose a systematic solution to be able to specify security policies of the cyber-physical space and ensure that security requirements hold in these policies. We first formulate a topology configuration model to capture the topology characteristics of the cyber and physical worlds. Then, based on this model, a Topology-Aware CyberPhysical Access Control model(TA-CPAC) is proposed, which can ensure the security of the cyber and physical worlds at the same time by adjusting permission assignment dynamically. Then, the topology configuration and TA-CPAC models are formalized by bigraphs and Bigraph Reactive System(BRS), respectively, allowing us to use model checking to rationalize the consequences of the evolution of topological configurations on the satisfaction of security requirements. Finally, a case study on a building automation access control system is conducted to evaluate the effectiveness of the proposed approach.
The cyber-physical space is a spatial environment that integrates the cyber and physical worlds to provide an intelligent environment for users to conduct their day-to-day activities. Mobile users and mobile objects are ubiquitous in this space, thereby exerting tremendous pressure on its security model. This model must ensure that both cyber and physical objects are always handled securely in this dynamic environment. In this paper,we propose a systematic solution to be able to specify security policies of the cyber-physical space and ensure that security requirements hold in these policies. We first formulate a topology configuration model to capture the topology characteristics of the cyber and physical worlds. Then, based on this model, a Topology-Aware CyberPhysical Access Control model(TA-CPAC) is proposed, which can ensure the security of the cyber and physical worlds at the same time by adjusting permission assignment dynamically. Then, the topology configuration and TA-CPAC models are formalized by bigraphs and Bigraph Reactive System(BRS), respectively, allowing us to use model checking to rationalize the consequences of the evolution of topological configurations on the satisfaction of security requirements. Finally, a case study on a building automation access control system is conducted to evaluate the effectiveness of the proposed approach.
引文
[1]C.Tsigkanos,L.Pasquale,C.Ghezzi,and B.Nuseibeh,On the interplay between cyber and physical spaces for adaptive security,IEEE Trans.Depend.Secure Comput.,vol.15,no.3,pp.466-480,2018.
[2]D.Chen,G.R.Chang,D.W.Sun,J.Jia,and X.W.Wang,Modeling access control for cyber-physical systems using reputation,Comput.Electr.Eng.,vol.38,no.5,pp.1088-1101,2012.
[3]M.Toahchoodee and I.Ray,On the formalization and analysis of a spatio-temporal role-based access control model,J.Comput.Secur.,vol.19,no.3,pp.399-452,2011.
[4]M.S.Kirkpatrick,M.L.Damiani,and E.Bertino,ProxRBAC:A proximity-based spatially aware RBAC,in Proc.19thACM Int.Conf.on Advances in Geographic Information Systems,Chicago,IL,USA,2011,pp.339-348.
[5]A.Gupta,M.S.Kirkpatrick,and E.Bertino,A formal proximity model for RBAC systems,Comput.Secur.,vol.41,pp.52-67,2014.
[6]A.B.Fadhel,D.Bianculli,and L.Briand,Acomprehensive modeling framework for role-based access control policies,J.Syst.Soft.,doi:10.1016/j.jss.2015.05.015.
[7]J.W.Huang,D.M.Nicol,R.Bobba,and J.H.Huh,Aframework integrating attribute-based policies into rolebased access control,in Proc.17thACM Symp.Access Control Models and Technologies,New York,NY,USA,2012,pp.187-196.
[8]X.Jin,R.Sandhu,and R.Krishnan,RABAC:Rolecentric attribute-based access control,in Proc.6thInt.Conf.Mathematical Methods,Models,and Architectures for Computer Network Security,St.Petersburg,Russia,2012,pp.84-96.
[9]N.Skandhakumar,F.Salim,J.Reid,F.Jason,and E.Dawson,Physical access control administration using building information models,presented at the 4thInt.Conf.Cyberspace Safety and Security,Melbourne,Australia,2012.
[10]F.Turkmen,S.Foley,B.O’Sullivan,W.Fitzgerald,T.Hadzic,S.Basagiannis,and M.Boubekeur,Explanations and relaxations for policy conflicts in physical access control,presented at the 25thInt.Conf.Tools with Artificial Intelligence,Herndon,VA,USA,2014.
[11]E.Geepalla,B.Bordbar,and X.F.Du,Spatio-temporal role based access control for physical access control systems,presented at the 14thInt.Conf.Emerging Security Technologies,Cambridge,UK,2013.
[12]C.Tsigkanos,T.Kehrer,and C.Ghezzi,Modeling and verification of evolving cyber-physical spaces,in Proc.11thJoint Meeting on Foundations of Software Engineering,New York,NY,USA,2017,pp.38-48.
[13]I.Ray and I.Ray,Access control challenges for cyberphysical systems,http://pdfs.semanticscholar.org/953a/5ef6ae9a1983469a0393f525f76d33191f94.pdf,2009.
[14]V.C.Hu and R.Kuhn,Access control policy verification,Computer,vol.49,no.12,pp.80-83,2016.
[15]X.Zhao and M.E.Johnson,Access governance:Flexibility with escalation and audit,in Proc.43rdHawaii Int.Conf.System Sciences,Washington,DC,USA,2010.
[16]V.C.Hu,D.R.Kuhn,T.Xie,and J.Hwang,Model checking for verification of mandatory access control models and properties,Int.J.Softw.Eng.Know.Eng.,vol.21,no.1,pp.103-127,2011.
[17]D.Unal and M.U.Caglayan,Spatiotemporal model checking of location and mobility related security policy specifications,Turk.J.Electr.Eng.Comput.Sci.,vol.21,no.1,pp.144-173,2013.
[18]D.Unal and M.U.Caglayan,A formal role-based access control model for security policies in multi-domain mobile networks,Comput.Networks,vol.57,no.1,pp.330-350,2013.
[19]S.Jha,N.H.Li,M.Tripunitara,Q.H.Wang,and W.Winsborough,Towards formal verification of rolebased access control policies,IEEE Trans.Depend.Secure Comput.,vol.5,no.4,pp.242-255,2008.
[20]A.Gouglidis,I.Mavridis,and V.C.Hu,Security policy verification for multi-domains in cloud systems,Int.J.Inf.Secur.,vol.13,no.2,pp.97-111,2014.
[21]M.Toahchoodee,I.Ray,K.Anastasakis,G.Georg,and B.Bordbar,Ensuring spatio-temporal access control for real-world applications,in Proc.14thACM Symp.Access Control Models and Technologies,New York,NY,USA,2009,pp.13-22.
[22]S.Mondal,S.Sural,and V.Atluri,Security analysis of GTRBAC and its variants using model checking,Comput.Secur.,vol.30,nos.2&3,pp.128-147,2011.
[23]L.Pasquale,C.Ghezzi,E.Pasi,C.Tsigkanos,M.Boubekeur,B.Florentino-Liano,T.Hadzic,and B.Nuseibeh,Topology-aware access control of smart spaces,Computer,vol.50,no.7,pp.54-63,2017.
[24]L.A.Walton and M.Worboys,A qualitative bigraph model for indoor space,presented at the 6thInt.Conf.Geographic Information Science,Berlin,Germany,2012.
[25]C.Tsigkanos,T.Kehrer,and C.Ghezzi,Architecting dynamic cyber-physical spaces,Computing,vol.98,no.10,pp.1011-1040,2016.
[26]S.Benford,M.Calder,T.Rodden,and M.Sevegnani,On lions,impala,and bigraphs:Modelling interactions in physical/virtual spaces,ACM Trans.Comput.-Human Interact.,vol.23,no.2,pp.1-56,2016.
[27]L.Pasquale,C.Ghezzi,C.Menghi,C.Menghi,and B.Nuseibeh,Topology aware adaptive security,in Proc.9th Int.Symp Software Engineering for Adaptive and SelfManaging Systems,New York,NY,USA,2014,pp.43-48.
[28]R.Milner,The Space and Motion of Communicating Agents.Cambridge,UK:Cambridge University Press,2009.
[29]G.Perrone,S.Debois,and T.T.Hildebrandt,A verification environment for bigraphs,Innovat.Syst.Soft.Eng.,vol.9,no.2,pp.95-104,2013.
[30]Y.Cao,Z.Q.Huang,S.L.Kan,H.F.Peng,and C.B.Ke,Location-constrainted access control model and verification methods,(in Chinese),J.Comput.Res.Dev.,vol.55,no.8,pp.1809-1825,2018.
[2]D.Chen,G.R.Chang,D.W.Sun,J.Jia,and X.W.Wang,Modeling access control for cyber-physical systems using reputation,Comput.Electr.Eng.,vol.38,no.5,pp.1088-1101,2012.
[3]M.Toahchoodee and I.Ray,On the formalization and analysis of a spatio-temporal role-based access control model,J.Comput.Secur.,vol.19,no.3,pp.399-452,2011.
[4]M.S.Kirkpatrick,M.L.Damiani,and E.Bertino,ProxRBAC:A proximity-based spatially aware RBAC,in Proc.19thACM Int.Conf.on Advances in Geographic Information Systems,Chicago,IL,USA,2011,pp.339-348.
[5]A.Gupta,M.S.Kirkpatrick,and E.Bertino,A formal proximity model for RBAC systems,Comput.Secur.,vol.41,pp.52-67,2014.
[6]A.B.Fadhel,D.Bianculli,and L.Briand,Acomprehensive modeling framework for role-based access control policies,J.Syst.Soft.,doi:10.1016/j.jss.2015.05.015.
[7]J.W.Huang,D.M.Nicol,R.Bobba,and J.H.Huh,Aframework integrating attribute-based policies into rolebased access control,in Proc.17thACM Symp.Access Control Models and Technologies,New York,NY,USA,2012,pp.187-196.
[8]X.Jin,R.Sandhu,and R.Krishnan,RABAC:Rolecentric attribute-based access control,in Proc.6thInt.Conf.Mathematical Methods,Models,and Architectures for Computer Network Security,St.Petersburg,Russia,2012,pp.84-96.
[9]N.Skandhakumar,F.Salim,J.Reid,F.Jason,and E.Dawson,Physical access control administration using building information models,presented at the 4thInt.Conf.Cyberspace Safety and Security,Melbourne,Australia,2012.
[10]F.Turkmen,S.Foley,B.O’Sullivan,W.Fitzgerald,T.Hadzic,S.Basagiannis,and M.Boubekeur,Explanations and relaxations for policy conflicts in physical access control,presented at the 25thInt.Conf.Tools with Artificial Intelligence,Herndon,VA,USA,2014.
[11]E.Geepalla,B.Bordbar,and X.F.Du,Spatio-temporal role based access control for physical access control systems,presented at the 14thInt.Conf.Emerging Security Technologies,Cambridge,UK,2013.
[12]C.Tsigkanos,T.Kehrer,and C.Ghezzi,Modeling and verification of evolving cyber-physical spaces,in Proc.11thJoint Meeting on Foundations of Software Engineering,New York,NY,USA,2017,pp.38-48.
[13]I.Ray and I.Ray,Access control challenges for cyberphysical systems,http://pdfs.semanticscholar.org/953a/5ef6ae9a1983469a0393f525f76d33191f94.pdf,2009.
[14]V.C.Hu and R.Kuhn,Access control policy verification,Computer,vol.49,no.12,pp.80-83,2016.
[15]X.Zhao and M.E.Johnson,Access governance:Flexibility with escalation and audit,in Proc.43rdHawaii Int.Conf.System Sciences,Washington,DC,USA,2010.
[16]V.C.Hu,D.R.Kuhn,T.Xie,and J.Hwang,Model checking for verification of mandatory access control models and properties,Int.J.Softw.Eng.Know.Eng.,vol.21,no.1,pp.103-127,2011.
[17]D.Unal and M.U.Caglayan,Spatiotemporal model checking of location and mobility related security policy specifications,Turk.J.Electr.Eng.Comput.Sci.,vol.21,no.1,pp.144-173,2013.
[18]D.Unal and M.U.Caglayan,A formal role-based access control model for security policies in multi-domain mobile networks,Comput.Networks,vol.57,no.1,pp.330-350,2013.
[19]S.Jha,N.H.Li,M.Tripunitara,Q.H.Wang,and W.Winsborough,Towards formal verification of rolebased access control policies,IEEE Trans.Depend.Secure Comput.,vol.5,no.4,pp.242-255,2008.
[20]A.Gouglidis,I.Mavridis,and V.C.Hu,Security policy verification for multi-domains in cloud systems,Int.J.Inf.Secur.,vol.13,no.2,pp.97-111,2014.
[21]M.Toahchoodee,I.Ray,K.Anastasakis,G.Georg,and B.Bordbar,Ensuring spatio-temporal access control for real-world applications,in Proc.14thACM Symp.Access Control Models and Technologies,New York,NY,USA,2009,pp.13-22.
[22]S.Mondal,S.Sural,and V.Atluri,Security analysis of GTRBAC and its variants using model checking,Comput.Secur.,vol.30,nos.2&3,pp.128-147,2011.
[23]L.Pasquale,C.Ghezzi,E.Pasi,C.Tsigkanos,M.Boubekeur,B.Florentino-Liano,T.Hadzic,and B.Nuseibeh,Topology-aware access control of smart spaces,Computer,vol.50,no.7,pp.54-63,2017.
[24]L.A.Walton and M.Worboys,A qualitative bigraph model for indoor space,presented at the 6thInt.Conf.Geographic Information Science,Berlin,Germany,2012.
[25]C.Tsigkanos,T.Kehrer,and C.Ghezzi,Architecting dynamic cyber-physical spaces,Computing,vol.98,no.10,pp.1011-1040,2016.
[26]S.Benford,M.Calder,T.Rodden,and M.Sevegnani,On lions,impala,and bigraphs:Modelling interactions in physical/virtual spaces,ACM Trans.Comput.-Human Interact.,vol.23,no.2,pp.1-56,2016.
[27]L.Pasquale,C.Ghezzi,C.Menghi,C.Menghi,and B.Nuseibeh,Topology aware adaptive security,in Proc.9th Int.Symp Software Engineering for Adaptive and SelfManaging Systems,New York,NY,USA,2014,pp.43-48.
[28]R.Milner,The Space and Motion of Communicating Agents.Cambridge,UK:Cambridge University Press,2009.
[29]G.Perrone,S.Debois,and T.T.Hildebrandt,A verification environment for bigraphs,Innovat.Syst.Soft.Eng.,vol.9,no.2,pp.95-104,2013.
[30]Y.Cao,Z.Q.Huang,S.L.Kan,H.F.Peng,and C.B.Ke,Location-constrainted access control model and verification methods,(in Chinese),J.Comput.Res.Dev.,vol.55,no.8,pp.1809-1825,2018.