Верификация соответствия между разноуровневыми моделями функциональных требований
https://doi.org/10.15514/ISPRAS-2020-32(6)-2
Аннотация
В статье предлагаются методы доказательства соответствия между разноуровневыми моделями, нацеленные на доказательство свойств безопасности в индивидуальной трассовой семантике. Эти методы более просты и пригодны для применения при решении практических задач верификации сложных видов функциональных требований по сравнению с традиционными подходами, основанными на установлении отношения уточнения между моделями.
При поддержке: Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 20-07-00954.
Об авторе
Алексей Владимирович ХОРОШИЛОВ
Институт системного программирования им. В.П. Иванникова РАН,
Московский государственный университет имени М. В. Ломоносова,
НИУ Высшая школа экономики,
Московский физико-технический институт
Россия
Кандидат физико-математических наук, ведущий научный сотрудник, директор Центра верификации ОС Linux в ИСП РАН, доцент кафедр системного программирования МГУ, ВШЭ и МФТИ
Россия
Кандидат физико-математических наук, ведущий научный сотрудник, директор Центра верификации ОС Linux в ИСП РАН, доцент кафедр системного программирования МГУ, ВШЭ и МФТИ
Список литературы
1. B. Alpern, F.B. Schneider. Defining liveness. Information Processing Letters, vol. 21, issue 4, 1985, pp. 181-185.
2. A. Khoroshilov. On formalization of operating systems behaviour verification. In Proc. of 11th International Conference on Computer Science and Information Technologies (CSIT-2017), 2017, pp. 168-172.
3. В.В. Кулямин, Н.В. Пакулин, О.Л. Петренко, А.А. Сортов, А.В. Хорошилов. Формализация требований на практике. Препринт no. 13, ИСП РАН, 2006 , 70 стр. / V.V. Kulyamin, N.V. Pakulin, O. L. Petrenko, A.A. Sortov, A.V. Khoroshilov. Formalization of requirements in practice. Preprint no. 13, ISP RAS, 2006, 70 pp. (in Russian).
4. J. He, C.A.R. Hoare, J.W. Sanders. Data refinement refined. Lecture Notes in Computer Science, vol. 213, 1986, pp. 187-196.
5. J.R. Abrial, D. Cansell, D. Méry. Refinement and reachability in Event-B. Lecture Notes in Computer Science, vol. 3455, 2005, pp. 222-241.
6. R.J.R. Back. Refinement of parallel and reactive programs. In M. Broy (ed). Program Design Calculi. Springer, 1993, pp. 73-92.
7. M. Butler. An approach to the design of distributed systems with B AMN. Lecture Notes in Computer Science, vol. 1212, 1997, pp. 223-241.
8. L. Aceto. Action Refinement in Process Algebras. Cambridge University Press, 1992, 283 p.
9. J. Derrick, E.A. Boiten. Non-atomic refinement in Z. Lecture Notes in Computer Science, vol. 1708, 1999, pp. 1477-1496.
10. G. Schellhorn. ASM refinement and generalizations of forward simulation in data refinement: A comparison. Theoretical Computer Sciences, vol. 336, issues 2-3, 2005, pp. 403–436.
11. П.Н. Девянин, В.В. Кулямин, А.Л. Оружейников, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Cпособ верификации формальной автоматной модели поведения программной системы. Патент на изобретение №2682003, 2019 г. / P.N. Devyanin, V.V. Kulyamin, A.L. Oruzheinikov, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. A method for verifying a formal automaton model of a software system's behavior. Patent for invention No. 2682003, 2019 (in Russian).
12. П.Н. Девянин, Д.В. Ефремов, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Моделирование и верификация политик безопасности управления доступом в операционных системах. М., Горячая линия – Телеком, 2019 г., 214 стр. / P.N. Devyanin, D.V. Efremov, V.V. Kulyamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Modeling and verification of access control security policies in operating systems. M., Hotline – Telecom, 2019, 214 p. (in Russian).
13. П.Н. Девянин, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы. Труды ИСП РАН, том 32, вып. 1, 2020 г., стр. 7-26. DOI: 10.15514/ISPRAS–2020–32(1)–1 / P.N. Devyanin, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System. Programming and Computer Software, 2020, vol. 46, issue 7, 2020, pp. 443–453. DOI: 10.1134/S0361768820070026.
14. V. Kuliamin, A. Khoroshilov, D. Medvedev. Formal Modeling of Multi-Level Security and Integrity Control Implemented with SELinux. In Proc. of the 2019 International Conference on Actual Problems of Systems and Software Engineering (APSSE), 2019, pp. 131-136.
15. А.В. Хорошилов, И.В. Щепетков. ADV_SPM – Формальные модели политики безопасности на практике. Труды ИСП РАН, том 29, вып. 3, 2017 г., стр. 43-56 / A.V. Khoroshilov, I.V. Shchepetkov. ADV_SPM – Formal security policy models in practice. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 3, 2017. pp. 43-56 (in Russian). DOI: 10.15514/ISPRAS-2017-29(3)-4.
16. ГОСТ Р ИСО/МЭК 15408-1-2012 Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 1. Введение и общая модель / ISO/IEC 15408-1:2012 Information technology - Security techniques - Evaluation criteria for IT security - Part 1: Introduction and general model.
17. ГОСТ Р ИСО/МЭК 15408-2-2013 Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 2. Функциональные компоненты безопасности / ISO/IEC 15408-2:2013 Information technology - Security techniques - Evaluation criteria for IT security - Part 2: Security functional requirements.
18. ГОСТ Р ИСО/МЭК 15408-3-2013 Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности / ISO/IEC 15408-3:2013 Information technology - Security techniques - Evaluation criteria for IT security - Part 3: Security assurance requirements.
Рецензия
Для цитирования:
ХОРОШИЛОВ А.В. Верификация соответствия между разноуровневыми моделями функциональных требований. Труды Института системного программирования РАН. 2020;32(6):19-30. https://doi.org/10.15514/ISPRAS-2020-32(6)-2
For citation:
KHOROSHILOV A.V. Verification of Compliance for Multilevel Models in Individual Trace Semantics. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(6):19-30. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(6)-2
Послать статью по эл. почте 