Verification of Access Control in Big Data Systems Using Temporal Logics

被引:0
作者
Poltavtseva, M. A. [1 ]
Podorov, A. A. [1 ]
Aleksandrova, E. B. [1 ]
机构
[1] Peter Great St Petersburg Polytech Univ, St Petersburg 195251, Russia
基金
俄罗斯科学基金会;
关键词
information security; big data; heterogeneous data processing systems; access control; verification; temporal logic; TLA;
D O I
10.3103/S0146411624700974
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Ensuring consistent access control is one of the key security challenges in heterogeneous big data systems. The problem is the large number of data processing tools, as well as sources and users of information; heterogeneity of security models; and complexity of granular access rules. Analysis of the time factor in this case will improve the consistency and reliability of access control. The aim of this study is to select a methodology and tools for implementing temporal logic in the processes of access control verification of big data systems. The types of temporal logic and verification methods based on the temporal logic of actions (TLAs) are analyzed. The use of TLA+ is proposed to solve the given problem and an example of the corresponding specification is given.
引用
收藏
页码:1311 / 1317
页数:7
相关论文
共 35 条
[1]  
Belyak A.A., 2022, SBORN NAUCHN STAT 8
[2]   Modeling and Analysis of Hadoop MapReduce Systems for Big Data Using Petri Nets [J].
Chiang, Dai-Lun ;
Wang, Sheng-Kuan ;
Wang, Yu-Ying ;
Lin, Yi-Nan ;
Hsieh, Tsang-Yen ;
Yang, Cheng-Ying ;
Shen, Victor R. L. ;
Ho, Hung-Wei .
APPLIED ARTIFICIAL INTELLIGENCE, 2021, 35 (01) :80-104
[3]   Technological Developments in Control Models Using Petri Nets for Smart Grids: A Review [J].
Contreras, Jose Ulises Castellanos ;
Urrego, Leonardo Rodriguez .
ENERGIES, 2023, 16 (08)
[4]  
Ding Z., 2023, 2023 IEEE INT C NETW, P1, DOI [10.1109/ICNSC58704.2023.10318998, DOI 10.1109/ICNSC58704.2023.10318998]
[5]  
Fatin A.D., 2022, Metody i Tekhnicheskie Sredstva Obespecheniya Bezopasnosti Informatsii, P19
[6]  
Gabbay Dov M., 2000, Temporal Logic: Mathematical Foundations and Computational Aspects, DOI [DOI 10.1093/OSO/9780198537687.001.0001, 10.1093/oso/ 9780198537687.001.0001]
[7]  
Garanina N, 2023, Arxiv, DOI [arXiv:2305.09130, 10.48550/arXiv.2305.09130, DOI 10.48550/ARXIV.2305.09130]
[8]   An access control model for medical big data based on clustering and risk [J].
Jiang, Rong ;
Han, Shanshan ;
Yu, Yimin ;
Ding, Weiping .
INFORMATION SCIENCES, 2023, 621 :691-707
[9]  
Kanner Andrey M., 2021, 2021 Ural Symposium on Biomedical Engineering, Radioelectronics and Information Technology (USBEREIT), P0411, DOI 10.1109/USBEREIT51232.2021.9455090
[10]  
Kanner A.M., 2021, Voprosy Zashchity Informatsii, P8, DOI [10.52190/2073-2600202138, DOI 10.52190/2073-2600202138]