METHODS FOR FORMAL VERIFICATION OF BINARY VULNERABILITY PATCHES FOR CRITICAL INFRASTRUCTURE SYSTEMS
DOI:
https://doi.org/10.28925/2663-4023.2026.35.1347Keywords:
Industrial control system security, operational technology security, formal verification, automated vulnerability repair, binary vulnerability analysisAbstract
Revolutionary changes in the cybersecurity industry, driven by the development of generative AI, have significantly affected the processes of finding, exploiting, and fixing vulnerabilities in software systems. Modern frontier large language models can autonomously identify and fix software vulnerabilities with an expertise level unattainable for most people. Fundamental changes are taking place in cybersecurity processes: the agent autonomy of artificial intelligence determines the critical importance of the reliability of these new processes. The paper investigates methods for automated analysis of software vulnerabilities in highly reliable critical infrastructure systems at the patch verification stage. The prerequisites for the occurrence of incorrect patches as a consequence of hallucinations -- structural features of modern large language models as a result of additional training with deprioritization of refusal to respond, are analyzed. Existing methods for hallucination detection and control are considered, and an approach based on formal verification of vulnerabilities, completeness, and equivalence of patches is proposed for the synthesis of software product patches. Practical methods for formal verification are proposed using large language models of the Leanstral-1.5 class, which synthesize Lean 4 code to prove the correctness of both the found vulnerability and the patch's correspondence to the vulnerability under study. The possibility of automatic analysis of patches at the source code level (in particular C/C++), binary patches (at the machine code level, ARM), and effective generalization at the level of intermediate representation of LLVM IR (including high-level languages with LLVM frontends, and machine code of QEMU-supported processor architectures through the lifting capabilities of the rev.ng platform) is shown. The accuracy of the proposed methods was experimentally evaluated on the Vul4C dataset (144 CVEs across 23 open-source software products and 19 different CWE types).
Downloads
References
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).
Published
How to Cite
Issue
Section
License
Copyright (c) 2026 Микола Ільїн, Ірина Стьопочкіна, Олексій Новіков
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
