A Model Checking Based Approach for Verification of Attribute-Based Access Control Policies in Cloud Infrastructures
- 13 Downloads
Attribute-Based Access Control (ABAC) model is a perspective access control model for cloud infrastructures used for automation of industrial, transport and energy systems as they include large number of users, resources and dynamical changed permissions. The paper considers the features of ABAC model and the theoretical background for verification of the ABAC policies based on the model checking. The possibility of applying the model checking is justified on the example of the ABAC policy. Implementation of the proposed approach was made using the UPPAAL verification tool. Experimental assessment shows high acceptability of the model checking not only for finding anomalies in ABAC policies but for finding decisions to eliminate them.
KeywordsAccess control Model checking Temporal logics ABAC Cloud infrastructure
This work was partially supported by grants of RFBR (projects No. 16-29-09482, 18-07-01369, 18-07-01488, 18-37-20047, 18-29-22034, 18-37-20047, 19-07-00953, 19-07-01246), by the budget (the project No. 0073-2019-0002), and by Government of Russian Federation (Grant 08-08).
- 2.Clarke, E.M., Grumberg, O., Peled, D.: Model checking (2000)Google Scholar
- 4.Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th International Conference on Software Engineering, pp. 196–205. ACM (2005)Google Scholar
- 6.Hu, V.: Attribute based access control (ABAC) definition and considerations. Tech. rep, National Institute of Standards and Technology (2014)Google Scholar
- 10.Kolomeets, M., Chechulin, A., Kotenko, I., Saenko, I.: Access control visualization using triangular matrices. In: 2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pp. 348–355. IEEE (2019)Google Scholar
- 11.Kolovski, V., Hendler, J., Parsia, B.: Analyzing web access control policies. In: Proceedings of the 16th International Conference on World Wide Web, pp. 677–686. ACM (2007)Google Scholar
- 12.Kotenko, I., Polubelova, O.: Verification of security policy filtering rules by model checking. In: Proceedings of the 6th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems, vol. 2, pp. 706–710. IEEE (2011)Google Scholar
- 15.Lee, A.J.: Credential-based access control. In: Encyclopedia of Cryptography and Security, pp. 271–272 (2011)Google Scholar
- 18.Mocanu, D., Turkmen, F., Liotta, A., et al.: Towards ABAC policy mining from logs with deep learning. In: Proceedings of the 18th International Multiconference, IS2015, pp. 124–128 (2015)Google Scholar
- 19.Rothmaier, G., Kneiphoff, T., Krumm, H.: Using spin and eclipse for optimized high-level modeling and analysis of computer network attack models. In: International SPIN Workshop on Model Checking of Software, pp. 236–250. Springer (2005)Google Scholar