漏洞检测：从形式化验证到大语言模型及混合方法的综合概述
软件工程
2025-03-17 v1 人工智能
摘要
软件测试与验证是确保现代软件系统可靠性和安全性的关键。传统方法包括模型检查和定理证明等形式化验证技术，提供了严格的漏洞和缺陷检测框架。然而，这些方法在应用于复杂真实程序时常面临可扩展性挑战。最近，大语言模型（LLMs）的出现引入了新的软件分析范式，利用其理解不安全编码实践的能力。尽管 LLMs 在诊断预测和不变式生成等任务中表现出有前景的能力，但缺乏经典方法的形式化保证。本文对最新软件测试与验证技术进行了全面研究，聚焦三种关键方法：经典形式方法、LLM 基于分析以及新兴的混合技术，这些技术将两者优势结合起来。我们探讨了每种方法的优势、局限性和实际应用，突出了混合系统在解决单一方法弱点的潜力。我们分析了将形式化严谨性与 LLM 驱动的见解相结合是否能够增强软件验证的有效性和可扩展性，探讨了它们作为更健壮和自适应测试框架的可行性。
引用
@article{arxiv.2503.10784,
title = {Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview},
author = {Norbert Tihanyi and Tamas Bisztray and Mohamed Amine Ferrag and Bilel Cherif and Richard A. Dubniczky and Ridhi Jain and Lucas C. Cordeiro},
journal= {arXiv preprint arXiv:2503.10784},
year = {2025}
}