МЕТОДИ ФОРМАЛЬНОЇ ВЕРИФІКАЦІЇ ВИПРАВЛЕНЬ БІНАРНИХ ВРАЗЛИВОСТЕЙ СИСТЕМ КРИТИЧНОЇ ІНФРАСТРУКТУРИ

Микола Ільїн; Ірина Стьопочкіна; Олексій Новіков

doi:10.28925/2663-4023.2026.35.1347

Автор(и)

Микола Ільїн НТУУ «Київський політехнічний інститут імені Ігоря Сікорського» https://orcid.org/0000-0002-1065-6500
Ірина Стьопочкіна НТУУ «Київський політехнічний інститут імені Ігоря Сікорського» https://orcid.org/0000-0002-0346-0390
Олексій Новіков НТУУ «Київський політехнічний інститут імені Ігоря Сікорського» https://orcid.org/0000-0001-5988-3352

DOI:

https://doi.org/10.28925/2663-4023.2026.35.1347

Ключові слова:

Безпека промислових систем керування, безпека контуру операційних технологій, формальна верифікація, автоматизоване виправлення вразливостей, аналіз бінарних вразливостей

Анотація

Революційні зміни в індустрії кібербезпеки внаслідок розвитку генеративного штучного інтелекту суттєво вплинули на процеси пошуку, експлуатації і виправлення вразливостей програмних систем. Сучасні передові великі мовні моделі здатні автономно знаходити та виправляти вразливості програмного забезпечення на рівні експертизи, недосяжної для більшості людей. Відбуваються фундаментальні зміни в процесах кібербезпеки: агентна автономність штучного інтелекту зумовлює критичну важливість надійності цих нових процесів. В роботі досліджуються методи автоматизованого аналізу вразливостей програмного забезпечення високонадійних систем критичної інфраструктури на етапі верифікації виправлень. Проаналізовано передумови виникнення некоректних виправлень як наслідку галюцинацій -- структурних особливостей сучасних великих мовних моделей в результаті донавчання з депріоритезацією відмови від відповіді. Розглянуто існуючі методи виявлення і контролю галюцинацій, для процесів синтезу виправлень програмних продуктів запропоновано підхід на основі формальної верифікації вразливостей, повноти та еквівалентності виправлень. Запропоновано практичні методи формальної верифікації із застосуванням великих мовних моделей класу Leanstral-1.5, що синтезують програмний код Lean 4 для доказу коректності як знайденої вразливості, так і відповідності виправлення досліджуваній вразливості. Показано можливість автоматичного аналізу виправлень на рівні вихідного коду (зокрема С/C++), бінарних виправлень (на рівні машинного коду, ARM) та ефективне узагальнення на рівні проміжного представлення LLVM IR (включно з мовами високого рівня, що мають фронтенди LLVM, та машинним кодом підтримуваних QEMU архітектур процесорів через можливості ліфтингу платформи rev.ng). Експериментально досліджено точність запропонованих методів на наборі даних Vul4C (144 CVE у 23 відкритих програмних продуктах, 19 різних типів вразливостей CWE).

Завантаження

Дані завантаження ще не доступні.

Посилання

Anthropic (2026). Project Glasswing: Securing critical software for the AI era. https://www.anthropic.com/glasswing

OpenAI (2026). Daybreak: Frontier AI for Cyber Defenders. https://openai.com/daybreak

Zhipu AI (2026). Z.ai Security Disclosure ledger. https://cvd.z.ai

Wang, Z., Shi, T., He, J., Cai, M., Zhang, J., & Song, D. (2025). CyberGym: Evaluating AI Agents' Cybersecurity Capabilities with Real-World Vulnerabilities at Scale. arXiv. https://arxiv.org/abs/2506.02548

Wang, Z., Schiller, N., Li, H., Narayana, S. S., Nasr, M., Carlini, N., Qi, X., Wallace, E., Bursztein, E., Invernizzi, L., Thomas, K., Shoshitaishvili, Y., Guo, W., He, J., Holz, T., & Song, D. (2026). ExploitGym: Can AI Agents Turn Security Vulnerabilities into Real Attacks?. arXiv. https://arxiv.org/abs/2605.11086

Lee, S., & Brumley, D. (2026). ExploitBench: A Capability Ladder Benchmark for LLM Cybersecurity Agents. arXiv. https://arxiv.org/abs/2605.14153 Website: https://exploitbench.ai

Qwen Team (2026, August). Qwen3.8-Max: A New Bar for Coding and Cowork. https://qwen.ai/blog?id=qwen3.8

