Verification of access control in big data systems using temporal logics

Ensuring consistent access control is one of the key security challenges in heterogeneous Big Data systems. The problem is presented by the large number of data processing tools, information sources and users; heterogeneity of security models; complexity of granular access rules. Analyzing the time factor in this case will improve the consistency and reliability of access differentiation. The aim of the work is to select a methodology and tools for the implementation of temporal logic in the verification processes of access control of Big Data systems. The paper analyzes types of temporal logic and verification methods based on TLA (temporal logic of actions). We propose the use of TLA+ to solve this problem and give an example of the corresponding specification