In this paper we present a novel solution that combines the capabilities of
Large Language Models (LLMs) with Formal Verification strategies to verify and
automatically repair software vulnerabilities. Initially, we employ Bounded
Model Checking (BMC) to locate the software vulnerability and derive a
counterexample. The counterexample provides evidence that the system behaves
incorrectly or contains a vulnerability. The counterexample that has been
detected, along with the source code, are provided to the LLM engine. Our
approach involves establishing a specialized prompt language for conducting
code debugging and generation to understand the vulnerability's root cause and
repair the code. Finally, we use BMC to verify the corrected version of the
code generated by the LLM. As a proof of concept, we create ESBMC-AI based on
the Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained
Transformer model, specifically gpt-3.5-turbo, to detect and fix errors in C
programs. Our experimentation involved generating a dataset comprising 1000 C
code samples, each consisting of 20 to 50 lines of code. Notably, our proposed
method achieved an impressive success rate of up to 80% in repairing vulnerable
code encompassing buffer overflow and pointer dereference failures. We assert
that this automated approach can effectively incorporate into the software
development lifecycle's continuous integration and deployment (CI/CD) process.

利用大型语言模型和形式验证策略结合的新颖解决方案，自动检测和修复 C 程序中的软件漏洞，成功率高达 80％。

软件安全新时代：基于大型语言模型和形式验证的自愈软件

A New Era in Software Security: Towards Self-Healing Software via Large  Language Models and Formal Verification

We present Self-Driven Strategy Learning (sdsl), a lightweight online
learning methodology for automated reasoning tasks that involve solving a set
of related problems. sdsl automatically gathers information, in form of a
dataset, while solving earlier problems. It utilizes the learned data to adjust
the solving strategy for later problems by fitting a machine learning model to
the obtained data on the fly. We formally define the approach as a set of
abstract transition rules. We describe a concrete instance of the sdsl calculus
which uses conditional sampling for generating data and random forests as the
underlying machine learning model. We implement the approach on top of the
Kissat solver and show that the combination of Kissat+sdsl certifies larger
bounds and finds more counter-examples than other state-of-the-art bounded
model checking approaches on benchmarks obtained from the latest Hardware Model
Checking Competition.

自驱动策略学习是一种轻量级在线学习方法，适用于解决一组相关问题的自动化推理任务。它使用机器学习模型根据数据集调整后续问题的解决策略，从而实现更好的边界模型检查性能。

自动推理中相关问题集的轻量级在线学习

Lightweight Online Learning for Sets of Related Problems in Automated  Reasoning

Solving Constrained Horn Clauses (CHCs) is a fundamental challenge behind a
wide range of verification and analysis tasks. Data-driven approaches show
great promise in improving CHC solving without the painstaking manual effort of
creating and tuning various heuristics. However, a large performance gap exists
between data-driven CHC solvers and symbolic reasoning-based solvers. In this
work, we develop a simple but effective framework, "Chronosymbolic Learning",
which unifies symbolic information and numerical data points to solve a CHC
system efficiently. We also present a simple instance of Chronosymbolic
Learning with a data-driven learner and a BMC-styled reasoner. Despite its
great simplicity, experimental results show the efficacy and robustness of our
tool. It outperforms state-of-the-art CHC solvers on a dataset consisting of
288 benchmarks, including many instances with non-linear integer arithmetics.

本论文提出了 Chronosymbolic Learning 这一基于数据驱动的框架，结合符号信息和数值数据点解决 Constrained Horn Clauses（CHC）系统，此工具在包含许多非线性整数算术实例的数据集上表现出比现有 CHC 求解器更高的性能。