软件安全的新纪元：基于大语言模型与形式化验证的自修复软件
软件工程
2024-07-01 v2 人工智能
形式语言与自动机理论
机器学习
摘要
本文提出一种结合大语言模型（LLMs）与形式化验证策略的自动化软件漏洞修复创新方法。首先，我们采用有界模型检测（BMC）识别漏洞并提取反例。这些反例由数学证明及漏洞的栈追踪所支持。利用专门设计的提示，我们将原始源代码与已识别的漏洞（包括其栈追踪和指明行号与错误类型的反例）相结合。该组合信息随后输入 LLM，指示其尝试修复代码。新代码随后再次使用 BMC 验证以确保修复成功。我们提出 ESBMC-AI 框架作为概念验证，利用广受认可且被工业界采用的基于高效 SMT 的上下文有界模型检测器（ESBMC）与预训练 transformer 模型来检测并修复 C 程序中的错误，尤其是关键软件组件中的错误。我们在从 FormAI 数据集中随机选取的 50,000 个 C 程序及其相应漏洞分类上评估了该方法。结果表明，ESBMC-AI 能够高精度自动化检测并修复缓冲区溢出、算术溢出和指针解引用失败等问题。ESBMC-AI 是一项开创性举措，将 LLMs 与 BMC 技术相集成，有望融入软件开发生命周期中的持续集成与部署（CI/CD）流程。
引用
@article{arxiv.2305.14752,
title = {A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification},
author = {Norbert Tihanyi and Ridhi Jain and Yiannis Charalambous and Mohamed Amine Ferrag and Youcheng Sun and Lucas C. Cordeiro},
journal= {arXiv preprint arXiv:2305.14752},
year = {2024}
}