Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы

Проектирование механизма управления доступом в операционной системе (ОС), требующей высокого уровня доверия, является сложной задачей. Еще более сложной она стан овится, если требуется интеграция нескольких разнородных механизмов, таких как ролевое управление доступом (role-based access control, RBAC) и мандатное управление доступом (mandatory access control, MAC). Данная статья представляет результаты разработки иерархической интегрированной модели управления доступом и информационных потоков (hierarchical integrated model of access control and information flows, HIMACF), интегрирующей механизмы RBAC, MAC и мандатного контроля целостности (mandatory integrity control, MIC) с сохранением их ключевых свойств безопасности. Эта модель является дальнейшим развитием МРОСЛ-ДП-модели, она формализована на языке Event-B и ее корректность доказана формально. В иерархическом представлении модели каждый ее уровень (или модуль) представляет отдельный механизм управления доступом, благодаря чему модель может быть верифицирована помодульно, что снижает общую трудоемкость ее верификации за счет переиспользования при доказательстве корректности очередного уровня результатов верификации нижележащих уровней. Данная модель реализована в ОС Astra Linux Special Edition на основе инфраструктуры Linux Security Modules (LSM).

1. R.S. Sandhu, E.J. Coyne, H.L. Feinstein, C.E. Youman. Role-based access control models. Computer, vol. 29, no. 2, 1996, pp. 38-47.

2. S. Smalley, C. Vance, W. Salamon. Implementing SELinux as a linux security module. Technical Report 01-043, NAI Labs, 2001.

3. S. Smalley, R. Craig. Security Enhanced (SE) Android: Bringing Flexible MAC to Android. In Proc. of Network & Distributed System Security Symposium (NDSS), 2013, 18 p.

4. M. Conover. Analysis of the Windows Vista security model. Technical Report, Symantec Corp., 2008.

5. A. Cunningham, L. Hutchinson. OSX10.11 El Capitan: The Ars Technica Review. Available at: https://arstechnica.com/apple/2015/09/os-x-10-11-el-capitan-the-ars-technica-review/. Accessed 21 January 2019.

6. D.E. Bell, L.J. LaPadula. Secure Computer Systems: Mathematical Foundations. Technical Report ESD-TR-73-278 v.~1, (also MTR-2547, v.~1), Electronic Systems Division, AFSC, Hanscom AFB, 1973.

7. K.J. Biba. Integrity considerations for secure computer systems. Technical Report MTR-3153, The MITRE Corporation, 1977.

8. R. Sandhu. Role hierarchies and constraints for lattice-based access controls. Lecture Notes in Computer Science, vol. 1146, 1996, pp.65-79.

9. П.Н. Девянин. Модели безопасности компьютерных систем. Управлне доступом и информационными потоками. Горячая линия-Телеком, 2013, 338 стр. / P.N. Devyanin. Security models of computer systems. Control for access and information flows. Hotline-Telecom, 2013, 338 p. (in Russian).

10. P.N. Devyanin, A.V. Khoroshilov, V.V. Kuliamin, A.K. Petrenko, I.V. Shchepetkov. Formal Verification of OS Security Model with Alloy and Event-B. Lecture Notes in Computer Science, vol. 8477, 2014, pp. 309-313.

11. J.R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010, 612 p.

12. J.R. Abrial, M. Butler, S. Hallerstede, T.S. Hoang, F. Mehta, L. Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, vol. 12, no. 6, 2010, pp. 447-466.

13. ISO/IEC 15408-1:2009. Information technology – Security techniques – Evaluation criteria for IT security – Part 1: Introduction and general model. ISO, 2009.

14. ISO/IEC 15408-2:2008. Information technology – Security techniques – Evaluation criteria for IT security – Part 2: Security functional components. ISO, 2008.

15. Astra Linux. Available at: https://en.wikipedia.org/wiki/Astra_Linux. Accessed 21 January 2019.

16. American National Standard for Information Technology – Role Based Access Control. ANSI INCITS 359-2004, 2004.

17. D.E. Bell, L.J. LaPadula. Secure Computer System: Unified Exposition and MULTICS Interpretation. Technical Report ESD-TR-75-306 (also MTR-2997), Electronic Systems Division, AFSC, Hanscom AFB, 1976.

18. A.K. Jones, R.J. Lipton, L. Snyder. A linear time algorithm for deciding security. In Proc. of 17-th Annual Symposium on Foundations of Computer Science, 1976, pp. 33-41.

19. M. Bishop, L. Snyder. The Transfer of Information and Authority in a Protection System. In Proc. of 7th ACM Symposium on Operating System Principles, 1979, pp. 45-54.

20. C.E. Landwehr, C.L. Heitmeyer, J. McLean. A security model for military message systems. ACM Transactions on Computer Systems, vol. 2, issue 3, 1984, pp. 198-222.

21. Security-Enhanced Linux. Available at: https://www.nsa.gov/what-we-do/research/selinux/. Accessed 21 January 2019.

22. PostgreSQL. Available at: https://en.wikipedia.org/wiki/PostgreSQL. Accessed 21 January 2019.

23. D-Bus. Available at: https://en.wikipedia.org/wiki/D-Bus. Accessed 21 January 2019.

24. X Window System. Available at: https://en.wikipedia.org/wiki/X_Window_System. Accessed 21 January 2019.

25. A. Eaman, B. Sistany, A. Felty. Review of Existing Analysis Tools for SELinux Security Policies: Challenges and a Proposed Solution. Lecture Notes in Business Information Processing, vol. 289, 2017, pp. 116-135.

26. G. Zanin, L.V. Mancini. Towards a Formal Model for Security Policies Specification and Validation in the Selinux System. In Proc. of 9th ACM Symposium on Access Control Models and Technologies, 2004, pp. 136-145.

27. G. Zhai, T. Guo, J. Huang. SCIATool: A Tool for Analyzing SELinux Policies Based on Access Control Spaces, Information Flows and CPNs. Lecture Notes in Computer Science, vol. 9473, 2015, pp. 294-309.

28. P. Amthor, W.E. Kühnhauser, A. Pölck. Model-based safety analysis of SELinux security policies. In Proc. of 5th International Conference on Network and System Security (NSS), 2011, pp. 208-215.

29. M.A. Harrison, W.L. Ruzzo, J.D. Ullman. Protection in operating systems. Communications of the ACM, vol. 19, no. 8, 1976, pp. 461-471.

30. B. Hicks, S. Rueda, L. St.Clair, T. Jaeger, P. McDaniel. A logical specification and analysis for SELinux MLS policy. ACM Transactions on Information and System Security, vol. 13, issue 3, 2010, article no. 26.

31. M.C. Tschantz. The clarity of languages for access-control policies. PhD Thesis, Brown University, Providence, Rhode Island, USA, 2005.

32. R. Sandhu, V. Bhamidipati, Q. Munawer. The ARBAC97 model for role-based administration of roles. ACM Transactions on Information and System Security, vol. 2, issue 1, 1999, pp. 105-135.

33. П.Н. Девянин, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Сравнение способов декомпозиции спецификаций на Event-B. Программирование, vol. 42, no. 4, 2016, pp. 17-26 / P.N. Devyanin, V.V. Kuliamin, 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.

34. J.C. Filliâtre, A.Paskevich. Why3 – Where Programs Meet Provers. Lecture Notes in Computer Science, vol. 7792, 2013, pp. 125-128.

35. D. Efremov, M. Mandrykin, A. Khoroshilov. Deductive verification of unmodified Linux kernel library functions. Lecture Notes in Computer Science, vol. 11245, 2018, pp. 216-234.