Спецификация модели управления доступом на языке темпоральной логики действий Лэмпорта

В статье представлено описание модели управления доступом на языке темпоральной логики действий Лэмпорта, обеспечивающей выполнение требований мандатного контроля целостности и конфиденциальности с учетом информационных потоков по памяти. Отличительной особенностью модели является учет особенностей жизненного цикла электронных документов (задания прав к метаинформации и содержимому документа отдельно, ограничение числа копий документа). Для задания модели управления доступом был выбран язык темпоральной логики действий Лэмпорта, поскольку его нотация представляется наиболее близкой к общепринятой математической, выразительные возможности и инструментальные средства позволяют описывать и верифицировать системы, заданные в виде конечных автоматов. В модели определены следующие действия: создание/удаление субъекта, чтение, запись, дозапись ("слепая" запись), создание/удаление объекта, назначение/удаление прав доступа, вложение объекта в объект, исключение вложенного объекта, утверждение объекта (документа), отправка объекта (документа) в архив, отмена действия утвержденного объекта (документа), копирование объекта (документа). Также определены следующие инварианты: проверки типов (включает в себя проверку соответствия всех полей объектов, также проверку соответствия типу субъектов и проверку уникальности идентификаторов субъектов и объектов) и проверки безопасности (включает в себя проверку меток конфиденциальности и целостности взаимодействующих субъектов и объектов, а также корректность процедуры назначения прав доступа).

1. Девянин П.Н. О проблеме представления формальной модели политики безопасности операционных систем. Труды ИСП РАН, том 29, вып. 3, 2017 г., стр. 7-16. DOI: 10.15514/ISPRAS-2017-29(3)-1.

2. Девянин П.Н. Реализация невырожденной решётки уровней целостности в рамках иерархического представления МРОСЛ ДП-модели. ПДМ. Приложение, № 10, 2017 г., стр. 111-114. DOI: 10.17223/2226308X/10/44.

3. Девянин П.Н. Администрирование системы в рамках мандатной сущностно-ролевой ДП-модели управления доступом и информационными потоками в ОС семейства Linux. ПДМ. Приложение, № 4, 2013 г., стр. 22-40.

4. Девянин П.Н. Необходимые условия нарушения безопасности информационных потоков по времени в рамках МРОСЛ ДП-модели. ПДМ. Приложение, № 8, 2015 г., стр. 81-83. DOI:10.17223/2226308X/8/30.

5. Девянин П.Н. О результатах формирования иерархического представления МРОСЛ ДП-модели. ПДМ. Приложение, № 9, 2016 г., стр. 83-87. DOI: 10.17223/2226308X/9/32.

6. Девянин П.Н. Уровень запрещающих ролей иерархического представления МРОСЛ ДП-модели. ПДМ, № 39, 2018 г., стр. 58-71. DOI: 10.17223/20710410/39/5.

7. П.Н. Девянин и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. Институт системного программирования им. В. П. Иванникова РАН, 2018, 181 с. URL: http://www.ispras.ru /publications/2018/security_policy_modeling_and_verification.

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. Девянин П. Н. Условия безопасности информационных потоков по памяти в рамках МРОСЛ ДП-модели. ПДМ. Приложение, № 7, 2014 г., стр. 82-85.

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.