arXiv 2502.076442026-03-01cs.AI

SymGPT：通过结合符号执行与大语言模型审计智能合约

SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models

The Pennsylvania State University（宾夕法尼亚州立大学）；University of Connecticut（康涅狄格大学）；University of California San Diego（加州大学圣地亚哥分校）；University of Oxford（牛津大学）；SKLP, Institute of Computing Technology, Chinese Academy of Sciences（SKLP，计算技术研究所，中国科学院）

Shihao Xia, Mengting He, Shuai Shao, Tingting Yu, Yiying Zhang, Nobuko Yoshida, Linhai Song

备注：: 34 pages. arXiv admin note: text overlap with arXiv:2404.04306
DOI：: 10.1145/3798217

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

AI总结：

SymGPT结合符号执行与大语言模型，自动检测智能合约的ERC规则违规，识别出大量潜在安全漏洞。

摘要：

为了管理运行在以太坊上的智能合约，已经开发出多个以太坊请求评论（ERC）标准，每个标准定义了一组规定智能合约行为的规则。违反这些规则可能导致严重的安全问题和经济损失，这表明验证ERC合规性的重要性。目前的验证实践包括手动审计、专家开发的程序分析工具和大语言模型（LLMs），这些方法在检测ERC规则违规方面仍然无效。本文介绍了SymGPT，一种结合LLMs和符号执行的工具，用于自动验证智能合约对ERC规则的合规性。我们首先通过实证分析了132个ERC规则，来自三个主要ERC标准，研究了其内容、安全影响和自然语言描述。基于这项研究，SymGPT指导LLM将ERC规则翻译成领域特定语言，合成从翻译规则中得到的约束以建模潜在的违规情况，并通过符号执行进行违规检测。我们的评估显示，SymGPT在4000个真实世界合约中识别出5783个ERC规则违规，包括1375个具有明确攻击路径的财务盗窃违规。此外，SymGPT在六种自动化技术和一个安全专家审计服务中表现更优，凸显其优于当前智能合约分析方法。

英文摘要：

To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each defining a set of rules governing contract behavior. Violating these rules can cause serious security issues and financial losses, signifying the importance of verifying ERC compliance. Today's practices of such verification include manual audits, expert-developed program-analysis tools, and large language models (LLMs), all of which remain ineffective at detecting ERC rule violations. This paper introduces SymGPT, a tool that combines LLMs with symbolic execution to automatically verify smart contracts' compliance with ERC rules. We begin by empirically analyzing 132 ERC rules from three major ERC standards, examining their content, security implications, and natural language descriptions. Based on this study, SymGPT instructs an LLM to translate ERC rules into a domain-specific language, synthesizes constraints from the translated rules to model potential rule violations, and performs symbolic execution for violation detection. Our evaluation shows that SymGPT identifies 5,783 ERC rule violations in 4,000 real-world contracts, including 1,375 violations with clear attack paths for financial theft. Furthermore, SymGPT outperforms six automated techniques and a security-expert auditing service, underscoring its superiority over current smart contract analysis methods.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。