Publication: Special Features of TLA + Temporal Logic of Actions for Verifying Access Control Policies
Дата
2021
Авторы
Kanner, A. M.
Kanner, T. M.
Journal Title
Journal ISSN
Volume Title
Издатель
Аннотация
© 2021 IEEE.The paper considers special features of applying Lamport's temporal logic of actions when verifying access control policies for arbitrary data protection tools. It justifies the necessity of implementing verification in the process of development and certification of various software tools and algorithms, in particular, policies for controlling subjects' access to objects. It contains a general structure of notation or specification of the system being studied in a formal language suitable for verification, and its particular version in the TLA + language. The paper considers special features of using Lamport's temporal logic of actions, and gives recommendations regarding dos and don'ts when initializing the modeled system, when forming and using invariants or temporal properties, history and auxiliary variables, safety and liveness properties, as well as when accounting for the termination of the verification process. Such features and recommendations are formulated in a quite universal way and do not depend on the applied verification approach and on the system being studied. The paper lists typical errors that may be done during verification, which make its results useless, while artificially creating a feeling of confidence in the system's 'rightness', 'correctness' or 'security / safety'. The conclusion presents key features that can have a significant impact on verification results, as well as on feasibility of its implementation. It proposes one of the possible directions for further research on the development of a general approach to substantiating conformity of the verified system specification in some formal language with its practical implementation.
Описание
Ключевые слова
Цитирование
Kanner, A. M. Special Features of TLA + Temporal Logic of Actions for Verifying Access Control Policies / Kanner, A.M., Kanner, T.M. // Proceedings - 2021 Ural Symposium on Biomedical Engineering, Radioelectronics and Information Technology, USBEREIT 2021. - 2021. - P. 411-414. - 10.1109/USBEREIT51232.2021.9455090