PropertyGPT：面向智能合约的 LLM 驱动形式化验证工具
摘要
近期大语言模型（LLM）的进展促使本文探讨了利用最先进的 LLM（如 GPT-4）将现有人类编写的属性（例如来自 Certora 审计报告的属性）并自动为未知代码生成定制属性的潜力。为此，我们将现有属性嵌入向量数据库，并检索参考属性以进行 LLM-based 的 in-context 学习，以为给定代码生成新属性。虽然这一基本过程相对直接，但确保生成的属性（i）可编译、（ii）合适、（iii）可验证仍具有挑战。为解决（i），我们使用编译和静态分析反馈作为外部 oracle，指导 LLM 在迭代修订生成的属性。为解决（ii），我们考虑多个相似性维度，对属性进行排序，并采用加权算法识别前 K 个属性作为最终结果。为解决（iii），我们设计了一个专门的证明器来形式化验证生成属性的正确性。我们将这些策略实现为一个新的 LLM-based 属性生成工具，称为 PropertyGPT。我们的实验表明，PropertyGPT 能够生成全面且高质量的属性，召回率达到 80%。它成功检测了 37 个测试中的 26 个 CVE/攻击事件，也发现了 12 个零日漏洞，带来 8,256 美元的 bug bounty 收入。
引用
@article{arxiv.2405.02580,
title = {PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation},
author = {Ye Liu and Yue Xue and Daoyuan Wu and Yuqiang Sun and Yi Li and Miaolei Shi and Yang Liu},
journal= {arXiv preprint arXiv:2405.02580},
year = {2024}
}
备注
Accepted by NDSS Symposium 2025. Please cite the conference version of this paper, e.g., "Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, Yang Liu. PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation. In 32nd Annual Network and Distributed System Security Symposium (NDSS 2025)."