TLA+ based access control model specification
https://doi.org/10.15514/ISPRAS-2018-30(5)-9
Abstract
The article describes TLA+ access control model specification for computer systems, ensuring compliance with the mandatory integrity and confidentiality monitoring requirements with considering memory-based covert channels. The distinctive feature of the model is taking into account the characteristics of the lifecycle of electronic documents and their operating procedure. To specify the access control model, Lamport's Temporal Logic of Actions language was chosen (TLA+). Its notation seems to be the closest to generally accepted mathematical notation and its expressive capabilities and tools allow describing and verifying systems specified as finite automata. The following actions are defined in the model: create/delete a subject, read, write, append (blind write), create/delete an object, grant/remove access rights, include an object, exclude a nested object, approve an object (document), archive an object (document), cancel an approved object (document), copy an object (document). The following invariants are also defined: the type invariant (includes checking the compliance of all fields of the object, the compliance of the subject type, the uniqueness of the subject and object identifiers) and the safety invariant (includes checking the confidentiality and integrity labels of the interacting subjects and objects, the correctness of rights assignment procedures).
References
1. Devyanin P.N. On the problem of representation of the formal model of security policy for operating systems. Trudy ISP RAN/Proc. ISP RAS. vol. 29, issue 3, 2017, pp. 7-16 (in Russian). DOI: 10.15514/ISPRAS-2017-29(3)-1.
2. Devyanin P. N. Approaches to formal modelling access control in postgresql within framework of the mrosl DP-mode. PDM. Prilozhenie/Applied Discrete Mathematics. Supplement, no. 10, 2017, pp. 111-114 (in Russian.) DOI: 10.17223/2226308X/10/44.
3. Devyanin P. N. System administration in MROSL DP-model. PDM/Applied Discrete Mathematics. Supplement, 2013, no 4, pp. 22-40 (in Russian).
4. Devyanin P. N. Security violation necessary conditions for time information flows in MROSL DP-model. PDM. Prilozhenie/Applied Discrete Mathematics. Supplement, no 8, 2015, pp. 81-83 (in Russian) DOI: 10.17223/2226308X/8/30.
5. Devyanin P. N. About results of designing hierarchical representation of mrosl DP-model. PDM. Prilozhenie/Applied Discrete Mathematics. Supplement, 2016, no 9. pp. 83-87 (in Russian) DOI: 10.17223/2226308X/9/32.
6. Devyanin P. N. The level of negative roles of the hierarchical representation of MROSL DP-model. PDM/Applied Discrete Mathematics, 2018, no 39, pp. 58-71 (in Russian) DOI: 10.17223/20710410/39/5.
7. P.N. Devyanin et al. Modeling and verification of security policies for access management in operating systems. ISP RAN, 2018, 181 p. Available at: http://www.ispras.ru/publications/security_policy_modeling_and_verification.pdf (in Russian)
8. Jackson D. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2012, 376 p.
9. Abrial J.-R. The B-book: Assigning Programs to Meanings. Cambridge University Press, 1996, 779 p.
10. Jean-Raymond Abrial. Modeling in Event-B. System and Software Engineering. Cambridge University Press, 2010.
11. P.N. Devyanin, V. V. Kulyamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Comparison of specification decomposition methods in Event-B. Programming and Computer Software, vol. 42, no. 4, 2016, pp. 198-205. DOI: 10.1134/S0361768816040022.
12. Jones C. B. Systematic Software Development Using VDM (2nd Ed.). Prentice-Hall, Inc., 1990, 333 p.
13. Singh M., Sharma A. K., Saxena R. Formal Transformation of UML Diagram: Use Case, Class, Sequence Diagram with Z Notation for Representing the Static and Dynamic Perspectives of System. Proc. of the International Conference on ICT for Sustainable Developmen, 2016, pp. 25-38, DOI: 10.1007/978-981-10-0135-2_3.
14. Lamport L. The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst, vol. 16, no. 3, 1994, pp. 872-923.
15. Lamport L. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
16. L. Lamport et al. Specifying and verifying systems with TLA+. Proc. of the 10th ACM SIGOPS European Workshop, 2002, pp. 45-48.
17. Lamport L. The PlusCAL Algorithm Language. Lecture Notes in Computer Science, vol. 4229, 2006, pp. 23-23. DOI: 10.1007/11888116_2.
18. Devyanin P. N. Security conditions for information flows by memory within the mrosl DP-model. PDM. Prilozhenie/Applied Discrete Mathematics. Supplement, issue 7, 2014, pp. 82-85 (in Russian).
19. Denis Cousineau et al. TLA + Proofs. Lecture Notes in Computer, vol. 7436, 2012, pp. 147-154. DOI: 10.1007/978-3-642-32759-9_14.
20. Kaustuv Chaudhuri et al. A TLA+ Proof System. In Proc. of the Combined KEAPPA - IWIL Workshops, 2008, pp. 17-37, URL: http://ceur-ws.org/Vol-418/paper2.pdf.
21. Merz S., Vanzetto H. Encoding TLA+ into Many-Sorted First-Order Logic. In Proc. of the 5th International Conference on Abstract State Machines, 2016, pp. 54-69.
22. Xinwen Zhang et al. Formal Model and Policy Specification of Usage Control. ACM Transactions on Information and System Security, vol. 8, no. 4, 2005, pp. 351-387. DOI: 10.1145/1108906.1108908.
23. Gouglidis A., Grompanopoulos C., Mavridou A. Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+. In Proc. of the 1st International Workshop on Methods and Tools for Rigorous System Design, 2018, pp. 52-64.
24. Stirling C. Modal and temporal logics. LFCS, Department of Computer Science, University of Edinburgh, 1991.
25. McMillan K. L. Eager Abstraction for Symbolic Model Checking. Lecture Notes in Computer Science, vol. 10981, 2018, pp. 191-208. DOI: 10.1007/978-3-319-96145-3_11.
26. Storey V. C., Song I.-Y. Big data technologies and Management: What conceptual modeling can do. Data & Knowledge Engineering, vol. 108, 2017, pp. 50-67. DOI: 10.1016/j.datak.2017.01.001.
27. Chris Newcombe et al. How AmazonWeb Services Uses Formal. Communications of the ACM, vol. 58, no. 4, 2015, pp. 66-73.
Review
For citations:
Kozachok A.V. TLA+ based access control model specification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(5):147-162. (In Russ.) https://doi.org/10.15514/ISPRAS-2018-30(5)-9
Email this article 