Литература

  1. Операционные системы Astra Linux. URL: http://www.astralinux.ru
  2. Astra Linux сертифицирована по требованиям ФСТЭК России к операционным системам (2017). URL: http://old.astra-linux.su/home/novosti/437-rbt-fstec.html
  3. Буренин П.В., Девянин П.Н., Лебеденко Е.В. и др. Безопасность операционной системы специального назначения Astra Linux Special Edition. Учебное пособие для вузов / Под ред. д-ра техн. наук П.Н. Девянина. 2-е издание, стереотипное. М.: Горячая линия Телеком, 2016. 312 с.
  4. ГОСТ Р ИСО/МЭК 15408-1-2012. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 1. Введение и общая модель.
  5. ГОСТ Р ИСО/МЭК 15408-2-2013. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 2. Функциональные компоненты безопасности.
  6. ГОСТ Р ИСО/МЭК 15408-3-2013. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности.
  7. Bell D.E., LaPadula L.J. Secure Computer Systems: Unified Exposition and Multics Interpretation. Bedford, Mass.: MITRE Corp., 1976. MTR-2997 Rev. 1.
  8. Bishop M. Computer Security: art and science. ISBN 0-201-44099-7, 2002. 1084 p.
  9. Девянин П.Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками. Учебное пособие для вузов. 2-е изд., испр. и доп. М.: Горячая линия Телеком, 2013. 338 с.
  10. Thumser W. Formal Specification of Security Policy Models // Proc. of The 7th International Common Criteria Conference, Spain, 2006.
  11. Trusted Computer System Evaluation Criteria. US Department Of Defense, 1985. CSC-STD-001-83.
  12. Гостехкомиссия России. Руководящий документ. Средства вычислительной техники защита от несанкционированного доступа к информации показатели защищенности от несанкционированного доступа к информации. М.: Военное издательство, 1992.
  13. Профиль защиты операционных систем типа «A» третьего класса защиты. Методический документ. ФСТЭК России, 2017.
  14. Профиль защиты операционных систем типа «A» второго класса защиты. Методический документ. ФСТЭК России, 2017.
  15. Информационное сообщение об утверждении Требований безопасности информации к операционным системам от 18 октября 2016 г. № 240/24/4893 / ФСТЭК России. URL: http://fstec.ru/component/attachments/download/1051
  16. Security-Enhanced Linux. URL: http://www.nsa.gov/research/selinux.index.shtml
  17. Документы по сертификации средств защиты информации и аттестации объектов информатизации по требованиям безопасности информации. URL: http://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty
  18. ГОСТ Р ИСО/МЭК 18045-2013. Информационная технология. Методы и средства обеспечения безопасности. Методология оценки безопасности информационных технологий.
  19. ГОСТ Р 53113.1-2008. Информационная технология. Защита информационных технологий и автоматизированных систем от угроз информационной безопасности, реализуемых с использованием скрытых каналов. Часть 1. Общие положения.
  20. Девянин П.Н. О запрещенных информационных потоках по времени через параметры сущностей в операционных системах семейства Linux с мандатным управлением доступом // Методы и технические средства обеспечения безопасности информации: Материалы 21-й научно-технической конференции 24 июня 29 июня 2012 года. СПб.: Изд-во Политехн. ун-та, 2012. С. 88–90.
  21. Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
  22. Biba K. Integrity considerations for secure computer systems. Technical Report MTR-3153, The MITRE Corporation. 1975.
  23. Девянин П.Н. Анализ безопасности управления доступом и информационными потоками в компьютерных системах. М.: Радио и связь, 2006. 176 с.
  24. Назаров И.О. Анализ безопасности веб-систем, в условиях реализации уязвимости класса межсайтового скриптинга // Проблемы информационной безопасности. Компьютерные системы / Под ред. П.Д. Зегжды. Выпуск 2, 2007. С. 105–117.
  25. Назаров И.О. Обеспечение безопасности управления доступом и информационными потоками в веб-системе на основе СУБД // Вестник Казанского государственного технического университета им. А.Н. Туполева. Выпуск 2, 2008. С. 56–59.
  26. Колегов Д.Н. ДП-модель компьютерной системы с функционально и параметрически ассоциированными с субъектами сущностями // Вестник Сибирского государственного аэрокосмического университета им. академика М.Ф. Решетнева. Вып. 1(22), 2009. Часть 1. С. 49–54.
  27. Буренин П.В. Подходы к построению ДП-модели файловых систем // Прикладная дискретная математика. 2009. № 1(3). С. 93–112.
  28. Девянин П.Н. Базовая ролевая ДП-модель // Прикладная дискретная математика. 2008. № 1(1). С. 64–70.
  29. Девянин П.Н. Ролевая ДП-модель управления доступом и информационными потоками в операционных системах семейства Linux // Прикладная дискретная математика. 2012. № 1(15). С. 69–90.
  30. Девянин П.Н. О результатах формирования иерархического представления МРОСЛ ДП-модели // Прикладная дискретная математика. 2016. Приложение № 9. С. 83–87.
  31. Тележников В.Ю. Правила преобразования состояний системы в рамках ДП-модели управления доступом в компьютерных сетях, построенных на основе ОС семейства Linux // Прикладная дискретная математика. 2016. № 1(31). С. 67–85.
  32. Программный комплекс «Виртуализации и управления». URL: http://old.astra-linux.su/doc-pkviu.html
  33. Девянин П.Н. Реализация невырожденной решетки уровней целостности в рамках иерархического представления МРОСЛ ДП-модели // Прикладная дискретная математика. 2017. Приложение № 10. С. 111–114.
  34. Способ обеспечения безопасности информационных потоков в защищенных информационных системах с мандатным и ролевым управлением доступом: пат. 2525481 Рос. Федерация: МПК G 06 F 21/62 / Девянин П.Н.; патентообладатели Девянин П.Н. и ОАО «НПО РусБИТех». № 2012146550/08; заявл. 01.11.2012; опубл. 10.05.2014, Бюл. № 13. 12 с.
  35. Sandhu R. Rationale for the RBAC96 family of access control models // Proceeding of the 1st ACM Workshop on Role-Based Access Control. ACM, 1997.
  36. Sandhu R. Role-Based Access Control // Advanced in Computers. Academic Press, 1998. Vol. 46.
  37. Rodin Handbook. http://handbook.event-b.org
  38. Gurevich Y. Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9-36. Oxford University Press, Oxford, 1995.
  39. Jackson D. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, 2006.
  40. Abrial J.-R. The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, 1996.
  41. Lamport L. Specifying Concurrent Systems with TLA+. NATO Science Series, III: Computer and Systems Sciences. IOS Press, Amsterdam. 173 (Calculational System Design): 183–247, 2000.
  42. Bjorner D., Jones C.B. The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science 61. Berlin, Heidelberg, New York: Springer, 1978.
  43. Abrial J.-R. Data Semantics // Klimbie J.W., Koffeman K.L. Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59, 1974.
  44. Abrial J.-R., Butler M., Hallerstede S. et al. Rodin: An Open Toolset for Modelling and Reasoning in Event-B // International Journal on Software Tools for Technology Transfer. 2010. Vol. 12, no. 6. P. 447–466.
  45. AstraVer Toolset URL: https://forge.ispras.ru/projects/astraver-toolset
  46. Wirth N. Program development by stepwise refinement // CACM: Communications of the ACM 14 (1971).
  47. Abrial J.-R., Hallerstede S. Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamentae // Informatica. 2007. 77(1,2). 1–28.
  48. Bourdonov I., Kossatchev A., Petrenko A., Galter D. KVEST: Automated Generation of Test Suites from Formal Specifications // FM’99: Formal Methods. LNCS, vol. 1708, pp. 608–621, Springer-Verlag, 1999.
  49. Microsoft Interoperability Initiative. URL: http://www.microsoft.com/openspecifications
  50. OLVER project. URL: http://linuxtesting.org
  51. George C., Haxthausen A.E., Hughes S., Milne R., Prehn S., Pedersen J.S. The Raise Development Method. London: Prentice-Hall International, 1995.
  52. Baudin P., Filliâtre J. C., Marché C., Monate B., Moy Y., Prevosto V. ACSL: ANSI C Specification Language. ver 1.12, 2017.
  53. Shutemov K. Kernel: use the gnu89 standard explicitly // Журнал разработки ядра ОС Linux, Октябрь 2014. URL: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=51b97e354ba9fce1890cf38ecc754aa49677fc89
  54. Edge J. LSM: loadable or static? LWN.net, Октябрь 2007. URL: https://lwn.net/Articles/255650/
  55. Wright C., Cowan C., Smalley S., Morris J., Kroah-Hartman G. Linux Security Module Framework // Ottawa Linux Symposium, 2002. URL: http://www.kroah.com/linux/talks/ols_2002_lsm_paper/lsm.pdf
  56. Wright C., Cowan C., Morris J., Smalley S. and Kroah-Hartman G.: Linux security modules: general security support for the linux kernel. Foundations of Intrusion Tolerant Systems, 2003 [Organically Assured and Survivable Information Systems], 2003, pp. 213-226. doi: 10.1109/FITS.2003.1264934. URL: https://www.usenix.org/legacy/event/sec02/full_papers/wright/wright.pdf
  57. Edge J. Progress in security module stacking // LWN.net, Март 2015. URL: https://lwn.net/Articles/635771
  58. Zhang X., Edwards A., Jaeger T. Using CQUAL for Static Analysis of Authorization Hook Placement // Proceedings of the 11th USENIX Security Symposium, D. Boneh (Ed.), 2002, USENIX Association, Berkeley, CA, USA, 33-48. URL: https://www.usenix.org/legacy/event/sec02/full_papers/zhang/zhang.pdf
  59. Edwards A., Jaeger T., Zhang X. Runtime verification of authorization hook placement for the linux security modules framework // Proceedings of the 9th ACM conference on Computer and communications security (CCS ’02), 2002, V. Atluri (Ed.). ACM, New York, NY, USA, 225–234. doi: 10.1145/586110.58614
  60. Jaeger T., Edwards A., Zhang, X. Consistency analysis of authorization hook placement in the Linux security modules framework // ACM Trans. Inf. Syst. Secur. 7, 2 (May 2004), 175–205. doi: 10.1145/996943.99694
  61. Ganapathy V., Jaeger T., Jha S. Automatic placement of authorization hooks in the linux security modules framework // Proceedings of the 12th ACM conference on Computer and communications security (CCS ’05), 2005, ACM, New York, NY, USA, 330–339. doi: 10.1145/1102120.110216
  62. Zheng, Y.: ceph: fix security xattr deadlock. Лог разработки ядра, Март 2016. URL: https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=315f24088048a51eed341c53be66ea477a3c7d1
  63. Floyd R. Assigning Meanings to Programs // Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, American Mathematical Society, Providence, Rhode Island, 1967, pp. 19–32.
  64. Hoare C.A.R. An Axiomatic Basis for Computer Programming // Comm. ACM 12, 10 (1969), 576-583.
  65. King J.C. A Program Verifier. Ph.D. Th., Carnegie-Mellon University, 1969.
  66. Boyer R.S., Moore J.S. A Verification Condition Generator for FOR-TRAN // The Correctness Problem in Computer Science, R.S. Boyer and J.S. Moore, Eds. London: Academic Press, 1981.
  67. Tschannen J., Carlo F., Nordio M., Polikarpova N. AutoProof: Autoactive Functional Verification of Object-oriented Programs // Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 15, 2015.
  68. Chapman R., Schanda F. Are we there yet? 20 years of industrial theorem proving with SPARK // International Conference on Interactive Theorem Proving, Springer, Cham, 2014, pp. 17–26.
  69. Pearce D.J., Groves L. Whiley: a platform for research in software verification // International Conference on Software Language Engineering, Springer, Cham, 2013, pp. 238–248.
  70. Leino, K.R.M. Dafny: An automatic program verifier for functional correctness // International Conference on Logic for Programming Artificial Intelligence and Reasoning, Springer, Berlin, Heidelberg, 2010, pp. 348–370.
  71. Filliâtre J.C., Paskevich A. Why3 where programs meet provers // European Symposium on Programming, Springer, Berlin, Heidelberg, 2013, pp. 125–128.
  72. Leroy X. et al. The CompCert verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt, 2012.
  73. Klein G. et al. seL4: Formal verification of an OS kernel // Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, ACM, 2009, pp. 207–220.
  74. Cok D.R., Blissard I., Robbins J. C Library annotations in ACSL for Frama-C: experience report. GrammaTech Inc., 2017. URL: http://annotationsforall.org/resources/links/GT-libc-experience-report.pdf
  75. Pariente D., Ledinot E. Formal verification of industrial C code using Frama-C: a case study. Formal Verification of Object-Oriented Software, 2010, 205 pp.
  76. Мандрыкин М., Хорошилов А. Высокоуровневая модель памяти промежуточного языка Jessie с поддержкой произвольного приведения типов указателей // Программирование. 2015. № 4. С. 23–39.
  77. Мандрыкин М. Моделирование памяти Си-программ для инструментов статической верификации на основе SMT-решателей. Диссертация. М., 2016.
  78. Barnes J. Rationale for Ada 2012: Contracts and aspects. January 2013, DOI: 10.1007/978-3-642-45210-9
  79. Мейер Б. Объектно-ориентированное конструирование программных систем. М.: Русская редакция, 2004. 1204 с.
  80. AstraVer Project. ИСП РАН им. В.П. Иванникова. URL: http://linuxtesting.ru/astraver
  81. Kirchner F., Kosmatov N., Prevosto V., Signoles J., & Yakobowski B. Frama-C: a software analysis perspective // Formal Aspects of Computing. 2015. 27(3). P. 573-609.
  82. Marché C., Moy Y. The Jessie plugin for deductive verification in Frama-C. INRIA Saclay Île-de-France and LRI, CNRS UMR, 2012.
  83. Gouw S., Boer F., Bubel R., Hähnle R., Rot J., Steinhöfel D. Verifying OpenJDK’s Sort Method for Generic Collections // Journal of Automated Reasoning. 2017. URL: https://doi.org/10.1007/s10817-017-9426-4 URL: https://github.com/abstools/java-timsort-bug/blob/master/KeY/src/java/util/TimSort.java
  84. AstraVer Toolset. ИСП РАН им. В.П. Иванникова. URL: http://linuxtesting.ru/astraver
  85. MISRA C: 2012. Guidelines for the Use of the C Language in Critical Systems, ISBN 978-1-906400-10-1 (paperback), ISBN 978-1-906400-11-8 (PDF), March 2013.
  86. Watson A., Wallace D., McCabe, T. Structured testing: A testing methodology using the cyclomatic complexity metric. US Department of Commerce, Technology Administration, National Institute of Standards and Technology, 1996, 500-235, 140 p.
  87. Howells D. Credentials in Linux. URL: https://www.kernel.org/doc/Documentation/security/credentials.txt
  88. Wright C. LSM update, another missing hook. Linux kernel log, lwn.net, 2005. URL: https://lwn.net/Articles/155496/
  89. Georget L. Add missing LSM hooks in mq_timed{send,receive} and splice. Linux kernel log, 2016. URL: http://thread.gmane.org/gmane.linux.kernel.lsm/28737
  90. Belousov K., Viro A.: Linux Kernel LSM file_permission Hook Restriction Bypass. 2005. URL: https://vulners.com/osvdb/OSVDB:25747
  91. Jurgens D. SELinux support for Infiniband RDMA. 2016. URL: https://lwn.net/Articles/684431/
  92. Goyal V. Overlayfs SELinux Support. 2016. URL: https://lwn.net/Articles/693663/
  93. Corbet J. ACCESS_ONCE() and compiler bugs. 2014. URL: https://lwn.net/Articles/624126/
  94. Draios, Sysdig 2018 URL: http://www.sysdig.org/
  95. Desnoyers M., Dagenais M. LTTng: Tracing across execution layers, from the hypervisor to user-space // Linux symposium, 2008.
  96. Gregg B., Mauro J. D’Trace: Dynamic Tracing in Oracle Solaris, Mac OS X and FreeBSD. Prentice Hall Professional, 2011.
  97. Ktap: A lightweight script-based dynamic tracing tool for Linux URL: https://github.com/ktap/ktap URL: http://www.ktap.org
  98. perf: Linux profiling with performance counters URL: https://perf.wiki.kernel.org/index.php/Main_Page
  99. ftrace Function Tracer URL: https://www.kernel.org/doc/Documentation/trace/ftrace.txt
  100. Eigler F.C. et al.: Architecture of systemtap: a Linux trace/probe tool. 2005.
  101. Méry D., Singh N.K. Automatic code generation from Event-B models // Proceedings of the second symposium on information and communication technology, ACM, 2011. pp. 179-188.
  102. Wright S. Automatic generation of C from Event-B // Workshop on integration of model-based formal methods and tools, 2009, 14 pp.
  103. Dalvandi M., Butler M., Rezazadeh A. From Event-B Models to Dafny Code Contracts // Fundamentals of Software Engineering, 2015, Springer International Publishing, LNCS volume 9392, ISBN: 978-3-319-24644-4 DOI: https://doi.org/10.1007/978-3-319-24644-4_21
  104. Новиков Е.М.: Развитие ядра операционной системы Linux // Труды Института системного программирования РАН. 2017. Т. 29, вып. 2. С. 77–96.
  105. E-ACSL Executable ANSI/ISO C Specification Language Version 1.12. URL: https://frama-c.com/download/e-acsl/e-acsl.pdf
  106. Delahaye M., Kosmatov N., Signoles J. Common specification language for static and dynamic analysis of C programs // Proceedings of the 28th Annual ACM Symposium on Applied Computing, ACM, 2013, С. 1230–1235.
  107. Kosmatov N., Petiot G., Signoles J. An optimized memory monitoring for runtime assertion checking of C programs // International Conference on Runtime Verification. Springer, Berlin, Heidelberg, 2013, С. 167–182.
  108. A Concise Summary of the Event-B mathematical toolkit. http://wiki.event-b.org/images/EventB-Summary.pdf
  109. AstraVer Toolset URL: https://forge.ispras.ru/projects/astraver-toolset
  110. Back R.-J. On the correctness of refinement steps in program development. Ph.D. thesis, University of Helsinki (1978).