NIST (2026). UK AISI/CAISI Preliminary Assessment of Kimi K3's Cyber Capabilities. https://www.nist.gov/news-events/news/2026/07/uk-aisi-caisi-preliminary-assessment-kimi-k3s-cyber-capabilities

NIST (2026). CAISI Assessment of Z.ai's GLM-5.2. https://www.nist.gov/news-events/news/2026/07/caisi-assessment-zais-glm-52

Z.ai (2026). GLM-5.3: Frontier Coding with Emergent Cyber Capabilities. https://z.ai/blog/glm-5.3

Meta Superintelligence Lab (2026). Introducing Muse Glimmer: An Open Agentic Model That Runs on Your Device. https://research.meta.ai/blog/introducing-muse-glimmer-open-agentic-model

U.S. Department of Energy (2026). Genesis Open Models. https://genesisopenmodels.anl.gov

Kalai, A. T., Nachum, O., Vempala, S. S., & Zhang, E. (2025). Why Language Models Hallucinate. arXiv. https://arxiv.org/abs/2509.04664

Farquhar, S., Kossen, J., Kuhn, L., & Gal, Y. (2024, June). Detecting hallucinations in large language models using semantic entropy. Nature, 630(8017), 625-630. https://doi.org/10.1038/s41586-024-07421-0

Chen, C., Liu, K., Chen, Z., Gu, Y., Wu, Y., Tao, M., Fu, Z., & Ye, J. (2024). INSIDE: LLMs' Internal States Retain the Power of Hallucination Detection. arXiv. https://arxiv.org/abs/2402.03744

Azaria, A., & Mitchell, T. (2023). The Internal State of an LLM Knows When It's Lying. arXiv. https://arxiv.org/abs/2304.13734

Orgad, H., Toker, M., Gekhman, Z., Reichart, R., Szpektor, I., Kotek, H., & Belinkov, Y. (2025). LLMs Know More Than They Show: On the Intrinsic Representation of LLM Hallucinations. arXiv. https://arxiv.org/abs/2410.02707

Kossen, J., Han, J., Razzak, M., Schut, L., Malik, S., & Gal, Y. (2024). Semantic Entropy Probes: Robust and Cheap Hallucination Detection in LLMs. arXiv. https://arxiv.org/abs/2406.15927

Chuang, Y.-S., Qiu, L., Hsieh, C.-Y., Krishna, R., Kim, Y., & Glass, J. (2024). Lookback Lens: Detecting and Mitigating Contextual Hallucinations in Large Language Models Using Only Attention Maps. arXiv. https://arxiv.org/abs/2407.07071

Manakul, P., Liusie, A., & Gales, M. J. F. (2023). SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Models. arXiv. https://arxiv.org/abs/2303.08896

Zhang, J., Li, Z., Das, K., Malin, B., & Kumar, S. (2023, December). SAC3: Reliable Hallucination Detection in Black-Box Language Models via Semantic-aware Cross-check Consistency. In Findings of the Association for Computational Linguistics: EMNLP 2023, 15445–15458 pp. Association for Computational Linguistics. https://aclanthology.org/2023.findings-emnlp.1032/

Yehuda, Y., Malkiel, I., Barkan, O., Weill, J., Ronen, R., & Koenigstein, N. (2024, August). InterrogateLLM: Zero-Resource Hallucination Detection in LLM-Generated Answers. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 9333–9347 pp. Association for Computational Linguistics. https://aclanthology.org/2024.acl-long.506/

Tamber, M. S., Bao, F. S., Xu, C., Luo, G., Kazi, S., Bae, M., Li, M., Mendelevitch, O., Qu, R., & Lin, J. (2025). Benchmarking LLM Faithfulness in RAG with Evolving Leaderboards. arXiv. https://arxiv.org/abs/2505.04847

Magesh, V., Surani, F., Dahl, M., Suzgun, M., Manning, C. D., & Ho, D. E. (2025). Hallucination-Free? Assessing the Reliability of Leading AI Legal Research Tools. Journal of Empirical Legal Studies, 22(2), 216-242. https://onlinelibrary.wiley.com/doi/abs/10.1111/jels.12413

Alansari, A., & Luqman, H. (2026). Large Language Models Hallucination: A Comprehensive Survey. arXiv. https://arxiv.org/abs/2510.06265

Mishra, S., Niroula, S., Yadav, U., Thakur, D., Gyawali, S., & Gaire, S. (2026). SoK: Agentic Retrieval-Augmented Generation (RAG): Taxonomy, Architectures, Evaluation, and Research Directions. arXiv. https://arxiv.org/abs/2603.07379

