|
DOI: 10.14489/vkit.2026.05.pp.052-058
Трифонов В. И.
ФОРМАЛЬНЫЕ МЕТОДЫ В ЗАМКНУТОМ КОНТУРЕ ТРАНСФОРМАЦИИ ТРЕБОВАНИЙ ИНФОРМАЦИОННОЙ БЕЗОПАСНОСТИ ДЛЯ МНОГОУРОВНЕВЫХ СИСТЕМ УПРАВЛЕНИЯ
(с. 52-58)
Аннотация. Посвящена разработке комплексной методологии трансформации требований информационной безопасности в многоуровневых системах управления. Предложена интеграция подходов формальной спецификации (FormalMethods for Security) и формальной верификации (Formal Methods for Verification) в замкнутый контур обработки требований. Представлен синтез методов Model-Driven Security, политик уточнения требований, стандартов SCAP и технологий SMT-решателей для обеспечения семантической согласованности требований информационной безопасности на всех уровнях системы. Эта методология позволяет автоматизировать процесс трансформации требований безопасности, выявлять и разрешать конфликты между политиками различных уровней, а также верифицировать корректность конфигураций с использованием формальной логики.
Ключевые слова: формальные методы; верификация безопасности; трансформация требований; многоуровневые системы управления; семантическая согласованность; SMT-решатели; Model-Driven Security; политики безопасности; автоматизированная верификация; информационная безопасность.
Trifonov V. I.
FORMAL METHODS IN A CLOSED-LOOP TRANSFORMATION OF INFORMATION SECURITY REQUIREMENTS FOR MULTI-LEVEL CONTROL SYSTEMS
(pp. 52-58)
Abstract. This paper addresses the critical challenge transforming information security requirements within multi-level management systems where manual configuration leads to inconsistencies and vulnerabilities. The research develops a comprehensive methodology integrating Formal Methods for Security and Formal Methods for Verification into a closed-loop requirement processing framework. The proposed approach synthesizes four key components: Model-Driven Security techniques for automated policy generation, refinement methods enabling systematic transformation from high-level security objectives to low-level configurations, SCAP standards providing machine-readable security content representation, and SMT-solver technologies ensuring semantic consistency verification across all system levels. This integration creates a unified framework addressing the semantic gap between abstract security requirements and concrete implementation rules. The methodology operates through five distinct stages: requirements formalization using temporal logic notations (LTL, CTL), automated policy generation employing refinement algorithms, semantic consistency verification through SMT-solvers (Z3), conflict detection between inter-level policies, and feedback-driven requirement adjustment based on verification results. Dynamic policies adapt logging levels according to user roles and operation types, resolving conflicts such as blocking versus monitoring requirements. Experimental validation demonstrates the framework's capability to automatically detect cross-layer policy conflicts, reducing configuration errors by an order magnitude compared to manual approaches. The system identifies shadowing rules, redundant policies, and semantic inconsistencies that human administrators typically overlook. Automated verification using Z3 SMT-solver provides formal guarantees for configuration correctness, eliminating the 99% breach rate associated with manual misconfigurations reported by Gartner research. The methodology offers significant practical value for industrial SCADA systems, cloud environments, and enterprise networks requiring rigorous security assurance. Future work will extend the framework to incorporate machine learning techniques for adaptive policy optimization based on runtime security events.
Keywords: Formal methods; Security verification; Requirements transformation; multi-level control systems; Semantic consistency, SMT solvers, Model-Driven Security; Security policies; Automated verification; Information security.
В. И. Трифонов (Ростовский государственный экономический университет (РИНХ), Ростов-на-Дону, Россия) E-mail:
Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript
V. I. Trifonov (Rostov State University of Economics (RINH), Rostov-on-Don, Russia) E-mail:
Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript
1. Буйневич М. В., Ярошенко А. Ю. Обзор способов формализации требований к различным объектам и системам в аспекте решения задачи ранжирования // Научно-аналитический журнал «Вестник Санкт-Петербургского университета ГПС МЧС России». 2023. Т. № 3. С. 95–105.
2. Косачев А. С., Пономаренко В. Н. Анализ подходов к верификации функций безопасности и мобильности // Препринт Института системного программирования РАН. 2018. № 2(26). С. 2.
3. Приезжая А. Н. Технологии встраивания функций безопасности в бизнес-процессы // История и архивы. 2009. С. 71–83.
4. Оценка рисков киберфизических систем с использованием моделирования доменов и имитационного моделирования / А. А. Тейланс, А. В. Романов, Ю. А. Меркурьев и др. // Труды СПИИРАН. 2018. Т. 4(59). С. 115–139.
5. Vincent C. Hu. Security Property Verification by Transition Model // NIST Interagency Report (IR) 8539. 2025.
6. Hsu Tzu-Han, Sánchez C., Sheinvald S., Bonakdarpour B. Efficient Loop Conditions for Bounded Model Checking Hyperproperties. 2023. arxiv.org/pdf/2301.06209.
7. Pisarev I. A., Babenko L. K. C# parser for extracting cryptographic protocols structure from source code // Труды ИСП РАН. 2019. Т. 31(3). С. 191–202.
8. Карпов Ю. Г. MODEL СHECKING. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.
9. Белим С. В., Богаченко Н. Ф., Ракицкий Ю. С. Совмещение политик безопасности, основанное на алгоритмах поддержки принятия решений // Информационно-управляющие системы. 2016. № 5. С. 66–75.Полубелова О. В. Методика верификации правил фильтрации методом «Проверки на модели» // Инновации в науке. 2025. URL: https://cyberleninka.ru/article/n/metodika-verifikatsii-pravil-filtratsii-metodom-proverki-na-modeli/viewer (дата обращения: 15.12.2025).
10. Gérald Doussot. Software Verification and Analysis Using Z3. NCC Group: сайт. 2021. URL: https://www.nccgroup.com/research-blog/software-verification-and-analysis-using-z3/ (дата обращения: 10.04.2026).
11. Бубакар И., Будько М. Б., Будько М. Ю., Гирик А. В. Онтологическое обеспечение управления рисками информационной безопасности // Труды ИСП РАН. 2025. Т. 33(5). С. 41–64.
12. Basile C., Gatti G., Settanni F. A Formal Model of Security Controls Capabilities and Its Applications to Policy Refinement and Incident Management // IEEE/ACM Transactions on Networking. 2025. arxiv.org/pdf/2405.03544.
13. Eichler J., Rieke R. Model-Based Situational Security Analysis // Workshop Proceedings. 2011. URL: https://ceur-ws.org/Vol-794/paper_1.pdf (дата обращения: 17.12.2025).
14. Кораблин Ю. П., Шипов А. А. Унифицированное представление формул логик LTL и CTL системами рекурсивных уравнений // Программные продукты и системы. 2019. Т. 1(32). С. 20–25.
15. Горбачев И. Е. Концепция итерационного внешнего проектирования облика проактивных систем информационной безопасности // Вопросы кибербезопасности. 2017. № 5(24). С. 50–62.
16. Guo W., Zhang L., Lian X. Automatically detecting the conflicts between software requirements based on finer semantic analysis // Information and Software Technology. 2021. arxiv.org/pdf/2103.02255.
17. Лепешкин О. М., Харечкин П. В. Функционально-ролевая модель управления доступом в социотехнических системах // Известия Южного федерального университета. Технические науки. 2009. № 11(100). С. 52–57.
18. Земцов И. В. Об автоматизации процессов управления информационной безопасностью в образовательных организациях // Решетниковские чтения. 2015. Т. 2. С. 286–288.
1. Buinevich, M. V., & Yaroshenko, A. Yu. (2023). Review of methods for formalizing requirements for various objects and systems in the context of the ranking problem. Vestnik Sankt-Peterburgskogo universiteta GPS MChS Rossii, (3), 95–105. [in Russian language].
2. Kosachev, A. S., & Ponomarenko, V. N. (2018). Analysis of approaches to verification of safety and mobility functions. Preprint Instituta sistemnogo programmirovaniya RAN, (2), 2. [in Russian language].
3. Priezzhaya, A. N. (2009). Technologies for embedding security functions into business processes. Istoriya i arkhivy, 71–83. [in Russian language].
4. Teilans, A. A., Romanov, A. V., Merkuryev, Yu. A., et al. (2018). Risk assessment of cyber physical systems using domain modeling and simulation. Trudy SPIIRAN, 4(59), 115–139. [in Russian language].
5. Hu, V. C. (2025). Security property verification by transition model (NIST Interagency Report IR 8539). National Institute of Standards and Technology.
6. Hsu, T.-H., Sánchez, C., Sheinvald, S., & Bonakdarpour, B. (2023). Efficient loop conditions for bounded model checking hyperproperties. arXiv. https://arxiv.org/abs/2301.06209
7. Pisarev, I. A., & Babenko, L. K. (2019). C# parser for extracting cryptographic protocols structure from source code. Trudy ISP RAN, 31(3), 191–202. [in Russian language].
8. Karpov, Yu. G. (2010). Model checking. Verification of parallel and distributed software systems. BKhV Peterburg. [in Russian language].
9. Belim, S. V., Bogachenko, N. F., & Rakitsky, Yu. S. (2016). Combining security policies based on decision support algorithms. Informatsionno-upravlyayushchie sistemy, (5), 66–75. [in Russian language].
10. Polubelova, O. V. (2025). Methodology for verifying filtering rules using the “model checking” method. Innovatsii v nauke. Retrieved December 15, 2025, from https://cyberleninka.ru/article/n/metodika-verifikatsii-pravil-filtratsii-metodom-proverki-na-modeli/viewer [in Russian language].
11. Doussot, G. (2021). Software verification and analysis using Z3. NCC Group. Retrieved April 10, 2026, from https://www.nccgroup.com/research-blog/software-verification-and-analysis-using-z3/
12. Bubakar, I., Budko, M. B., Budko, M. Yu., & Girik, A. V. (2025). Ontological support for information security risk management. Trudy ISP RAN, 33(5), 41–64. [in Russian language].
13. Basile, C., Gatti, G., & Settanni, F. (2025). A formal model of security controls capabilities and its applications to policy refinement and incident management. arXiv. https://ceur-ws.org/Vol-794/paper_1.pdf
14. Eichler, J., & Rieke, R. (2011). Model based situational security analysis. Workshop Proceedings. Retrieved December 17, 2025, from https://ceur-ws.org/Vol-794/paper_1.pdf
15. Korablin, Yu. P., & Shipov, A. A. (2019). Unified representation of LTL and CTL logic formulas by systems of recursive equations. Programmnye produkty i sistemy, 1(32), 20–25. [in Russian language].
16. Gorbachev, I. E. (2017). Concept of iterative external design of the appearance of proactive information security systems. Voprosy kiberbezopasnosti, (5), 50–62. [in Russian language].
17. Guo, W., Zhang, L., & Lian, X. (2021). Automatically detecting the conflicts between software requirements based on finer semantic analysis. arXiv. https://arxiv.org/abs/2103.02255
18. Lepeshkin, O. M., & Kharechkin, P. V. (2009). Functional role model of access control in socio technical systems. Izvestiya Yuzhnogo federal'nogo universiteta. Tekhnicheskie nauki, (11), 52–57. [in Russian language].
19. Zemtsov, I. V. (2015). On automation of information security management processes in educational organizations. Reshetnikovskie chteniya, 2, 286–288. [in Russian language].
Статью можно приобрести в электронном виде (PDF формат).
Стоимость статьи 700 руб. (в том числе НДС 20%). После оформления заказа, в течение нескольких дней, на указанный вами e-mail придут счет и квитанция для оплаты в банке.
После поступления денег на счет издательства, вам будет выслан электронный вариант статьи.
Для заказа скопируйте doi статьи:
10.14489/vkit.2026.05.pp.052-058
и заполните форму
Отправляя форму вы даете согласие на обработку персональных данных.
.
This article is available in electronic format (PDF).
The cost of a single article is 700 rubles. (including VAT 20%). After you place an order within a few days, you will receive following documents to your specified e-mail: account on payment and receipt to pay in the bank.
After depositing your payment on our bank account we send you file of the article by e-mail.
To order articles please copy the article doi:
10.14489/vkit.2026.05.pp.052-058
and fill out the form
.
|
Current Issue
Разработка концепции и создание сайта - ООО «Издательский дом «СПЕКТР»