PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation

📄 arXiv: 2405.02580v2 📥 PDF

作者: Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, Yang Liu

分类: cs.SE, cs.AI

发布日期: 2024-05-04 (更新: 2024-12-06)

备注: 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)."

DOI: 10.14722/ndss.2025.241357

💡 一句话要点

PropertyGPT：利用LLM和检索增强生成智能合约的形式化验证属性

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 智能合约 形式化验证 大型语言模型 属性生成 检索增强 漏洞检测 安全审计

📋 核心要点

  1. 现有智能合约形式化验证方法依赖人工编写属性，成本高且难以覆盖所有潜在漏洞。
  2. PropertyGPT利用LLM和检索增强，自动生成针对特定智能合约的定制化形式化验证属性。
  3. 实验表明PropertyGPT能有效检测CVE和零日漏洞，并获得实际漏洞赏金，验证了其有效性。

📝 摘要（中文）

本文探索了利用大型语言模型（LLM），如GPT-4，来迁移现有的人工编写的属性（例如，来自Certora审计报告的属性），并自动为未知代码生成定制属性的潜力。为此，我们将现有属性嵌入到向量数据库中，并检索参考属性，以便基于LLM的上下文学习为给定代码生成新属性。虽然这个基本过程相对简单，但确保生成的属性是（i）可编译的，（ii）适当的，以及（iii）可验证的，都带来了挑战。为了解决（i），我们使用编译和静态分析反馈作为外部预言机，以指导LLM迭代地修改生成的属性。对于（ii），我们考虑多个相似性维度来对属性进行排序，并采用加权算法来识别前K个属性作为最终结果。对于（iii），我们设计了一个专用的证明器来正式验证生成的属性的正确性。我们已将这些策略实现到一个名为PropertyGPT的基于LLM的新型属性生成工具中。我们的实验表明，PropertyGPT可以生成全面且高质量的属性，与真实情况相比，实现了80%的召回率。它成功检测到37个测试中的26个CVE/攻击事件，并且还发现了12个零日漏洞，获得了8,256美元的漏洞赏金。

🔬 方法详解

问题定义：智能合约的安全性至关重要，形式化验证是保障其安全性的有效手段。然而，现有形式化验证方法依赖于人工编写属性，这既耗时又需要专业知识，并且难以保证属性的全面性，可能遗漏潜在的安全漏洞。因此，如何自动生成高质量、全面的智能合约形式化验证属性是一个亟待解决的问题。

核心思路：PropertyGPT的核心思路是利用大型语言模型（LLM）的强大代码生成能力，结合检索增强技术，自动生成针对特定智能合约的形式化验证属性。通过检索与目标合约相似的已有合约及其属性，并利用LLM进行迁移和修改，可以快速生成高质量的属性，降低人工成本，提高验证效率。

技术框架：PropertyGPT的整体框架包含以下几个主要模块：1) 属性检索模块：将已有的智能合约属性存储在向量数据库中，并根据目标合约的代码特征检索相似的属性。2) LLM属性生成模块：利用检索到的属性作为上下文，指导LLM生成新的属性。3) 属性编译与静态分析模块：使用Solidity编译器和静态分析工具对生成的属性进行检查，并将反馈信息传递给LLM进行迭代修改，确保属性的可编译性。4) 属性排序模块：根据多个相似性维度对生成的属性进行排序，选择Top-K个属性作为最终结果。5) 属性验证模块：使用专门设计的证明器对生成的属性进行形式化验证，确保其正确性。

关键创新：PropertyGPT的关键创新在于将LLM的代码生成能力与检索增强技术相结合，实现了智能合约形式化验证属性的自动生成。与传统方法相比，PropertyGPT无需人工编写属性，大大降低了验证成本，提高了验证效率。此外，PropertyGPT还引入了编译和静态分析反馈机制，以及属性排序模块，进一步提高了生成属性的质量和准确性。

关键设计：PropertyGPT的关键设计包括：1) 向量数据库的选择和属性嵌入方式；2) LLM的选择和prompt设计；3) 相似性度量指标的选择和加权算法的设计；4) 证明器的设计和验证策略。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

PropertyGPT在实验中取得了显著成果，与真实情况相比，实现了80%的召回率。它成功检测到37个测试中的26个CVE/攻击事件，并且还发现了12个零日漏洞，获得了8,256美元的漏洞赏金。这些结果表明PropertyGPT能够生成高质量的属性，并有效检测智能合约中的安全漏洞。

🎯 应用场景

PropertyGPT可应用于智能合约的自动化安全审计，降低审计成本，提高审计效率。它还可以作为智能合约开发过程中的辅助工具，帮助开发者尽早发现和修复潜在的安全漏洞。未来，该技术有望推广到其他软件系统的形式化验证领域，提升软件的整体安全性。

📄 摘要（原文）

With recent advances in large language models (LLMs), this paper explores the potential of leveraging state-of-the-art LLMs,such as GPT-4, to transfer existing human-written properties (e.g.,those from Certora auditing reports) and automatically generate customized properties for unknown code. To this end, we embed existing properties into a vector database and retrieve a reference property for LLM-based in-context learning to generate a new property for a given code. While this basic process is relatively straightforward, ensuring that the generated properties are (i) compilable, (ii) appropriate, and (iii) verifiable presents challenges. To address (i), we use the compilation and static analysis feedback as an external oracle to guide LLMs in iteratively revising the generated properties. For (ii), we consider multiple dimensions of similarity to rank the properties and employ a weighted algorithm to identify the top-K properties as the final result. For (iii), we design a dedicated prover to formally verify the correctness of the generated properties. We have implemented these strategies into a novel LLM-based property generation tool called PropertyGPT. Our experiments show that PropertyGPT can generate comprehensive and high-quality properties, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and also uncovered 12 zero-day vulnerabilities, leading to $8,256 in bug bounty rewards.