Dhuliawala, S., Komeili, M., Xu, J., Raileanu, R., Li, X., Celikyilmaz, A., & Weston, J. (2023). Chain-of-Verification Reduces Hallucination in Large Language Models. arXiv. https://arxiv.org/abs/2309.11495

Tian, K., Mitchell, E., Yao, H., Manning, C. D., & Finn, C. (2023). Fine-tuning Language Models for Factuality. arXiv. https://arxiv.org/abs/2311.08401

Gu, Y., Zhang, W., Lyu, C., Lin, D., & Chen, K. (2025). Mask-DPO: Generalizable Fine-grained Factuality Alignment of LLMs. arXiv. https://arxiv.org/abs/2503.02846

Chaduvula, S., Radwan, A. Y., Farooq, A., Ioannou, Y., & Raza, S. (2026). Reducing Hallucinations in LLMs via Factuality-Aware Preference Learning. arXiv. https://arxiv.org/abs/2601.03027

Chuang, Y.-S., Xie, Y., Luo, H., Kim, Y., Glass, J., & He, P. (2024). DoLa: Decoding by Contrasting Layers Improves Factuality in Large Language Models. arXiv. https://arxiv.org/abs/2309.03883

Li, K., Patel, O., Viégas, F., Pfister, H., & Wattenberg, M. (2024). Inference-Time Intervention: Eliciting Truthful Answers from a Language Model. arXiv. https://arxiv.org/abs/2306.03341

Huang, J., Chen, X., Mishra, S., Zheng, H. S., Yu, A. W., Song, X., & Zhou, D. (2024). Large Language Models Cannot Self-Correct Reasoning Yet. arXiv. https://arxiv.org/abs/2310.01798

Tyen, G., Mansoor, H., Carbune, V., Chen, P., & Mak, T. (2024, August). LLMs cannot find reasoning errors, but can correct them given the error location. In Findings of the Association for Computational Linguistics: ACL 2024, 13894–13908 pp. Association for Computational Linguistics. https://aclanthology.org/2024.findings-acl.826/

Kirichenko, P., Ibrahim, M., Chaudhuri, K., & Bell, S. J. (2025). AbstentionBench: Reasoning LLMs Fail on Unanswerable Questions. arXiv. https://arxiv.org/abs/2506.09038

Voitsekhovskyi, A., Stopochkina, I., Sun, P., Xie, J., Ilin, M., & Novikov, O. (2026). Detection of vulnerabilities in software for unmanned aerial vehicles by using large language models. Eastern-European Journal of Enterprise Technologies, 1(2 (139)), 36–47. https://doi.org/10.15587/1729-4061.2026.352029

Novikov, O., Stopochkina, I., Voitsekhovskyi, A., & Ilin, M. (2024). Attack Models for Industrial Control System Elements Based on a Graph Approach and Countermeasures. In Proceedings of the XXIV International Scientific and Practical Conference "Information Technologies and Security" (ITS 2024), 67–82 pp. CEUR-WS.org. https://ceur-ws.org/Vol-4068/paper6.pdf

Novikov, O., Voitsekhovskyi, A., Stopochkina, I., Ilin, M., & Ovcharuk, M. (2025, December). Petri Net–Based Analysis of UAV Networks Availability Issues in Conditions of Adversary Counteraction. Theoretical and Applied Cybersecurity, 7(3), 67–73. https://doi.org/10.20535/tacs.2664-29132025.3.346322

de Moura, L., & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. In Automated Deduction – CADE 28, 625–635 pp. Springer. https://doi.org/10.1007/978-3-030-79876-5_37

Mistral AI (2026). Leanstral 1.5: Proof Abundance for All. https://mistral.ai/news/leanstral-1-5/

Lattner, C., & Adve, V. (2004, March). LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In Proceedings of the International Symposium on Code Generation and Optimization (CGO), 75–88 pp. https://doi.org/10.1155/2004/977395

Di Federico, A., Payer, M., & Agosta, G. (2017). rev.ng: a unified binary analysis framework to recover CFGs and function boundaries. In Proceedings of the 26th International Conference on Compiler Construction, 131–141 pp. Association for Computing Machinery. https://doi.org/10.1145/3033019.3033028

Hu, Y., Li, Z., Shu, K., Guan, S., Zou, D., Xu, S., Yuan, B., & Jin, H. (2025). SoK: automated vulnerability repair: methods, tools, and assessments. In Proceedings of the 34th USENIX Security Symposium (USENIX Security 25).