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 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.