On the problem of representation of the formal model of security policy for operating systems
https://doi.org/10.15514/ISPRAS-2017-29(3)-1
Abstract
In connection with the process of implementation by the Federal Service for Technical and Export Control of Russia "Information Security Requirements for Operating Systems", the work analyzes the ways of fulfilling the requirements of the functional component ADV_SPM.1 "Formal Security Policy Model", including defining the language, depth and detail of the presentation of the access control policy and information flows. Among other things, proposals are given on the composition of the main elements of the model, the use of tools for its verification. The practical possibility of applying the proposed approaches is considered by the example of the presentation of the description and verification of the mandatory entity-role security model for logical access control and information flows as the basis of the access control mechanism in the special-purpose operating system Astra Linux Special Edition.
About the Author
P. N. Devyanin
Federal Educational and Methodological Association of Higher Educational Institutions of Russia for Education in Information Security
Russian Federation
Russian Federation
References
1. Bishop M. Computer Security: art and science. ISBN 0-201-44099-7, 2002. 1084 p.
2. Devyanin P.N. Security models for computer systems. Control of access and information flows. Textbook for higher schools. 2nd ed. M.: Goryatchaya liniya - Telecom, 2013. 338 p (in Russian)
3. Bell D.E., LaPadula L.J. Secure Computer Systems: Unified Exposition and Multics Interpretation. Bedford, Mass.: MITRE Corp., 1976. MTR-2997 Rev. 1.
4. Information message on the approval of information security Requirements for operating systems, October 18, 2016. No 240/24/4893/ FSTEK Russian. URL: http://fstec.ru/component/attachments/download/1051.
5. GOST R ISO / IEC 15408-2013. Security techniques. Evaluation criteria for IT security. (in Russian).
6. GOST R ISO / IEC 18045-2013. Information technology - Security techniques - Methodology for IT security evaluation (in Russian)
7. Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
8. Operating system Astra Linux. URL: http://www.astra-linux.ru/ (in Russian).
9. P.V. Burenin, P.N. Devyanin, E.V. Lebedenko and others; Under the editorship of P.N. Devyanin. Security of the special-purpose operating system Astra Linux Special Edition. Textbook for high schools. 2nd edition, stereotyped. M.: Goryatchaya liniya - Telecom, 2016, 312 p. (in Russian)
10. P.N. Devyanin, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Using Refinement in Formal Development of OS Security Model. In Lecture Notes in Computer Sciences #9609 "Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference", Springer International Publishing, 2016, pp. 107-115. DOI: 10.1007/978-3-319-41579-6_9.
11. Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov. Comparison of Specification Decomposition Methods in Event-B. Programming and Computer Software, 2016, Vol. 42, No. 4, pp. 198-205. DOI: 10.1134/S0361768816040022
Review
For citations:
Devyanin P.N. On the problem of representation of the formal model of security policy for operating systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(3):7-16. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(3)-1
Email this article 